Sciweavers

ICFEM
2009
Springer

Circular Coinduction with Special Contexts

13 years 10 months ago
Circular Coinduction with Special Contexts
Coinductive proofs of behavioral equivalence often require human ingenuity, in that one is expected to provide a “good” relation extending one’s goal with additional lemmas, making automation of coinduction a challenging problem. Since behavioral satisfaction is a Π0 2 -hard problem, one can only expect techniques and methods that approximate the behavioral equivalence. Circular coinduction is an automated technique to prove behavioral equivalence by systematically exploring the behaviors of the property to prove: if all behaviors are circular then the property holds. Empirical evidence shows that one of the major reasons for which circular coinduction does not terminate in practice is that the circular behaviors may be guarded by a context. However, not all contexts are safe. This paper proposes a large class of contexts which are safe guards for circular behaviors, called special contexts, and extends circular coinduction appropriately. The resulting technique has been impleme...
Dorel Lucanu, Grigore Rosu
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ICFEM
Authors Dorel Lucanu, Grigore Rosu
Comments (0)