Distributed Event Clock Automata: Extended abstract

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

242 Downloads (Pure)

Abstract

In distributed real-time systems, we cannot assume that clocks are perfectly synchronized. To model them, we use independent clocks and define their timed semantics. The universal timed language, and the timed language inclusion of icTA are undecidable. Thus, we propose Recursive Distributed Event Clock Automata (DECA). DECA are closed under all boolean operations and their timed language inclusion problem is decidable (more precisely PSPACE-complete), allowing stepwise refinement. We also propose Distributed Event Clock Temporal Logic (DECTL), a real-time logic with independent time evolutions. This logic can be model-checked by translating a DECTL formula into a DECA automaton.
Original languageEnglish
Title of host publicationCIAA 2011
Subtitle of host publication16th International Conference on Implementation and Application of Automata
EditorsB Bouchou-Markhoff
Place of PublicationHeidelberg
PublisherSpringer
Pages250-263
Number of pages14
Volume6807
ISBN (Print)9783642222559
DOIs
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'Distributed Event Clock Automata: Extended abstract'. Together they form a unique fingerprint.
  • Model-driven engineering

    Cleve, A.

    1/01/1031/01/10

    Project: Research Axis

Cite this