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 |