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

Andrei Popescu; Elsa L. Gunter

doi:10.1007/978-3-642-12032-9_9

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

Andrei Popescu
, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Foundations 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.
Pages	109-127
Number of pages	19
DOIs	https://doi.org/10.1007/978-3-642-12032-9_9
State	Published - 2010
Event	13th 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 2010 → Mar 28 2010

Publication series

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

Other

Other	13th 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
Country/Territory	Cyprus
City	Paphos
Period	3/20/10 → 3/28/10

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-642-12032-9_9

Library availability

Discover UIUC Full Text

Cite this

Popescu, A., & Gunter, E. L. (2010). Incremental pattern-based coinduction for process algebra and its isabelle formalization. In Foundations 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. (pp. 109-127). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS). https://doi.org/10.1007/978-3-642-12032-9_9

Incremental pattern-based coinduction for process algebra and its isabelle formalization. / Popescu, Andrei; Gunter, Elsa L.
Foundations 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.. 2010. p. 109-127 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Popescu, A & Gunter, EL 2010, Incremental pattern-based coinduction for process algebra and its isabelle formalization. in Foundations 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.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6014 LNCS, pp. 109-127, 13th 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, 3/20/10. https://doi.org/10.1007/978-3-642-12032-9_9

Popescu A, Gunter EL. Incremental pattern-based coinduction for process algebra and its isabelle formalization. In Foundations 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.. 2010. p. 109-127. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-12032-9_9

Popescu, Andrei ; Gunter, Elsa L. / Incremental pattern-based coinduction for process algebra and its isabelle formalization. Foundations 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.. 2010. pp. 109-127 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b5cfddaf057a426b84e6c9e0e39e8bd0,

title = "Incremental pattern-based coinduction for process algebra and its isabelle formalization",

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.",

author = "Andrei Popescu and Gunter, \{Elsa L.\}",

year = "2010",

doi = "10.1007/978-3-642-12032-9\_9",

language = "English (US)",

isbn = "3642120318",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "109--127",

booktitle = "Foundations 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.",

note = "13th 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 ; Conference date: 20-03-2010 Through 28-03-2010",

}

TY - GEN

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

AU - Popescu, Andrei

AU - Gunter, Elsa L.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/77951490227

UR - https://www.scopus.com/pages/publications/77951490227#tab=citedBy

U2 - 10.1007/978-3-642-12032-9_9

DO - 10.1007/978-3-642-12032-9_9

M3 - Conference contribution

AN - SCOPUS:77951490227

SN - 3642120318

SN - 9783642120312

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 109

EP - 127

BT - Foundations 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.

T2 - 13th 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

Y2 - 20 March 2010 through 28 March 2010

ER -

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this