| Title: | Incremental pattern-based coinduction for process algebra and its Isabelle formalization |
| Author(s): | Popescu, Andrei; Gunter, Elsa L. |
| Subject(s): | Process Algebra, de Simone SOS, Incremental Coniduction, Isabelle/HOL |
| Abstract: | We present a coinductive proof system for bisimilarity in transition systems
specifiable in the de Simone SOS format.
Our coinduction is incremental,
in that it allows building incrementally an a priori unknown
bisimulation, and pattern-based, in that it works on equalities
of process patterns (i.e., universally quantified equations of process terms
containing process variables), thus taking advantage of equational reasoning
in a ``circular" manner, inside coinductive proof loops. The
proof system has been formalized and proved sound in Isabelle/HOL. |
| Issue Date: | 2010-01-28 |
| Citation Info: | FOSSACS 2010, editor C.-H. L. Ong |
| Series/Report: | LNCS 6014 |
| Genre: | Article |
| Type: | Text |
| Language: | English |
| URI: | http://hdl.handle.net/2142/14858 |
| Publication Status: | published or submitted for publication |
| Peer Reviewed: | is peer reviewed |
| Date Available in IDEALS: | 2010-01-28 |
Coind.pdf (325kB)