{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:09:58Z","timestamp":1762459798909},"reference-count":34,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,12,31]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler\u2013Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler\u2013Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\\textrm{FO}$ and (basic) modal logic $\\textrm{ML}$. We also present a version of the game for the modal $\\mu $-calculus $\\textrm{L}_\\mu $ and show that $\\textrm{FO}$ is also non-elementarily more succinct than $\\textrm{L}_\\mu $.<\/jats:p>","DOI":"10.1093\/logcom\/exz025","type":"journal-article","created":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T11:40:36Z","timestamp":1568288436000},"page":"1311-1344","source":"Crossref","is-referenced-by-count":9,"title":["Formula size games for modal logic and \u03bc-calculus"],"prefix":"10.1093","volume":"29","author":[{"given":"Lauri","family":"T Hella","sequence":"first","affiliation":[{"name":"Department of Computing Sciences, Tampere University, FI-33014, Tampere, Finland"}]},{"given":"Miikka","family":"S Vilander","sequence":"additional","affiliation":[{"name":"Department of Computing Sciences, Tampere University, FI-33014, Tampere, Finland"}]}],"member":"286","published-online":{"date-parts":[[2019,12,13]]},"reference":[{"key":"2020012603564496100_ref1","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/772062.772064","article-title":"An n! lower bound on formula size","volume":"4","author":"Adler","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020012603564496100_ref2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"2020012603564496100_ref3","doi-asserted-by":"crossref","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","article-title":"Chapter 12\u2014modal mu-calculi","volume-title":"Handbook of Modal Logic","author":"Bradfield","year":"2007"},{"key":"2020012603564496100_ref4","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1093\/jigpal\/jzu030","article-title":"On guarded transformation in the modal mu-calculus","volume":"23","author":"Bruse","year":"2015","journal-title":"Logic Journal of the IGPL"},{"key":"2020012603564496100_ref5","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1006\/inco.2001.2953","article-title":"First-order logic with two variables and unary temporal logic","volume":"179","author":"Etessami","year":"2002","journal-title":"Information and Computation"},{"key":"2020012603564496100_ref6","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1006\/inco.1999.2846","article-title":"An until hierarchy and other applications of an Ehrenfeucht-Fra\u00efss\u00e9 game for temporal logic","volume":"160","author":"Etessami","year":"2000","journal-title":"Information and Computation"},{"key":"2020012603564496100_ref7","first-page":"827","article-title":"Succinctness in subsystems of the spatial mu-calculus","volume-title":"Journal of Applied Logics - IfCoLoG Journal of Logics and their Applications","author":"Fern\u00e1ndez-Duque","year":"2018"},{"key":"2020012603564496100_ref8","first-page":"881","article-title":"Succinctness of epistemic languages","volume-title":"IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16\u201322, 2011","author":"French","year":"2011"},{"key":"2020012603564496100_ref9","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1016\/j.artint.2013.02.003","article-title":"On the succinctness of some modal logics","volume":"197","author":"French","year":"2013","journal-title":"Artificial Intelligence"},{"key":"2020012603564496100_ref10","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1093\/jigpal\/6.1.73","article-title":"Products of modal logics, part 1","volume":"6","author":"Gabbay","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"2020012603564496100_ref11","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1093\/jigpal\/8.2.165","article-title":"Products of modal logics. Part 2: relativised quantifiers in classical logic","volume":"8","author":"Gabbay","year":"2000","journal-title":"Logic Journal of the IGPL"},{"key":"2020012603564496100_ref12","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1021304426509","article-title":"Products of modal logics. Part 3: products of modal and temporal logics","volume":"72","author":"Gabbay","year":"2002","journal-title":"Studia Logica"},{"key":"2020012603564496100_ref13","first-page":"862","article-title":"The comparative linguistics of knowledge representation","volume-title":"Proceedings of the 14th International Joint Conference on Artificial Intelligence\u2014Volume 1, IJCAI\u201995","author":"Gogic","year":"1995"},{"key":"2020012603564496100_ref14","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-1(1:6)2005","article-title":"The succinctness of first-order logic on linear orders","volume":"1","author":"Grohe","year":"2005","journal-title":"Logical Methods in Computer Science"},{"key":"2020012603564496100_ref15","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1051\/ita:2004017","article-title":"Comparing the succinctness of monadic query languages over finite trees","volume":"38","author":"Grohe","year":"2004","journal-title":"RAIRO Theoretical Informatics and Applications"},{"key":"2020012603564496100_ref16","article-title":"Bounded game-theoretic semantics for modal mu-calculus","author":"Hella","year":"2017"},{"key":"2020012603564496100_ref17","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1515\/9781614516873.193","article-title":"The size of a formula as a measure of complexity","volume-title":"Logic Without Borders\u2014Essays on Set Theory, Model Theory, Philosophical Logic and Philosophy of Mathematics","author":"Hella","year":"2015"},{"key":"2020012603564496100_ref18","first-page":"401","article-title":"The succinctness of first-order logic over modal logic via a formula size game","volume-title":"Advances in Modal Logic 11, Budapest, Hungary, August 30\u2013September 2, 2016","author":"Hella","year":"2016"},{"key":"2020012603564496100_ref19","first-page":"112","article-title":"On proving lower bounds for circuit size","volume-title":"Proceedings of the Eighth Annual Structure in Complexity Theory Conference","author":"Karchmer","year":"1993"},{"key":"2020012603564496100_ref20","first-page":"293","article-title":"The modal mu-calculus: a survey","volume":"9","author":"Lenzi","year":"2005","journal-title":"Task Q"},{"key":"2020012603564496100_ref21","first-page":"137","article-title":"Complexity and succinctness of public announcement logic","volume-title":"5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8\u201312, 2006","author":"Lutz","year":"2006"},{"key":"2020012603564496100_ref22","first-page":"247","article-title":"Modal logic and the two-variable fragment","volume-title":"Computer Science Logic, Paris, France, September 10\u201313, 2001","author":"Lutz","year":"2001"},{"key":"2020012603564496100_ref23","first-page":"122","article-title":"Temporal logic with past is exponentially more succinct, concurrency column","volume":"79","author":"Markey","year":"2003","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"2020012603564496100_ref24","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5694-3","article-title":"Applied Logic Series","volume-title":"Multi-dimensional Modal Logic","author":"Marx","year":"1997"},{"key":"2020012603564496100_ref25","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1080\/11663081.2015.1050907","article-title":"Expressiveness and succinctness of a logic of robustness","volume":"25","author":"McCabe-Dansted","year":"2015","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2020012603564496100_ref26","first-page":"276","article-title":"Bisimulation invariance and finite models","volume-title":"Logic Colloquium\u201902","author":"Otto","year":"2006"},{"key":"2020012603564496100_ref27","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/BF02122698","article-title":"Applications of matrix methods to the theory of lower bounds in computational complexity","volume":"10","author":"Razborov","year":"1990","journal-title":"Combinatorica"},{"key":"2020012603564496100_ref28","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logics","volume":"32","author":"Sistla","year":"1985","journal-title":"Journal of the ACM"},{"key":"2020012603564496100_ref29","article-title":"The Complexity of Decision Problems in Automata Theory and Logic","author":"Stockmeyer","year":"1974"},{"key":"2020012603564496100_ref30","first-page":"341","article-title":"On the relative succinctness of modal logics with union, intersection and quantification","volume-title":"International conference on Autonomous Agents and Multi-Agent Systems, AAMAS\u201914, Paris, France, May 5\u20139, 2014","author":"van der Hoek","year":"2014"},{"key":"2020012603564496100_ref31","first-page":"323","article-title":"On the relative succinctness of two extensions by definitions of multimodal logic","volume-title":"How the World Computes\u2014Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 18\u201323, 2012","author":"van der Hoek","year":"2012"},{"key":"2020012603564496100_ref32","first-page":"139","article-title":"Some exponential lower bounds on formula-size in modal logic","volume-title":"Advances in Modal Logic 10, Groningen, The Netherlands, August 5\u20138, 2014","author":"van Ditmarsch","year":"2014"},{"key":"2020012603564496100_ref33","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1080\/11663081.2016.1144016","article-title":"The succinctness of the cover modality","volume":"25","author":"van Ditmarsch","year":"2015","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2020012603564496100_ref34","first-page":"110","article-title":"CTL$^{+}$ is exponentially more succinct than CTL","volume-title":"Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13\u201315, 1999","author":"Wilke","year":"1999"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1311\/32008427\/exz025.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1311\/32008427\/exz025.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T06:20:33Z","timestamp":1611123633000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/8\/1311\/5675042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":34,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2019,12,13]]},"published-print":{"date-parts":[[2019,12,31]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz025","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2019,12]]},"published":{"date-parts":[[2019,12]]}}}