Verification of Two-Variable Logic Revisited

Two-variable logic is a fragment of first-order logic that allows for decidable verification problems. In previous work, we developed an approach to FO² verification that is particularly useful for probabilistic systems, based on analysis of the translation of FO² to automata. In this work we show that the techniques introduced there can be applied to give information on other logics, and can be used in conjunction with automata-theoretic techniques for Linear Temporal Logic (LTL) in the context of probabilistic verification. First we revisit the technique of our prior work starting with FO² without the successor relation. Making use of recent results by Weis we show here that we can get quite small automata for these formula. We then show that we can recapture the automata size bounds for general FO² formulas by bootstrapping results for FO² without successor. Next, we look at combining FO² verification techniques with those for LTL. We present here a language that subsumes both FO² and LTL, and inherits the model checking properties of both languages. Our automata translation gives new bounds on model-checking for this large language for non-deterministic systems, and is particularly useful for probabilistic systems: e.g Markov Chains, Recursive Markov Chains, and Markov Decision Processes.