On the Translation of Automata to Linear Temporal Logic
| Autor: | Udi Boker, Karoliina Lehtinen, Salomon Sickert |
|---|---|
| Přispěvatelé: | Modélisation et Vérification (MOVE), Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Aix Marseille Université (AMU) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Formal Languages and Automata Theory (cs.FL) Computer Science::Logic in Computer Science [INFO]Computer Science [cs] Computer Science - Formal Languages and Automata Theory Computer Science::Digital Libraries Computer Science::Formal Languages and Automata Theory Logic in Computer Science (cs.LO) |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030992521 FOSSACS FOSSACS, Apr 2022, Munich, Germany. pp.140-160, ⟨10.1007/978-3-030-99253-8_8⟩ |
| DOI: | 10.1007/978-3-030-99253-8_8⟩ |
| Popis: | While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $\omega$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic $\omega$-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a looping, weak, B\"uchi, coB\"uchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words). Comment: Full version with appendix of a chapter with the same title that appears in the FoSSaCS 2022 conference proceedings |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|