On the relationship between LTL normal forms and Büchi automata

Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, Kim Guldstrand Larsen

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review


In this paper, we revisit the problem of translating LTL formulas to Büchi automata. We first translate the given LTL formula into a special disjuctive-normal form (DNF). The formula will be part of the state, and its DNF normal form specifies the atomic properties that should hold immediately (labels of the transitions) and the formula that should hold afterwards (the corresponding successor state). If the given formula is Until-free or Release-free, the Büchi automaton can be obtained directly in this manner. For a general formula, the construction is more involved: an additional component will be needed for each formula that helps us to identify the set of accepting states. Notably, our construction is an on-the-fly construction, which starts with the given formula and explores successor states according to the normal forms. We implement our construction and compare the tool with SPOT [3]. The comparision results are very encouraging and show our construction is quite innovative.
Original languageEnglish
Title of host publicationTheories of Programming and Formal Methods : Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday
Publication date2013
ISBN (Print)978-3-642-39697-7
ISBN (Electronic)978-3-642-39698-4
Publication statusPublished - 2013
SeriesLecture Notes in Computer Science


  • Artificial intelligence
  • Computer science
  • Automata theory


Dive into the research topics of 'On the relationship between LTL normal forms and Büchi automata'. Together they form a unique fingerprint.

Cite this