English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Model checking linear-time properties expressed in first-order logic hasnon-elementary complexity, and thus various restricted logical languages areemployed. In this paper we consider two such restricted specification logics,linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL ismore expressive but FO2 can be more succinct, and hence it is not clear whichshould be easier to verify. We take a comprehensive look at the issue, giving acomparison of verification problems for FO2, LTL, and various sublogics thereofacross 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 considerthe stutter-free fragment of FO2, obtained by omitting the successor relation,and the expressively equivalent fragment of UTL, obtained by omitting the nextand previous connectives. We give three logic-to-automata translations whichcan be used to give upper bounds for FO2 and UTL and various sublogics. Weapply these to get new bounds for both non-deterministic systems (hierarchicaland recursive state machines, games) and for probabilistic systems (Markovchains, recursive Markov chains, and Markov decision processes). We couplethese with matching lower-bound arguments. Next, we look at combining FO2verification techniques with those for LTL. We present here a language thatsubsumes both FO2 and LTL, and inherits the model checking properties of bothlanguages. Our results give both a unified approach to understanding thebehaviour of FO2 and LTL, along with a nearly comprehensive picture of thecomplexity of verification for these logics and their sublogics.

Two Variable vs. Linear Temporal Logic in Model Checking and Games