Search

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 $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, \psi_i $, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalization 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 direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata., Comment: Accepted in J. ACM. arXiv admin note: text overlap with arXiv:2304.08872, arXiv:2005.00472

In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} \psi$, where $\varphi$ and $\psi$ contain only past operators. Some years later, Chang, Manna, and Pnueli derived a similar normal form for LTL. Both normalization 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. In 2020, Sickert and Esparza presented a direct and purely syntactic normalization procedure for LTL yielding a normal form similar to the one by Chang, Manna, and Pnueli, with a single exponential blow-up, and applied it to the problem of constructing a succinct deterministic $\omega$-automaton for a given formula. However, their procedure had exponential time complexity in the best case. In particular, it does not perform better for formulas that are almost in normal form. In this paper we present an alternative normalization procedure based on a simple set of rewrite rules.

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions., Comment: accepted for publication in STTT

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