Back to the Future: A Fresh Look at Linear Temporal Logic

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

1 Scopus citations

Abstract

This note tells the story of how I came to understand that my work with Křetínský and Sickert on translating LTL into ω -automata was deeply connected to a normal form for LTL, obtained 35 years ago by Lichtenstein, Pnueli and Zuck.

Original languageEnglish
Title of host publicationImplementation and Application of Automata - 25th International Conference, CIAA 2021, Proceedings
EditorsSebastian Maneth
PublisherSpringer Science and Business Media Deutschland GmbH
Pages3-13
Number of pages11
ISBN (Print)9783030791209
DOIs
StatePublished - 2021
Event25th International Conference on Implementation and Application of Automata, CIAA 2021 - Virtual, Online
Duration: 19 Jul 202122 Jul 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12803 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Implementation and Application of Automata, CIAA 2021
CityVirtual, Online
Period19/07/2122/07/21

Keywords

  • Formal verification
  • Linear Temporal Logic
  • ω -Automata

Fingerprint

Dive into the research topics of 'Back to the Future: A Fresh Look at Linear Temporal Logic'. Together they form a unique fingerprint.

Cite this