2008 | OriginalPaper | Buchkapitel
Distributed Timed Automata with Independently Evolving Clocks
verfasst von : S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund, K. Narayan Kumar
Erschienen in: CONCUR 2008 - Concurrency Theory
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
We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to.
There are two natural semantics for such systems. The
universal
semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. However, to check if a system avoids a negative specification, it is better to use the
existential
semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates.
We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness turns out to be undecidable. As an alternative to the universal semantics, we propose a
reactive
semantics that allows us to check positive specifications and yet describes a regular set of behaviors.