2011 | OriginalPaper | Buchkapitel
Distributed Event Clock Automata
Extended Abstract
verfasst von : James Ortiz, Axel Legay, Pierre-Yves Schobbens
Erschienen in: Implementation and Application of Automata
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.