{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:55Z","timestamp":1750220635628,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T00:00:00Z","timestamp":1619740800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,4,30]]},"abstract":"<jats:p>\n            We define and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic equilibria of multi-agent systems. We use\n            <jats:italic>iterated Boolean games<\/jats:italic>\n            as our abstract model of multi-agent systems\u00a0[Gutierrez et\u00a0al. 2013, 2015a]. In such a game, each agent\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            has a goal\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , represented using (a fragment of)\n            <jats:bold>\n              Linear Temporal Logic (\n              <jats:inline-formula>\n                <jats:alternatives>\n                  <jats:tex-math>\n                    \n                  <\/jats:tex-math>\n                <\/jats:alternatives>\n              <\/jats:inline-formula>\n              )\n            <\/jats:bold>\n            . The goal\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            captures agent\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            \u2019s preferences, in the sense that the models of\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            represent system behaviours that would satisfy\u00a0\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            . Each player controls a subset of Boolean variables\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , and at each round in the game, player\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            is at liberty to choose values for variables\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            in any way that she sees fit. Play continues for an infinite sequence of rounds, and so as players act they collectively trace out a model for\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , which for every player will either satisfy or fail to satisfy their goal. Players are assumed to act strategically, taking into account the goals of other players, in an attempt to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of (pure) Nash equilibria. The (possibly empty) set of Nash equilibria of an iterated Boolean game can be understood as inducing a set of computations, each computation representing one way the system could evolve if players chose strategies that together constitute a Nash equilibrium. Such a set of equilibrium computations expresses a temporal property\u2014which may or may not be expressible within a particular\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            fragment. The new notion of expressiveness that we formally define and investigate is then as follows:\n            <jats:italic>\n              What temporal properties are characterised by the Nash equilibria of games in which agent goals are expressed in specific fragments of\u00a0\n              <jats:inline-formula>\n                <jats:alternatives>\n                  <jats:tex-math>\n                    \n                  <\/jats:tex-math>\n                <\/jats:alternatives>\n              <\/jats:inline-formula>\n            <\/jats:italic>\n            ? We formally define and investigate this notion of expressiveness for a range of\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            fragments. For example, a very natural question is the following:\n            <jats:italic>\n              Suppose we have an iterated Boolean game in which every goal is represented using a particular fragment\n              <jats:inline-formula>\n                <jats:alternatives>\n                  <jats:tex-math>\n                    \n                  <\/jats:tex-math>\n                <\/jats:alternatives>\n              <\/jats:inline-formula>\n              of\n              <jats:inline-formula>\n                <jats:alternatives>\n                  <jats:tex-math>\n                    \n                  <\/jats:tex-math>\n                <\/jats:alternatives>\n              <\/jats:inline-formula>\n              : is it then always the case that the equilibria of the game can be characterised within\n              <jats:inline-formula>\n                <jats:alternatives>\n                  <jats:tex-math>\n                    \n                  <\/jats:tex-math>\n                <\/jats:alternatives>\n              <\/jats:inline-formula>\n              ?\n            <\/jats:italic>\n            We show that this is not true in general.\n          <\/jats:p>","DOI":"10.1145\/3439900","type":"journal-article","created":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T21:14:08Z","timestamp":1623186848000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Expressiveness and Nash Equilibrium in Iterated Boolean Games"],"prefix":"10.1145","volume":"22","author":[{"given":"Julian","family":"Gutierrez","sequence":"first","affiliation":[{"name":"Monash University, Melbourne, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Harrenstein","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8687-6323","authenticated-orcid":false,"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[{"name":"Sapienza University of Rome, Rome, Italy, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2171725"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1373322"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1385-7258(53)50042-3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1567016.1567077"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9110-4"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 30th Symposium on the Mathematical Foundations of Computer Science (MFCS\u201903)","volume":"2747","author":"\u010cerna I.","unstructured":"I. \u010cerna and R. Pel\u00e1nek . 2003. Relating hierarchy of temporal properties to model checking . In Proceedings of the 30th Symposium on the Mathematical Foundations of Computer Science (MFCS\u201903) (Lecture Notes in Computer Science (LNCS)) , vol. 2747 ,B. Rovan and Peter Vojt\u00e1\u0161 (Eds.). Springer-Verlag, 318\u2013327. I. \u010cerna and R. Pel\u00e1nek. 2003. Relating hierarchy of temporal properties to model checking. In Proceedings of the 30th Symposium on the Mathematical Foundations of Computer Science (MFCS\u201903) (Lecture Notes in Computer Science (LNCS)), vol. 2747,B. Rovan and Peter Vojt\u00e1\u0161 (Eds.). Springer-Verlag, 318\u2013327."},{"key":"e_1_2_1_9_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"73","author":"Chang C. C.","unstructured":"C. C. Chang and H. J. Keisler . 1990. Model Theory (3rd ed.) . Studies in Logic and the Foundations of Mathematics , vol. 73 . North-Holland Publishing Company. C. C. Chang and H. J. Keisler. 1990. Model Theory (3rd ed.). Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland Publishing Company."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646246.684871"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.07.004"},{"key":"e_1_2_1_12_1","unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 2000. Model Checking. The MIT Press Cambridge MA.  E. M. Clarke O. Grumberg and D. A. Peled. 2000. Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(93)90005-H"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-9906-9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/3092772"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3094"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/114891.114907"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2030470.2030482"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00113-7"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1807662.1807687"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2540128.2540252"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2936924.2937028"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2540128.2540263"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/3031929.3031979"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the CONCUR\u201915 (LIPIcs)","volume":"42","author":"Gutierrez J.","unstructured":"J. Gutierrez , P. Harrenstein , and M. Wooldridge . 2015b. Expressiveness and complexity results for strategic reasoning . In Proceedings of the CONCUR\u201915 (LIPIcs) , vol. 42 . Schloss Dagstuhl, 268\u2013282. J. Gutierrez, P. Harrenstein, and M. Wooldridge. 2015b. Expressiveness and complexity results for strategic reasoning. In Proceedings of the CONCUR\u201915 (LIPIcs), vol. 42. Schloss Dagstuhl, 268\u2013282."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.03.011"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.10.009"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091225"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S175502030999013X"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1028128.1028159"},{"volume-title":"Model Theory. Encyclopedia of Mathematics and its Applications","author":"Hodges W.","key":"e_1_2_1_33_1","unstructured":"W. Hodges . 1993. Model Theory. Encyclopedia of Mathematics and its Applications , vol. 42 . Cambridge University Press . W. Hodges. 1993. Model Theory. Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160665"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.103170"},{"volume-title":"Handbook of Model Checking, Edmund M","author":"Kupferman O.","key":"e_1_2_1_36_1","unstructured":"O. Kupferman . 2018. Automata theory and model checking . In Handbook of Model Checking, Edmund M . Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer-Verlag , 107\u2013151. O. Kupferman. 2018. Automata theory and model checking. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer-Verlag, 107\u2013151."},{"key":"e_1_2_1_37_1","first-page":"7","article-title":"The stuttering principle revisited","volume":"41","author":"Ku\u010dera A.","year":"2005","unstructured":"A. Ku\u010dera and J. Strej\u010dek . 2005 . The stuttering principle revisited . Acta Informatica 41 , 7 \u2013 8 (2005), 415\u2013434. A. Ku\u010dera and J. Strej\u010dek. 2005. The stuttering principle revisited. Acta Informatica 41, 7\u20138 (2005), 415\u2013434.","journal-title":"Acta Informatica"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 9th IFIP Congress on Information Processing, R. E. A. Mason (Ed.). North-Holland, 657\u2013667","author":"Lamport L.","year":"1983","unstructured":"L. Lamport . 1983 . What good is temporal logic? In Information Processing \u201983 : Proceedings of the 9th IFIP Congress on Information Processing, R. E. A. Mason (Ed.). North-Holland, 657\u2013667 . L. Lamport. 1983. What good is temporal logic? In Information Processing \u201983: Proceedings of the 9th IFIP Congress on Information Processing, R. E. A. Mason (Ed.). North-Holland, 657\u2013667."},{"key":"e_1_2_1_39_1","series-title":"IISc Research Monographs Series","volume-title":"Modern Applications of Automata Theory, D. D\u2019Souza and P Shankar (Eds.)","author":"L\u00f6ding Christof","unstructured":"Christof L\u00f6ding . 2012. Basics on tree automata . In Modern Applications of Automata Theory, D. D\u2019Souza and P Shankar (Eds.) . IISc Research Monographs Series , Vol. 2 . World Scientific , 79\u2013110. Christof L\u00f6ding. 2012. Basics on tree automata. In Modern Applications of Automata Theory, D. D\u2019Souza and P Shankar (Eds.). IISc Research Monographs Series, Vol. 2. World Scientific, 79\u2013110."},{"key":"e_1_2_1_40_1","unstructured":"R. D. Luce and H. Raiffa. 1957. Games and Decisions. John Wiley & Sons.  R. D. Luce and H. Raiffa. 1957. Games and Decisions. John Wiley & Sons."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93442"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"M. Maschler E. Solan and S. Zamir. 2013. Game Theory. Cambridge U.P.  M. Maschler E. Solan and S. Zamir. 2013. Game Theory. Cambridge U.P.","DOI":"10.1017\/CBO9780511794216"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/267846.267847"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/646513.695664"},{"key":"e_1_2_1_45_1","unstructured":"M. J. Osborne and A. Rubinstein. 1994. A Course in Game Theory. The MIT Press Cambridge MA.  M. J. Osborne and A. Rubinstein. 1994. A Course in Game Theory. The MIT Press Cambridge MA."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00225-3"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00133-6"},{"volume-title":"Epistemic Game Theory: Reasoning and Choice","author":"Perea A.","key":"e_1_2_1_48_1","unstructured":"A. Perea . 2012. Epistemic Game Theory: Reasoning and Choice . Cambridge University Press , U.K. A. Perea. 2012. Epistemic Game Theory: Reasoning and Choice. Cambridge University Press, U.K."},{"key":"e_1_2_1_49_1","volume-title":"Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics","author":"Perrin D.","year":"2004","unstructured":"D. Perrin and J-\u00c9. Pin. 2004 . Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics , Vol. 141 . Elsevier Academic Press . D. Perrin and J-\u00c9. Pin. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics, Vol. 141. Elsevier Academic Press."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/646737.701932"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1483085"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/543812.543837"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/267871.267878"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/239519.239527"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694478"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_60_1","unstructured":"Y. Wang and F. Dechesne. 2009. On expressive power and class invariance. https:\/\/arxiv.org\/abs\/0905.4332 (2009).  Y. Wang and F. Dechesne. 2009. On expressive power and class invariance. https:\/\/arxiv.org\/abs\/0905.4332 (2009)."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3439900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3439900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:53Z","timestamp":1750197713000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3439900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4,30]]}},"alternative-id":["10.1145\/3439900"],"URL":"https:\/\/doi.org\/10.1145\/3439900","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,4,30]]},"assertion":[{"value":"2020-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}