Nicolas Markey

Résumé

This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).

@incollection{hmc2018-BFLMOW,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {Model Checking Real-Time Systems},
  editor =              {Clarke, Edmund M. and Henzinger, Thomas A. and
                         Veith, Helmut and Bloem, Roderick},
  booktitle =           {Handbook of Model Checking},
  publisher =           {Springer-Verlag},
  pages =               {1001-1046},
  chapter =             {29},
  year =                {2018},
  month =               may,
  doi =                 {10.1007/978-3-319-10575-8_29},
  abstract =            {This chapter surveys timed automata as a formalism
                         for model checking real-time systems. We begin with
                         introducing the model, as an extension of
                         finite-state automata with real-valued variables for
                         measuring time. We then present the main
                         model-checking results in this framework, and give a
                         hint about some recent extensions (namely weighted
                         timed automata and timed games).},
}