Paper Info
Title
Timed automata with disjoint activity
Abstract
The behavior of timed automata consists of idleness and activity, i.e. delay and action transitions. We study a class of timed automata with periodic phases of activity. We show that, if the phases of activity of timed automata in a network are disjoint, then location reachability for the network can be decided using a concatenation of timed automata. This reduces the complexity of verification in Uppaal-like tools from quadratic to linear time (in the number of components) while traversing the same reachable state space. We provide templates which imply, by construction, the applicability of sequential composition, a variant of concatenation, which reflects relevant reachability properties while removing an exponential number of states. Our approach covers the class of TDMA-based (Time Division Multiple Access) protocols, e.g. FlexRay and TTP. We have successfully applied our approach to an industrial TDMA-based protocol of a wireless fire alarm system with more than 100 sensors.
Year
DOI
Venue
2012
10.1007/978-3-642-33365-1_14
FORMATS
Keywords
Field
DocType
exponential number,location reachability,periodic phase,relevant reachability property,disjoint activity,industrial tdma-based protocol,reachable state space,linear time,uppaal-like tool,time division multiple access,timed automaton,action transition
FlexRay,Discrete mathematics,Disjoint sets,Computer science,Automaton,Theoretical computer science,Reachability,Timed automaton,Concatenation,Time complexity,Time division multiple access
Conference
Citations 
PageRank 
References 
6
0.45
15
Authors
3
Name
Order
Citations
PageRank
Marco Muñiz1545.68
Bernd Westphal2438.45
Andreas Podelski32760197.87