Paper Info
Title
Distributed Timed Automata with Independently Evolving Clocks
Abstract
We propose a model of distributed timed systems where each com- ponent is a timed automaton with a set of local clocks that evolve at a rate in- dependent 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 cap- tures behaviors that hold under any choice of clock rates for the individual com- ponents. This is a natural choice when checking that a system always satisfies a positive specification. However, to check if a system avoids a negative specifi- cation, 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 behav- iors. However, in the case of universal semantics, checking emptiness turns out to be undecidable. As an alternative to the universal semantics, we propose a re- active semantics that allows us to check positive specifications an d yet describes a regular set of behaviors.
Year
DOI
Venue
2014
10.3233/FI-2014-996
International Conference on Concurrency Theory
Keywords
Field
DocType
individual component,existential semantics,natural semantics,independently evolving clocks,universal semantics,natural choice,positive specification,regular set,reactive semantics,clock rate,timed automata,local clock,distributed systems
Discrete mathematics,Natural semantics,Automaton,Algorithm,Theoretical computer science,Timed automaton,Emptiness,Universality (philosophy),Mathematics,Semantics,Undecidable problem
Journal
Volume
Issue
ISSN
130
4
0169-2968
Citations 
PageRank 
References 
8
0.52
19
Authors
5
Name
Order
Citations
PageRank
S. Akshay16112.47
Benedikt Bollig242735.02
Paul Gastin3116575.66
Madhavan Mukund453043.20
K. Narayan Kumar51396.98