Record Details

Distributed Timed Automata with Independently Evolving Clocks

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Distributed Timed Automata with Independently Evolving Clocks
 
Creator AKSHAY, S
BOLLIG, B
GASTIN, P
MUKUND, M
KUMAR, KN
 
Subject timed automata
distributed systems
 
Description 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. 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 or universality 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.
 
Publisher IOS PRESS
 
Date 2014-12-28T17:27:50Z
2014-12-28T17:27:50Z
2014
 
Type Article
 
Identifier FUNDAMENTA INFORMATICAE, 130(4)377-407
0169-2968
1875-8681
http://dx.doi.org/10.3233/FI-2014-996
http://dspace.library.iitb.ac.in/jspui/handle/100/16988
 
Language English