Distributed Event Clock Automata: Extended abstract

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

282 Downloads (Pure)


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
Number of pages14
ISBN (Print)9783642222559
Publication statusPublished - 2011


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

Cite this