2011 | OriginalPaper | Chapter
Two Variable vs. Linear Temporal Logic in Model Checking and Games
Authors : Michael Benedikt, Rastislav Lenhardt, James Worrell
Published in: CONCUR 2011 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.