Incremental pattern-based coinduction for process algebra and its isabelle formalization

Andrei Popescu, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFoundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
Pages109-127
Number of pages19
DOIs
StatePublished - 2010
Event13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 - Paphos, Cyprus
Duration: Mar 20 2010Mar 28 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6014 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
CountryCyprus
CityPaphos
Period3/20/103/28/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Incremental pattern-based coinduction for process algebra and its isabelle formalization'. Together they form a unique fingerprint.

Cite this