  Model checking linear-time properties expressed in first-order logic has
non-elementary complexity, and thus various restricted logical languages are
employed. In this paper we consider two such restricted specification logics,
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 also consider
the stutter-free fragment of FO2, obtained by omitting the successor relation,
and the expressively equivalent fragment of UTL, obtained by omitting the next
and previous connectives. 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 both non-deterministic systems (hierarchical
and recursive state machines, games) and for probabilistic systems (Markov
chains, recursive Markov chains, and Markov decision processes). We couple
these with matching lower-bound arguments. Next, we look at combining FO2
verification techniques with those for LTL. We present here a language that
subsumes both FO2 and LTL, and inherits the model checking properties of both
languages. Our results give both a unified approach to understanding the
behaviour of FO2 and LTL, along with a nearly comprehensive picture of the
complexity of verification for these logics and their sublogics.
