ACG

Circular Behavioral Reasoning

Circular coinduction was introduced by G. Rosu and J. Goguen (IJCAR 2001, WADT 2002) as an algorithm for proving behavioral properties expressed as indistinguishability under experiments, where the experiments are described as particular contexts. Later, G. Rosu and D. Lucanu formalized the circular coinduction as a proof system (CALCO 2009) and extended it with special contexts (ICFEM 2009) and equational interpolants (ICFEM 2010). The current proof system is implemented in CIRC tool: http://fsl.cs.uiuc.edu/index.php/Circ https://fmse.info.uaic.ro/projects/5/?t=info The tool can be used for proving properties of streams, infinite binary trees, processes, regular expressions defined by polynomial functors, etc. During the development of the CIRC tool, we noticed that the same circularity principle can be applied for proving inductive properties in an automated way.

In this talk we present an abstract formalism of the circular behavioral reasoning such that the circular coinduction and circular induction are instances of this formalism. This result is somehow surprising, since the induction and the coinduction are dual notions. We also discuss some aspects regarding the combination of the two proving techniques in this formalism.

ACG

Other presentations

An Introduction to K Framework by Examples

Other presentations

hosted by

social