Abstract
In this paper, a timed modal logic Lc is presented for the specification and verification of real-time systems. Several important results for Lc 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 Lc model checking. Finally we consider several control problems for which Lc can be used to check controllability.
Original language | English |
---|---|
Pages (from-to) | 169-203 |
Number of pages | 35 |
Journal | Journal of Logic, Language and Information |
Volume | 20 |
Issue number | 2 |
DOIs | |
Publication status | Published - Apr 2011 |
Externally published | Yes |
Keywords
- model checking
- timed automata
- timed control
- timed modal logic