Verification of two-variable logic revisited

Journal article

Two-variable logic (FO2) is a fragment of first-order logic that allows for decidable verification problems. In previous work [2], we developed an approach to FO2 verification that is particularly useful for probabilistic systems, based on analysis of the translation of FO2 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 [2] starting with FO2 without the successor relation. Making use of recent results by Weis [10] 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 2 from [2] by bootstrapping results for FO2 without successor. 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 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. © 2012 IEEE.

Authors: Benedikt, M; Lenhardt, R; Worrell, J

• Journal: Proceedings - 2012 9th International Conference on Quantitative Evaluation of Systems, QEST 2012
• Pages: 114-123
• Publication date: 2012-01-01
• DOI: 10.1109/QEST.2012.38
• Language: English
• Keywords: two variable logic; probabilistic model checking; verification