Effective recognizability and model checking of reactive fiffo automata

Gregoire Sutre; Alain Finkel; Olivier Roux; Franck Cassez

doi:10.1007/3-540-49253-4_10

Effective recognizability and model checking of reactive fiffo automata

Gregoire Sutre, Alain Finkel, Olivier Roux, Franck Cassez

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

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 language	English
Title of host publication	Algebraic methodology and software technology
Subtitle of host publication	7th International Conference, AMAST’98 Amazonia, Brazil, January 4–8, 1999 Proceedings
Editors	Armando M. Haeberer
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	106-123
Number of pages	18
Volume	1548
ISBN (Electronic)	9783540492535
ISBN (Print)	3540654623, 9783540654629
DOIs	https://doi.org/10.1007/3-540-49253-4_10
Publication status	Published - 1999
Externally published	Yes
Event	7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998 - Amazonia, Brazil Duration: 4 Jan 1999 → 8 Jan 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1548
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Other

Other	7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998
Country/Territory	Brazil
City	Amazonia
Period	4/01/99 → 8/01/99

Access to Document

10.1007/3-540-49253-4_10

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). Springer, Springer Nature. https://doi.org/10.1007/3-540-49253-4_10

Sutre, Gregoire ; Finkel, Alain ; Roux, Olivier et al. / Effective recognizability and model checking of reactive fiffo automata. Algebraic methodology and software technology: 7th International Conference, AMAST’98 Amazonia, Brazil, January 4–8, 1999 Proceedings. editor / Armando M. Haeberer. Vol. 1548 Berlin : Springer, Springer Nature, 1999. pp. 106-123 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2d00fbcd93804ca191c83ce925faa787,

title = "Effective recognizability and model checking of reactive fiffo automata",

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

author = "Gregoire Sutre and Alain Finkel and Olivier Roux and Franck Cassez",

year = "1999",

doi = "10.1007/3-540-49253-4_10",

language = "English",

isbn = "3540654623",

volume = "1548",

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

publisher = "Springer, Springer Nature",

pages = "106--123",

editor = "Haeberer, {Armando M.}",

booktitle = "Algebraic methodology and software technology",

address = "United States",

note = "7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998 ; Conference date: 04-01-1999 Through 08-01-1999",

}

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

Effective recognizability and model checking of reactive fiffo automata. / Sutre, Gregoire; Finkel, Alain; Roux, Olivier et al.
Algebraic methodology and software technology: 7th International Conference, AMAST’98 Amazonia, Brazil, January 4–8, 1999 Proceedings. ed. / Armando M. Haeberer. Vol. 1548 Berlin: Springer, Springer Nature, 1999. p. 106-123 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1548).

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

TY - GEN

T1 - Effective recognizability and model checking of reactive fiffo automata

AU - Sutre, Gregoire

AU - Finkel, Alain

AU - Roux, Olivier

AU - Cassez, Franck

PY - 1999

Y1 - 1999

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

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

UR - http://www.scopus.com/inward/record.url?scp=84958999085&partnerID=8YFLogxK

U2 - 10.1007/3-540-49253-4_10

DO - 10.1007/3-540-49253-4_10

M3 - Conference proceeding contribution

AN - SCOPUS:84958999085

SN - 3540654623

SN - 9783540654629

VL - 1548

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

SP - 106

EP - 123

BT - Algebraic methodology and software technology

A2 - Haeberer, Armando M.

PB - Springer, Springer Nature

CY - Berlin

T2 - 7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998

Y2 - 4 January 1999 through 8 January 1999

ER -

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

Effective recognizability and model checking of reactive fiffo automata

Abstract

Publication series

Other

Access to Document

Other files and links

Fingerprint

Cite this