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).
Handbook of Model Checking, Springer, 2018. 46 pages.
PDF
© 2018 Springer International Publishing AG.