Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Book sections

Specification and Verification using Temporal Logics

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.
Document type :
Book sections
Complete list of metadata
Contributor : Benedikt Bollig Connect in order to contact the contributor
Submitted on : Tuesday, April 6, 2021 - 12:45:29 PM
Last modification on : Saturday, June 25, 2022 - 9:15:32 PM
Long-term archiving on: : Wednesday, July 7, 2021 - 6:33:46 PM


Files produced by the author(s)



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, ⟨10.1142/7237⟩. ⟨hal-00776601⟩



Record views


Files downloads