Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool duggi and discuss experimental results that compare the automata sizes and c…
Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $ω$-automata and then applying model checking. We revisit Vardi's transformation of an LTL formula to an alternating $ω$-automaton and Wolper's LTL tableau method for satisfiability checking. We observe that both constructions effectively rely on a decomposition of formulae into linear factors. Linear factors have been introduced previously by Antimirov in the context of regular expressions. W…
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these compo…
Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can …
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL …
In this paper, we consider the problem of translating LTL formulas to Buechi 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). Surprisingly, if the given formula is Until-free or Release-free, the Buechi automaton can be obtained directly in this manner. For a general formula, the construction is slightly involved: an a…
We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known a…
We present a new algorithm to construct a deterministic Rabin automaton for an LTL formula $φ$. The automaton is the product of a master automaton and an array of slave automata, one for each $G$-subformula of $φ$. The slave automaton for $Gψ$ is in charge of recognizing whether $FGψ$ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows to apply various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compa…
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW co…
When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Büchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic ω-automata with no determinization procedure involved. Since our approach is tailored to LTL, w…
In this paper we introduce a weighted LTL over product $ω$-valuation monoids that satisfy specific properties. We also introduce weighted generalized Büchi automata with $\varepsilon$-transitions, as well as weighted Büchi automata with $\varepsilon$-transitions over product $ω$-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted Büchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized Büchi automaton with $\varepsilon$-t…
The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL m…
Translating formulas of Linear Temporal Logic (LTL) over finite traces, or LTLf, to symbolic Deterministic Finite Automata (DFA) plays an important role not only in LTLf synthesis, but also in synthesis for Safety LTL formulas. The translation is enabled by using MONA, a powerful tool for symbolic, BDD-based, DFA construction from logic specifications. Recent works used a first-order encoding of LTLf formulas to translate LTLf to First Order Logic (FOL), which is then fed to MONA to get the symbolic DFA. This encoding was shown to perform well, but other encodings have not been studied. Specif…
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 $ω$-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 consist…
This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of the given formula. Finite LTL differs from traditional LTL in that formulas are interpreted with respect to finite, rather than infinite, sequences of states; this fact means that traditional finite-state automata, rather than ω-automata such as those developed by Büchi and others, suffice for recognizing models of such formulas. The approach considered is based on well-known tableau-construction techniques developed …
Transforming deterministic $ω$-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art…
In this paper we give automata-based representation of LTL-FO$^+$ properties. LTL-FO$^+$ is an extension of LTL that includes first-order quantification over bounded variable, thus greatly increasing the expressivity of the language. An automata representation of this formalism allows greater ease in writing and understanding properties, as well as in performing manipulations, such as negation or emptiness checking. The automata representation of an LTL-FO$^+$ formula has finite size regardless of the domain of quantified variables, and the number of states that is linear in the size of the pr…
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} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$, where $φ_i$ and $ψ_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 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 a…
We present a direct transformation of weak alternating $ω$-automata into equivalent backward deterministic $ω$-automata and show (1) how it can be used to obtain a transformation of non-deterministic Büchi automata into equivalent backward deterministic automata and (2) that it yields optimal equivalent backward deterministic automata when applied to linear-time temporal logic formulas. (1) uses the alternation-free fragment of the linear-time $μ$-calculus as an intermediate step; (2) is based on the straightforward translation of linear-time temporal logic into weak alternating $ω$-automata.
We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Buechi automata studied in this context and we indicate possible applications.
This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary %fairness assumptions ones. Notably, by making use of some syntactic transformations, our algorithm avoids to construct corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach ex…
We study alternating good-for-games (GFG) automata, i.e., alternating automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we lift many results from nondeterministic parity GFG automata to alternating ones: a single exponential determinisation procedure, an Exptime upper bound to the GFGness problem, a PTime algorithm for the GFGness problem of weak automata, and…
To model real-world software systems, modelling paradigms should support a form of compositionality. In interface theory and model-based testing with inputs and outputs, conjunctive operators have been introduced: the behaviour allowed by composed specification s1 $\wedge$ s2 is the behaviour allowed by both partial models s1 and s2. The models at hand are non-deterministic interface automata, but the interaction between non-determinism and conjunction is not yet well understood. On the other hand, in the theory of alternating automata, conjunction and non-determinism are core aspects. Alterna…
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property spec…
We give a new version of fuzzy alternating $\mathrm{B\ddot{u}chi}$ automata over distributive lattices: weights are putting in every leaf node of run trees rather than along with edges from every node to its children. Such settings are great benefit to obtain complement just by taking dual operation and replacing each final weight with its complement. We prove that $L$-fuzzy nondeterministic $\mathrm{B\ddot{u}chi}$ automata have the same expressive power as $L$-fuzzy alternating $\mathrm{B\ddot{u}chi}$ ones. A direct construction (without related knowledge about $L$-fuzzy nondeterministic $\ma…
We study temporal logics and automata on multi-attributed data words. Recently, BD-LTL was introduced as a temporal logic on data words extending LTL by navigation along positions of single data values. As allowing for navigation wrt. tuples of data values renders the logic undecidable, we introduce ND-LTL, an extension of BD-LTL by a restricted form of tuple-navigation. While complete ND-LTL is still undecidable, the two natural fragments allowing for either future or past navigation along data values are shown to be Ackermann-hard, yet decidability is obtained by reduction to nested multi-co…
A word automaton recognizing a language $L$ is good for games (GFG) if its composition with any game with winning condition $L$ preserves the game's winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various other properties that are used in the literature for defining that a nondeterministic automaton is GFG, including "history-deterministic", "compliant with some letter game", "good for trees", and "good for composition with other automata". The equivalence of these properties has not been formally shown. We generalize all of these definitions…
In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.
For a given regular language of infinite trees, one can ask about the minimal number of priorities needed to recognize this language with a non-deterministic, alternating, or weak alternating parity automaton. These questions are known as, respectively, the non-deterministic, alternating, and weak Rabin-Mostowski index problems. Whether they can be answered effectively is a long-standing open problem, solved so far only for languages recognizable by deterministic automata (the alternating variant trivializes). We investigate a wider class of regular languages, recognizable by so-called game au…
An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the smallest universal ordered trees and hence it is quasi-polynomial, and only polynomial if the asymptotic number of priorities is logarithmic in the number of states. This is an exponential improvement on the translation of Kupferman and Vardi (2001) and a quasi-polynomial improvement on the translation of Boker and Lehtinen (2018). Any slightly better such translation would (if---like all presently known such transla…
We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over s-AFAs have linear complexity, which is in sharp contrast with the quadratic cost of intersection and union for non-alternating symbolic automata. Due to this succinctness, emptiness and equivalence checking are PSpace-hard. We introduce an algorithm for checking the equivalence of two s-AFAs based on bisimulation up to congruence. This algorithm allows us to exploit the power of SAT and SMT solvers t…
In this paper, we give a Nivat-like characterization for weighted alternating automata over commutative semirings (WAFA). To this purpose we prove that weighted alternating can be characterized as the concatenation of weighted finite tree automata (WFTA) and a specific class of tree homomorphism. We show that the class of series recognized by weighted alternating automata is closed under inverses of homomorphisms, but not under homomorphisms. We give a logical characterization of weighted alternating automata, which uses weighted MSO logic for trees. Finally we investigate the strong connectio…
We introduce a new class of automata on infinite trees called \emph{alternating nonzero automata}, which extends the class of non-deterministic nonzero automata. We reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain as a corollary algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.
$μ$-Calculus and automata on infinite trees are complementary ways of describing infinite tree languages. The correspondence between $μ$-Calculus and alternating tree automaton is used to solve the satisfiability and model checking problems by compiling the modal $μ$-Calculus formula into an alternating tree automata. Thus advocating an automaton model specially tailored for working with modal $μ$-Calculus. The advantage of the automaton model is its ability to deal with arbitrary branching in a much simpler way as compare to the one proposed by Janin and Walukiewicz. Both problems (i.e., mode…
We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we…
