Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Event Clock Automata: From Theory to Practice
verfasst von : Gilles Geeraerts, Jean-François Raskin, Nathalie Sznajder
Erschienen in: Formal Modeling and Analysis of Timed Systems
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
Event clock automata
(
ECA
) are a model for
timed languages
that has been introduced by Alur, Fix and Henzinger as an alternative to
timed automata
, with better theoretical properties (for instance,
ECA
are determinizable while timed automata are not). In this paper, we
revisit
and
extend
the theory of
ECA
. We first prove that
no finite time abstract language equivalence
exists for
ECA
, thereby disproving a claim in the original work on
ECA
. This means in particular that regions
do not form a time abstract bisimulation
. Nevertheless, we show that regions can still be used to build a finite automaton recognizing the
untimed language of an
ECA
.
Then, we extend the classical notions of
zones
and
DBMs
to let them handle event clocks instead of plain clocks (as in timed automata) by introducing
event zones
and
Event DBMs
(EDBMs). We discuss algorithms to handle event zones represented as EDBMs, as well as (semi-) algorithms based on EDBMs to decide language emptiness of
ECA
.