Timed modal logics for real-time systems

Patricia Bouyer; Franck Cassez; François Laroussinie

doi:10.1007/s10849-010-9127-4

Timed modal logics for real-time systems

Patricia Bouyer, Franck Cassez, François Laroussinie^*

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

7 Citations (Scopus)

Abstract

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.

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	https://doi.org/10.1007/s10849-010-9127-4
Publication status	Published - Apr 2011
Externally published	Yes

Keywords

model checking
timed automata
timed control
timed modal logic

Access to Document

10.1007/s10849-010-9127-4

Cite this

@article{e5481b44aa684d5d88711e6fefa492a4,

title = "Timed modal logics for real-time systems",

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.",

keywords = "model checking, timed automata, timed control, timed modal logic",

author = "Patricia Bouyer and Franck Cassez and Fran{\c c}ois Laroussinie",

year = "2011",

month = apr,

doi = "10.1007/s10849-010-9127-4",

language = "English",

volume = "20",

pages = "169--203",

journal = "Journal of Logic, Language and Information",

issn = "0925-8531",

publisher = "Springer, Springer Nature",

number = "2",

}

TY - JOUR

T1 - Timed modal logics for real-time systems

AU - Bouyer, Patricia

AU - Cassez, Franck

AU - Laroussinie, François

PY - 2011/4

Y1 - 2011/4

N2 - 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.

AB - 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.

KW - model checking

KW - timed automata

KW - timed control

KW - timed modal logic

UR - http://www.scopus.com/inward/record.url?scp=79952695122&partnerID=8YFLogxK

U2 - 10.1007/s10849-010-9127-4

DO - 10.1007/s10849-010-9127-4

M3 - Article

AN - SCOPUS:79952695122

SN - 0925-8531

VL - 20

SP - 169

EP - 203

JO - Journal of Logic, Language and Information

JF - Journal of Logic, Language and Information

IS - 2

ER -

Timed modal logics for real-time systems

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this