Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization

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.

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Andrei Popescu, Elsa L. Gunter
• Keywords: Applied Computing, Coinductive Proof, FOSSACS 2010, Priori Unknown Bisimulation, Simone SOS Format