Nicolas Markey

Abstract

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks.

First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.

@inproceedings{concur2004-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking Timed Automata with One or Two
                         Clocks},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {387-401},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_25},
  abstract =            {In this paper, we study model checking of timed
                         automata (TAs), and more precisely we aim at finding
                         efficient model checking for subclasses of TAs. For
                         this, we consider model checking TCTL and TCTL, over
                         TAs with one clock or two clocks.\par First we show
                         that the reachability problem is NLOGSPACE-complete
                         for one clock TAs (i.e. as complex as reachability
                         in classical graphs) and we give a polynomial time
                         algorithm for model checking TCTL, over this class
                         of TAs. Secondly we show that model checking becomes
                         PSPACE-complete for full TCTL over one clock TAs. We
                         also show that model checking CTL (without any
                         timing constraint) over two clock TAs is
                         PSPACE-complete and that reachability is NP-hard.},
}