An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata

Salomon Sickert, Javier Esparza

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form nu=1 GF† v FGψi, where † and ψ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

Original languageEnglish
Title of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
PublisherAssociation for Computing Machinery
Pages831-844
Number of pages14
ISBN (Electronic)9781450371049
DOIs
StatePublished - 8 Jul 2020
Event35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany
Duration: 8 Jul 202011 Jul 2020

Publication series

NameACM International Conference Proceeding Series

Conference

Conference35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Country/TerritoryGermany
CitySaarbrucken
Period8/07/2011/07/20

Keywords

  • Deterministic Automata
  • Linear Temporal Logic
  • Normal Form
  • Weak Alternating Automata

Fingerprint

Dive into the research topics of 'An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata'. Together they form a unique fingerprint.

Cite this