Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.

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.
Type de document :
Article dans une revue
Journal of Logic, Language and Computation, Springer, 2010
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00493638
Contributeur : Franck Cassez <>
Soumis le : lundi 21 juin 2010 - 06:00:08
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13
Document(s) archivé(s) le : mercredi 22 septembre 2010 - 17:53:01

Fichier

jlli-2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00493638, version 1

Collections

Citation

Patricia Bouyer, Franck Cassez, François Laroussinie. Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.. Journal of Logic, Language and Computation, Springer, 2010. 〈inria-00493638〉

Partager

Métriques

Consultations de la notice

135

Téléchargements de fichiers

73