Two Variable vs. Linear Temporal Logic in Model Checking and Games

Verification tasks have non-elementary complexity for properties of linear traces specified in first-order logic, and thus various limited logical languages are employed. In this paper we consider two restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO

2

). LTL is more expressive, but FO

2

is often more succinct, and hence it is not clear which should be easier to verify. In this paper we take a comprehensive look at the issue, giving a comparison of verification problems for FO

2

, LTL, and the subset of LTL expressively equivalent to FO

2

, unary temporal logic (UTL). We give two logic-to-automata translations which can be used to give upper bounds for FO

2

and UTL; 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 this with lower-bound arguments for FO

2

and UTL. Our results give both a unified approach to understanding the behavior of FO

2

and UTL, along with a nearly comprehensive picture of the complexity of verification for these logics.