Timed modal logics for real-time systems

Patricia Bouyer, Franck Cassez, François Laroussinie*

*Corresponding author for this work

Research output: Contribution to journalArticle

5 Citations (Scopus)

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

Keywords

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

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

  • Cite this