Two variable vs. linear temporal logic in model checking and games
From MaRDI portal
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)
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1335875 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1500523 (Why is no real title available?)
- scientific article; zbMATH DE number 1786477 (Why is no real title available?)
- A survey of stochastic -regular games
- An optimal automata approach to LTL model checking of probabilistic systems
- First-order logic with two variables and unary temporal logic
- On the Complexity of Ltl Model-Checking of Recursive State Machines
- Playing games with boxes and diamonds.
- STACS 2005
- Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
- The complexity of probabilistic verification
- The complexity of propositional linear temporal logics
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)
