Logic in Computer Science (LICS 2002)

Paper: Computing reachability relations in timed automata (at LICS 2002)

Authors: Catalin Dima

Abstract

Several problems in the domain of verification of real-time systems translate to checking whether a set of states is reachable in a timed automaton. The possibility to reach, starting from a state q, another state r in a timed automata depends essentially on the clock values with which one starts from state q. Moreover, even if r is reachable by starting from q with the clock values denoted by the vector v, the set of clock values when reaching r is in general an uncountable set. The dependence between clock values when starting from q and clock values when reaching r, call it the reachability relation defined by q and r, is an important characteristics for the timed automaton, and its algorithmic computation would be another way of attacking verification problems in timed automata. This algorithmic computation is the subject of this paper. Our approach is to build the reachability relations by computing unions, compositions and reflexive-transitive closures of such relations. The main feature that allows us to take this approach is a representation of relations by means of finite automata: we introduce 2n-automata as a new representation of the relations that are associated to each transition in a timed automaton. The idea is that each tuple in the relation is coded by a run in the 2n-automaton. We then show that these automata are closed under union, concatenation and (for mild conditions) star and have a decidable emptiness problem. We also show that the mild conditions are necessary since in general star closure is not possible, and that the 2n-automata arising from the relational semantics of timed automata bear these mild conditions.

BibTeX

  @InProceedings{Dima-Computingreachabili,
    author = 	 {Catalin Dima},
    title = 	 {Computing reachability relations in timed automata},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }