Verification of embedded reactive fiffo systems

Frédéric Herbreteau, Franck Cassez, Alain Finkel, Olivier Roux, Grégoire Sutre

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


Reactive Fiffo Systems (RFS) are used to model reactive systems which are able to memorize the events that cannot be processed when they occur. In this paper we investigate the decidability of verification problems for Embedded RFS which are RFS running under some environmental constraints. We show that almost all the usual verification problems are undecidable for the class of Periodically Embedded RFS with two memorizing events, whereas they become decidable for Regularly Embedded RFS with a single memorizing event. We then focus on Embedded Lossy RFS and we show in particular that for Regularly Embedded Lossy RFS the set of predecessors Pred is upward closed and effectively computable.

Original languageEnglish
Title of host publicationLATIN 2002 : Theoretical Informatics - 5th Latin American Symposium, Proceedings
EditorsSergio Rajsbaum
Place of PublicationBerlin; Heidelberg
PublisherSpringer, Springer Nature
Number of pages15
ISBN (Electronic)3540434003, 9783540434009
Publication statusPublished - 2002
Externally publishedYes
Event5th Latin American Symposium on Theoretical Informatics, LATIN 2002 - Cancun, Mexico
Duration: 3 Apr 20026 Apr 2002

Publication series

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


Other5th Latin American Symposium on Theoretical Informatics, LATIN 2002


  • Decidability
  • Embedded systems
  • Infinite-state systems
  • Reactive fiffo systems
  • Real-time systems
  • Verification

Fingerprint Dive into the research topics of 'Verification of embedded reactive fiffo systems'. Together they form a unique fingerprint.

Cite this