Circular Coinduction-based Techniques for Proving Behavioral Properties

Behavioral abstraction in algebraic specification appears undervarious names in the literature such as hidden algebra (Goguen et al.),observational logic (Hennicker, Bidoit), swinging types (Padawitz),coherent hidden algebra (Diaconescu, Futatsugi), hidden logic (Rosu), andso on.  Most of these approaches appeared as a need to extendalgebraic specifications to ease the process of specifying andverifying designs of systems and also for various other reasons, suchas, to naturally handle infinite types, to give semantics to the objectparadigm, to specify finitely otherwise infinitely axiomatizableabstract data types, etc.  The main characteristic of these approachesis that sorts are split into visible (directly accessible)for data and hidden (not directly accessible) for states, and the equality is behavioral,in the sense that two states are behaviorally equivalent if andonly if they appear to be the same under any visible experiment. 
Coalgebraic bisimulation and context induction are sound prooftechniques for behavioral equivalence.  Unfortunately, both need humanintervention: coinduction to pick a “good” bisimulation relation,and context induction to invent and prove lemmas.Circular coinduction is an automatic proof technique for behavioral equivalence.
CIRC is an automated circular coinductive prover for propetiesexpressed as behavioral equiavlences. CIRC is implemented as anextension of Maude (maude.cs.uiuc.edu) using metalevel capabilities ofrewriting logic.   In this talk we present the CIRC tool together with the circular coinductive-based techniques that forms the core of CIRC.

Sidebar