{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:12:51Z","timestamp":1778497971985,"version":"3.51.4"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2013,5,23]],"date-time":"2013-05-23T00:00:00Z","timestamp":1369267200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/H017690\/1"],"award-info":[{"award-number":["EP\/H017690\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Model checking linear-time properties expressed in first-order logic has\nnon-elementary complexity, and thus various restricted logical languages are\nemployed. In this paper we consider two such restricted specification logics,\nlinear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is\nmore expressive but FO2 can be more succinct, and hence it is not clear which\nshould be easier to verify. We take a comprehensive look at the issue, giving a\ncomparison of verification problems for FO2, LTL, and various sublogics thereof\nacross a wide range of models. In particular, we look at unary temporal logic\n(UTL), a subset of LTL that is expressively equivalent to FO2; we also consider\nthe stutter-free fragment of FO2, obtained by omitting the successor relation,\nand the expressively equivalent fragment of UTL, obtained by omitting the next\nand previous connectives. We give three logic-to-automata translations which\ncan be used to give upper bounds for FO2 and UTL and various sublogics. We\napply these to get new bounds for both non-deterministic systems (hierarchical\nand recursive state machines, games) and for probabilistic systems (Markov\nchains, recursive Markov chains, and Markov decision processes). We couple\nthese with matching lower-bound arguments. Next, we look at combining FO2\nverification techniques with those for LTL. We present here a language that\nsubsumes both FO2 and LTL, and inherits the model checking properties of both\nlanguages. Our results give both a unified approach to understanding the\nbehaviour of FO2 and LTL, along with a nearly comprehensive picture of the\ncomplexity of verification for these logics and their sublogics.<\/jats:p>","DOI":"10.2168\/lmcs-9(2:4)2013","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:39:25Z","timestamp":1385732365000},"source":"Crossref","is-referenced-by-count":4,"title":["Two Variable vs. Linear Temporal Logic in Model Checking and Games"],"prefix":"10.46298","volume":"Volume 9, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":false,"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rastislav","family":"Lenhardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8151-2443","authenticated-orcid":false,"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2013,5,23]]},"reference":[{"key":"776:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1103\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1103\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:30Z","timestamp":1681243410000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,23]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-9(2:4)2013","relation":{"is-same-as":[{"id-type":"arxiv","id":"1303.4533","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1303.4533","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-04921-2_37","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,23]]},"article-number":"1103"}}