Files in this item



application/pdfCoind.pdf (325kB)
(no description provided)PDF


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
Publication Status:published or submitted for publication
Peer Reviewed:is peer reviewed
Date Available in IDEALS:2010-01-28

This item appears in the following Collection(s)

Item Statistics