Two variable vs. linear temporal logic in model checking and games

DOI10.1007/978-3-642-23217-6_33zbMATH Open1343.68151arXiv1303.4533OpenAlexW1506717375MaRDI QIDQ3090852FDOQ3090852

Authors: Michael Benedikt, Rastislav Lenhardt, James Worrell 

Publication date: 2 September 2011

Published in: CONCUR 2011 – Concurrency Theory (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1303.4533

Recommendations

• Two variable vs. linear temporal logic in model checking and games
• First-order logic with two variables and unary temporal logic
• scientific article; zbMATH DE number 1775408
• On logics with two variables
• Alternating-time temporal logic

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Applications of game theory (91A80) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• The complexity of probabilistic verification
• The complexity of propositional linear temporal logics
• A survey of stochastic \(\omega \)-regular games
• Title not available (Why is that?)
• On the Complexity of Ltl Model-Checking of Recursive State Machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• Playing games with boxes and diamonds.
• Title not available (Why is that?)
• STACS 2005
• First-order logic with two variables and unary temporal logic
• An optimal automata approach to LTL model checking of probabilistic systems
• Title not available (Why is that?)
• Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

Cited In (5)

• Two variable vs. linear temporal logic in model checking and games
• Complexity of two-variable logic on finite trees
• First-order logic with two variables and unary temporal logic
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• A fragment of linear temporal logic for universal very weak automata

This page was built for publication: Two variable vs. linear temporal logic in model checking and games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3090852)