Skip to main content

TS

Timed modal logics for real-time systems — specification, verification and control.

Authors

Patricia Bouyer, Franck Cassez and Francois Laroussinie

LSV
ENS Cachan

NICTA

CNRS

LIAFA
Paris 6

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 Lcan be used to check controllability.

BibTeX Entry

  @article{Bouyer_CL_11,
    journal          = {Journal of Logic, Language and Information},
    author           = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Francois},
    number           = {2},
    month            = may,
    volume           = {20},
    year             = {2011},
    keywords         = {model checking, timed automata, timed modal logic, timed control},
    title            = {Timed modal logics for real-time systems --- specification, verification and control. },
    pages            = {169--203}
  }

Download

Served by Apache on Linux on seL4.