Effective recognizability and model checking of reactive fiffo automata

Gregoire Sutre, Alain Finkel, Olivier Roux, Franck Cassez

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

5 Citations (Scopus)

Abstract

Our work intends to verify reactive systems with event memorization specified with the reactive language Electre. For this, we define a particular behavioral model for Electre programs, Reactive Fiffo Automata (RFAs), which is close to Fifo Automata. Intuitively, a RFA is the model of a reactive system which may store event occurrences that must not be immediately taken into account. We show that, contrarily to lossy systems where the reachability set is recognizable but not effectively computable, (1) the reachability set of a RFA is recognizable, and (2) it is effectively computable. Moreover, we also study the relationships between RFAs and Finite Automata and we prove that (3) from a trace language point of view, inclusions between RFAs and Finite Automata are undecidable and (4) the linear temporal logic LTL on states without the temporal operator next is decidable for RFAs, while LTL on transitions is undecidable.

Original languageEnglish
Title of host publicationAlgebraic methodology and software technology
Subtitle of host publication7th International Conference, AMAST’98 Amazonia, Brazil, January 4–8, 1999 Proceedings
EditorsArmando M. Haeberer
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Pages106-123
Number of pages18
Volume1548
ISBN (Electronic)9783540492535
ISBN (Print)3540654623, 9783540654629
DOIs
Publication statusPublished - 1999
Externally publishedYes
Event7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998 - Amazonia, Brazil
Duration: 4 Jan 19998 Jan 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1548
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998
CountryBrazil
CityAmazonia
Period4/01/998/01/99

Fingerprint Dive into the research topics of 'Effective recognizability and model checking of reactive fiffo automata'. Together they form a unique fingerprint.

  • Cite this

    Sutre, G., Finkel, A., Roux, O., & Cassez, F. (1999). Effective recognizability and model checking of reactive fiffo automata. In A. M. Haeberer (Ed.), Algebraic methodology and software technology: 7th International Conference, AMAST’98 Amazonia, Brazil, January 4–8, 1999 Proceedings (Vol. 1548, pp. 106-123). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1548). Berlin: Springer, Springer Nature. https://doi.org/10.1007/3-540-49253-4_10