Benedikt, Michael and Lenhardt, Rastislav and Worrell, James - Two Variable vs. Linear Temporal Logic in Model Checking and Games

lmcs:1103 - Logical Methods in Computer Science, May 23, 2013, Volume 9, Issue 2
Two Variable vs. Linear Temporal Logic in Model Checking and Games

Authors: Benedikt, Michael and Lenhardt, Rastislav and Worrell, James

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.


Source : oai:arXiv.org:1303.4533
DOI : 10.2168/LMCS-9(2:4)2013
Volume: Volume 9, Issue 2
Published on: May 23, 2013
Submitted on: August 17, 2012
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,F.4.1,F.4.3,F.1.1


Share

Consultation statistics

This page has been seen 93 times.
This article's PDF has been downloaded 30 times.