Timed Modal Logics for Real-Time Systems Specification Verification and Control

摘要

In this paper, a timed modal logic L_c is presented for the specification and verification of real-time systems. Several important results for L_c are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for L_c model checking. Finally we consider several control problems for which L_c can be used to check controllability.