Timed modal logics for real-time systems

Patricia Bouyer, Franck Cassez, François Laroussinie*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


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 languageEnglish
Pages (from-to)169-203
Number of pages35
JournalJournal of Logic, Language and Information
Issue number2
Publication statusPublished - Apr 2011
Externally publishedYes


  • model checking
  • timed automata
  • timed control
  • timed modal logic


Dive into the research topics of 'Timed modal logics for real-time systems'. Together they form a unique fingerprint.

Cite this