Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Popescu, Andrei; Gunter, Elsa L.
Loading…
Permalink
https://hdl.handle.net/2142/14858
Description
Title
Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Author(s)
Popescu, Andrei
Gunter, Elsa L.
Issue Date
2010-01-28
Keyword(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."
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
