Unambiguous and finitely ambiguous automata
Cas Widdershoven · Oxford University Research Archive (ORA) (University of Oxford) · 2022
This thesis is concerned with unambiguous and finitely ambiguous automata, with a focus on automata on infinite words. In particular, it is concerned with the model checking question, which asks whether the traces of a (stochastic and / or non-deterministic) system satisfy a property given by an automaton. By studying these automata through the lens of matrix semigroups and making use of their spectral properties, we show that the model checking question can be solved efficiently in several different settings. Our first result is an adaptation of Baier et al.’s method for model checking Markov chains against unambiguous Büchi automata. This method expresses the model checking problem as a system of linear equations, given by a product of the automaton and Markov chain combined with a normalising equation for each strongly connected component of this product. By replacing their combinatorial algorithm for computing normalisers with one based on linear algebra, we obtain a speedup in the (edge set) size of the automaton at the cost of a slowdown in the size of the Markov chain. Next we introduce a type of weighted automata called image-binary automata, generalising unambiguous automata. We show that these automata are closed efficiently under the standard Boolean operations, implying an efficient algorithm to check whether a given Q-weighted automaton is image-binary, and that they accept precisely the regular languages. We show that image-binary automata can be exponentially more succinct than deterministic automata, that an exponential blowup in the state size is sufficient and necessary for converting NFAs to image-binary automata, and that converting an image-binary automaton to an NFA may require a superpolynomial state size blowup. We then consider image-binary automata over infinite words, with a Büchi acceptance condition. We show that k-ambiguous Büchi automata can be translated to image-binary Büchi automata using a PSPACE transducer, and that the model checking question of Markov chains against image-binary Büchi automata can be done in NC using an adaptation of Baier et al.’s algorithm for UBAs. Combining these gives a PSPACE procedure for model checking k-ABAs against Markov chains, implying optimality of both the translation from k-ABAs to image-binary Büchi automata as well as the model checking procedure. Lastly, we consider model checking of branching processes against LTL formulas using an automata theoretic approach. Branching processes are a model exhibiting both stochastic and non-deterministic branching, generalising both Markov chains and Kripke-structures. We consider both the questions whether it’s almost surely the case that a branching process generates a tree all of whose branches are accepted by a given automaton, and whether this is almost never the case, as well as the question whether a branching process almost surely generates a finite tree. We consider specifications given in terms of deterministic parity automata, NBAs, co-NBAs (where a tree is accepted iff all of its branches are rejected by a given NBA), co-UBAs (where all branches have to be rejected by a given UBA), and finally, LTL formulas. In general, this paints a picture where the question whether a branching process almost surely generates an accepted tree is easier than the question whether it almost never generates an accepted tree. By using the spectral properties of unambiguous automata, we show that the question whether a branching process almost surely generates a tree all of whose branches are rejected by a UBA is in NC. Combining this with a PSPACE transduction from an LTL formula to a UBA, we obtain an optimal procedure to check whether a branching process almost surely generates a tree satisfying an LTL formula.