Verification of Embedded Reactive Fiffo Systems

Abstract:

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 memorized event. We then focus on Embedded Lossy RFS and we shoe in particular that for Regurlarly Embedded RFS the set of predecessors Pre* is upward closed and effectively computable.

Keywords:

Reactive Fiffo Systems, Embedded Systems, Verification, Real-time Systems, Infinite-State Systems, Decidability.

Download:

[ps.gz | pdf]

BibTeX entry:

@InProceedings{HCFRS:LATIN02, author = "Herbreteau, F. and Cassez, F. and Finkel, A. and Roux, O. and Sutre, G.", title = "Verification of Embedded Reactive Fiffo Systems", booktitle = "Proc.\ 5th Latin American Theoretical INformatics Conference (LATIN'02), Canc\'un, M\'exico", volume = "2286", series = "Lecture Notes in Computer Science", publisher = "Springer", year = "2002", month = apr, pages = "400--414", }