Specification and Verification using Temporal Logics

Stéphane Demri 1 Paul Gastin 1, 2
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : This chapter illustrates two aspects of automata theory related to linear-time temporal logic LTL used for the verification of computer systems. First, we present a translation from LTL formulae to Büchi automata. The aim is to design an elementary translation which is reasonably efficient and produces small automata so that it can be easily taught and used by hand on real examples. Our translation is in the spirit of the classical tableau constructions but is optimized in several ways. Secondly, we recall how temporal operators can be defined from regular languages and we explain why adding even a single operator definable by a context-free language can lead to undecidability.
Type de document :
Chapitre d'ouvrage
D'Souza, Deepak and Shankar, Priti. Modern applications of automata theory, 2, World Scientific, pp.457-494, 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00776601
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:41:08
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

  • HAL Id : hal-00776601, version 1

Collections

Citation

Stéphane Demri, Paul Gastin. Specification and Verification using Temporal Logics. D'Souza, Deepak and Shankar, Priti. Modern applications of automata theory, 2, World Scientific, pp.457-494, 2012. 〈hal-00776601〉

Partager

Métriques

Consultations de la notice

314