No description available.

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In the first part of this dissertation we consider two such restricted specification logics on words: linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is more expressive but FO2 can be more succinct, and hence it is not clear which should be easier to verify. We take a comprehensive look at the issue, giving a comparison of verification problems for FO2, LTL, and various sublogics thereof across a wide range of models. In particular, we look at unary temporal logic (UTL), a subset of LTL that is expressively equivalent to FO2. We give three logic-to-automata translations which can be used to give upper bounds for FO2 and UTL and various sublogics. We apply these to get new bounds for model checking both non-deterministic systems (hierarchical and recursive state machines, games) and for probabilistic systems (Markov chains, recursive Markov chains, and Markov decision processes). Our results give a unified approach to understanding the behaviour of FO2, LTL, and their sublogics. We further consider the problem of computing maximal probabilities for interval Markov chains (and recursive interval Markov chains, stochastic context-free grammars) to satisfy LTL specifications. Using again our automata constructions we describe an expectation-maximisation algorithm to solve this problem in practice. Our algorithm can be seen as a variant of the classical Baum-Welch algorithm on hidden Markov models. We also introduce a publicly available on-line tool Tulip to perform such analysis. Finally, we investigate the extension of our techniques from words to trees. We show that the parallel between the complexity of FO2 satisfiability on general and on restricted structures breaks down as we move from words to trees, since trees allow one to encode alternating exponential time computation.