{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:29Z","timestamp":1760202749512,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T00:00:00Z","timestamp":1532995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"crossref","award":["2015-04388"],"award-info":[{"award-number":["2015-04388"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council","award":["647289CODA"],"award-info":[{"award-number":["647289CODA"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,7,31]]},"abstract":"<jats:p>\n            We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game. Thus, the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators and on the meta-level, where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyze an\n            <jats:italic>unbounded<\/jats:italic>\n            and\n            <jats:italic>(ordinal) bounded<\/jats:italic>\n            GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that, in bounded GTS, truth of ATL formulae can always be determined in finite time, that is, without constructing infinite paths. We also introduce a nonequivalent\n            <jats:italic>finitely bounded<\/jats:italic>\n            semantics and argue that it is natural from both logical and game-theoretic perspectives.\n          <\/jats:p>","DOI":"10.1145\/3179998","type":"journal-article","created":{"date-parts":[[2018,9,4]],"date-time":"2018-09-04T12:37:30Z","timestamp":1536064650000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Game-Theoretic Semantics for Alternating-Time Temporal Logic"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0157-1644","authenticated-orcid":false,"given":"Valentin","family":"Goranko","sequence":"first","affiliation":[{"name":"Stockholm University, and University of Johannesburg (visiting professorship), Frescati, Stockholm Sweden"}]},{"given":"Antti","family":"Kuusisto","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"}]},{"given":"Raine","family":"R\u00f6nnholm","sequence":"additional","affiliation":[{"name":"University of Tampere, Finland"}]}],"member":"320","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"volume-title":"IJCAI\u201915","author":"Alechina Natasha","key":"e_1_2_1_1_1","unstructured":"Natasha Alechina , Nils Bulling , Brian Logan , and Hoang Nga Nguyen . 2015. On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic . In IJCAI\u201915 . AAAI Press , Palo Alto , California USA, 1494--1501. Natasha Alechina, Nils Bulling, Brian Logan, and Hoang Nga Nguyen. 2015. On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic. In IJCAI\u201915. AAAI Press, Palo Alto, California USA, 1494--1501."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq032"},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science, Ahmed Bouajjani and Wei-Ngan Chin (Eds.)","volume-title":"Proceedings of of ATVA\u201910","author":"Almagor Shaull","unstructured":"Shaull Almagor , Yoram Hirshfeld , and Orna Kupferman . 2010. Promptness in omega-regular automata . In Proceedings of of ATVA\u201910 , Lecture Notes in Computer Science, Ahmed Bouajjani and Wei-Ngan Chin (Eds.) , Vol. 6252 . Springer , Berlin , 22--36. Shaull Almagor, Yoram Hirshfeld, and Orna Kupferman. 2010. Promptness in omega-regular automata. In Proceedings of of ATVA\u201910, Lecture Notes in Computer Science, Ahmed Bouajjani and Wei-Ngan Chin (Eds.), Vol. 6252. Springer, Berlin, 22--36."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295659"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of AAMAS\u201916","author":"Aminof Benjamin","year":"2016","unstructured":"Benjamin Aminof , Vadim Malvone , Aniello Murano , and Sasha Rubin . 2016 . Graded strategy logic: Reasoning about uniqueness of Nash equilibria . In Proceedings of AAMAS\u201916 . IFAAMAS Publications, 698--706. Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. 2016. Graded strategy logic: Reasoning about uniqueness of Nash equilibria. In Proceedings of AAMAS\u201916. IFAAMAS Publications, 698--706."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of AAAI\u201915","author":"Cerm\u00e1k Petr","year":"2015","unstructured":"Petr Cerm\u00e1k , Alessio Lomuscio , and Aniello Murano . 2015 . Verifying and synthesising multi-agent systems against one-goal strategy logic specifications . In Proceedings of AAAI\u201915 , Blai Bonet and Sven Koenig (Eds.). AAAI Press , 2038--2044. Petr Cerm\u00e1k, Alessio Lomuscio, and Aniello Murano. 2015. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In Proceedings of AAAI\u201915, Blai Bonet and Sven Koenig (Eds.). AAAI Press, 2038--2044."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614432"},{"key":"e_1_2_1_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of CSL\u201909","author":"C\u00eerstea Corina","unstructured":"Corina C\u00eerstea , Clemens Kupke , and Dirk Pattinson . 2009. EXPTIME Tableaux for the coalgebraic -calculus . In Proceedings of CSL\u201909 , Lecture Notes in Computer Science , Vol. 5771 . Springer , Berlin , 179--193. Corina C\u00eerstea, Clemens Kupke, and Dirk Pattinson. 2009. EXPTIME Tableaux for the coalgebraic -calculus. In Proceedings of CSL\u201909, Lecture Notes in Computer Science, Vol. 5771. Springer, Berlin, 179--193."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxp004"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21949"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00355298"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Raul Andres Leal, and Yde Venema","author":"Fontaine Ga\u00eblle","year":"2010","unstructured":"Ga\u00eblle Fontaine , Raul Andres Leal, and Yde Venema . 2010 . Automata for coalgebras: An approach using predicate liftings. In Proceedings of ICALP\u201910, Lecture Notes in Computer Science , Vol. 6199 . Springer , Berlin, 381--392. Ga\u00eblle Fontaine, Raul Andres Leal, and Yde Venema. 2010. Automata for coalgebras: An approach using predicate liftings. In Proceedings of ICALP\u201910, Lecture Notes in Computer Science, Vol. 6199. Springer, Berlin, 381--392."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of AAMAS\u201916","author":"Goranko Valentin","year":"2016","unstructured":"Valentin Goranko , Antti Kuusisto , and Raine R\u00f6nnholm . 2016 . Game-theoretic semantics for alternating-time temporal logic . In Proceedings of AAMAS\u201916 . IFAAMAS Publications, 671--679. Valentin Goranko, Antti Kuusisto, and Raine R\u00f6nnholm. 2016. Game-theoretic semantics for alternating-time temporal logic. In Proceedings of AAMAS\u201916. IFAAMAS Publications, 671--679."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of TIME\u201917 (LIPIcs)","volume":"90","author":"Goranko Valentin","year":"2017","unstructured":"Valentin Goranko , Antti Kuusisto , and Raine R\u00f6nnholm . 2017 a. CTL with finitely bounded semantics . In Proceedings of TIME\u201917 (LIPIcs) , Vol. 90 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 14:1--14:19. Valentin Goranko, Antti Kuusisto, and Raine R\u00f6nnholm. 2017a. CTL with finitely bounded semantics. In Proceedings of TIME\u201917 (LIPIcs), Vol. 90. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 14:1--14:19."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of AAMAS\u201917","author":"Goranko Valentin","year":"2017","unstructured":"Valentin Goranko , Antti Kuusisto , and Raine R\u00f6nnholm . 2017 b. Game-theoretic semantics for ATL+ with applications to model checking . In Proceedings of AAMAS\u201917 . IFAAMAS Publications, 1277--1285. Valentin Goranko, Antti Kuusisto, and Raine R\u00f6nnholm. 2017b. Game-theoretic semantics for ATL+ with applications to model checking. In Proceedings of AAMAS\u201917. IFAAMAS Publications, 1277--1285."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Valentin Goranko Antti Kuusisto and Raine R\u00f6nnholm. 2018. Alternating-time temporal logic ATL with finitely bounded semantics. submitted.  Valentin Goranko Antti Kuusisto and Raine R\u00f6nnholm. 2018. Alternating-time temporal logic ATL with finitely bounded semantics. submitted.","DOI":"10.1016\/j.tcs.2019.05.029"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.043"},{"key":"e_1_2_1_19_1","unstructured":"Lauri Hella Antti Kuusisto and Raine R\u00f6nnholm. 2017. Bounded game-theoretic semantics for modal mu-calculus. CoRR abs\/1706.00753.  Lauri Hella Antti Kuusisto and Raine R\u00f6nnholm. 2017. Bounded game-theoretic semantics for modal mu-calculus. CoRR abs\/1706.00753."},{"volume-title":"Language-games and Information: Kantian Themes in the Philosophy of Logic","author":"Hintikka Jaakko","key":"e_1_2_1_20_1","unstructured":"Jaakko Hintikka . 1973. Logic , Language-games and Information: Kantian Themes in the Philosophy of Logic . Clarendon Press , Oxford . Jaakko Hintikka. 1973. Logic, Language-games and Information: Kantian Themes in the Philosophy of Logic. Clarendon Press, Oxford."},{"volume-title":"Logic, Methodology and Philosophy of Science VIII","author":"Hintikka Jaakko","key":"e_1_2_1_21_1","unstructured":"Jaakko Hintikka and Gabriel Sandu . 1989. Informational independence as a semantical phenomenon . In Logic, Methodology and Philosophy of Science VIII , J. E. Fenstad (Ed.). North-Holland , Amsterdam , 571--589. Jaakko Hintikka and Gabriel Sandu. 1989. Informational independence as a semantical phenomenon. In Logic, Methodology and Philosophy of Science VIII, J. E. Fenstad (Ed.). North-Holland, Amsterdam, 571--589."},{"volume-title":"Handbook of Logic and Language, J. van Benthem and A. ter Meulen (Eds.)","author":"Hintikka Jaakko","key":"e_1_2_1_22_1","unstructured":"Jaakko Hintikka and Gabriel Sandu . 1997. Game-theoretical semantics . In Handbook of Logic and Language, J. van Benthem and A. ter Meulen (Eds.) . Elsevier , Amsterdam , 361--410. Jaakko Hintikka and Gabriel Sandu. 1997. Game-theoretical semantics. In Handbook of Logic and Language, J. van Benthem and A. ter Meulen (Eds.). Elsevier, Amsterdam, 361--410."},{"key":"e_1_2_1_23_1","volume-title":"Vardi","author":"Kupferman Orna","year":"2007","unstructured":"Orna Kupferman , Nir Piterman , and Moshe Y . Vardi . 2007 . From liveness to promptness. Lecture Notes in Computer Science, Werner Damm and Holger Hermanns (Eds.). Vol. 4590 . Springer , Berlin, 406--419. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. 2007. From liveness to promptness. Lecture Notes in Computer Science, Werner Damm and Holger Hermanns (Eds.). Vol. 4590. Springer, Berlin, 406--419."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the Symposium on Foundations of Mathematics, Warsaw","author":"Lorenzen Paul","year":"1961","unstructured":"Paul Lorenzen . 1961 . Ein dialogisches Konstruktivit\u00e4tskriterium . In Proceedings of the Symposium on Foundations of Mathematics, Warsaw 1959, Andrzej Mostowski (Ed.). Panstwowe wydawnictwo naukowe, Warsaw, 193--200. Paul Lorenzen. 1961. Ein dialogisches Konstruktivit\u00e4tskriterium. In Proceedings of the Symposium on Foundations of Mathematics, Warsaw 1959, Andrzej Mostowski (Ed.). Panstwowe wydawnictwo naukowe, Warsaw, 193--200."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of AAMAS\u201914","author":"Mogavero Fabio","year":"2014","unstructured":"Fabio Mogavero , Aniello Murano , and Luigi Sauro . 2014 . Strategy games: A renewed framework . In Proceedings of AAMAS\u201914 , Ana L. C. Bazzan, Michael N. Huhns, Alessio Lomuscio, and Paul Scerri (Eds.). IFAAMAS\/ACM, 869--876. Fabio Mogavero, Aniello Murano, and Luigi Sauro. 2014. Strategy games: A renewed framework. In Proceedings of AAMAS\u201914, Ana L. C. Bazzan, Michael N. Huhns, Alessio Lomuscio, and Paul Scerri (Eds.). IFAAMAS\/ACM, 869--876."},{"key":"e_1_2_1_26_1","series-title":"Lecture Notes in Computer Science, Kenneth L","volume-title":"Proceedings of LPAR-19","author":"Mogavero Fabio","unstructured":"Fabio Mogavero , Aniello Murano , and Loredana Sorrentino . 2013. On promptness in parity games . In Proceedings of LPAR-19 , Lecture Notes in Computer Science, Kenneth L . McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.), Vol. 8312 . Springer , Berlin , 601--618. Fabio Mogavero, Aniello Murano, and Loredana Sorrentino. 2013. On promptness in parity games. In Proceedings of LPAR-19, Lecture Notes in Computer Science, Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.), Vol. 8312. Springer, Berlin, 601--618."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.10.017"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0021-9800(66)80005-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1148961.1709593"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3179998","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3179998","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:18Z","timestamp":1750208898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3179998"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,31]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,7,31]]}},"alternative-id":["10.1145\/3179998"],"URL":"https:\/\/doi.org\/10.1145\/3179998","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,7,31]]},"assertion":[{"value":"2017-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}