{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T04:11:36Z","timestamp":1783051896077,"version":"3.54.6"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We study verification problems for history-constrained systems (HCS), a model of guarded computation that uses nested systems. An outer system describes the process architecture in which a sequence of actions represents the communication between sub-systems through a global bus. Actions are either permitted or blocked locally by guards; these guards read and decide based on the sequence of actions so far in the global bus.<\/jats:p>\n                  <jats:p>\n                    When HCS have both the outer systems and the local guard controllers modelled by finite automata, we show they have the same expressive power as regular languages and finite automata, but they are exponentially more succinct. We also analyse games on this model, representing the interaction between environment and controller, and show that solving such games is -complete, where the lower bound already holds for reachability\/safety games and the upper bound holds for any\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03c9<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -regular winning condition. Finally, we consider HCS with guards of greater expressive power, Vector Addition Systems with States (VASS). We show that with deterministic coverability-VASS guards the reachability problem is -complete, while with reachability-VASS the problem is undecidable.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_28","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:08Z","timestamp":1779033068000},"page":"541-558","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["History-Constrained Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6696-9023","authenticated-orcid":false,"given":"Louwe B.","family":"Kuijer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0394-1634","authenticated-orcid":false,"given":"David","family":"Purser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1653-4069","authenticated-orcid":false,"given":"Henry","family":"Sinclair-Banks","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5274-8190","authenticated-orcid":false,"given":"Patrick","family":"Totzke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45220-1_1","volume-title":"Computer Science Logic","author":"PA Abdulla","year":"2003","unstructured":"Abdulla, P.A., Bouajjani, A., d\u2019Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1\u201314. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45220-1_1"},{"issue":"2","key":"28_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"28_CR3","doi-asserted-by":"publisher","unstructured":"Austin, P., Bose, S., Mazzocchi, N., Totzke, P.: Temporal explorability games. In: International Conference on Concurrency Theory (CONCUR). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0348, pp. 7:1\u20137:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2025.7","DOI":"10.4230\/LIPIcs.CONCUR.2025.7"},{"key":"28_CR4","doi-asserted-by":"publisher","unstructured":"Austin, P., Bose, S., Totzke, P.: Parity games on temporal graphs. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). Lecture Notes in Computer Science, vol. 14574, pp. 79\u201398. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-57228-9_5","DOI":"10.1007\/978-3-031-57228-9_5"},{"issue":"1","key":"28_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1023\/A:1022407907596","volume":"12","author":"MH ter Beek","year":"2003","unstructured":"ter Beek, M.H., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Comput. Support. Cooper. Work (CSCW) 12(1), 21\u201369 (2003). https:\/\/doi.org\/10.1023\/A:1022407907596","journal-title":"Comput. Support. Cooper. Work (CSCW)"},{"key":"28_CR6","doi-asserted-by":"publisher","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.F.: Faster algorithms for mean-payoff games. Form. Methods Syst. Des. 38(2), 97\u2013118 (2011). https:\/\/doi.org\/10.1007\/s10703-010-0105-x","DOI":"10.1007\/s10703-010-0105-x"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. In: 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pp. 1229\u20131240 (2022)","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"28_CR8","unstructured":"Fijalkow, N., et al.: Games on graphs (2023)"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4","DOI":"10.1007\/3-540-36387-4"},{"key":"28_CR10","doi-asserted-by":"publisher","unstructured":"Holme, P., Saram\u00e4ki, J.: Temporal Network Theory. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-23495-9","DOI":"10.1007\/978-3-030-23495-9"},{"issue":"1","key":"28_CR11","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/568438.568455","volume":"32","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. ACM SIGACT News 32(1), 60\u201365 (2001)","journal-title":"ACM SIGACT News"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Jurdzinski, M., Sproston, J., Laroussinie, F.: Model checking probabilistic timed automata with one or two clocks. Log. Methods Comput. Sci. 4(3) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(3:12)2008","DOI":"10.2168\/LMCS-4(3:12)2008"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-02424-5_15","volume-title":"Applications and Theory of Petri Nets","author":"M K\u00f6hler-Bu\u00dfmeier","year":"2009","unstructured":"K\u00f6hler-Bu\u00dfmeier, M.: Hornets: nets within nets combined with net algebra. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 243\u2013262. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02424-5_15"},{"key":"28_CR14","doi-asserted-by":"publisher","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing, San Francisco, California, USA, 5\u20137 May 1982, pp. 267\u2013281. ACM (1982). https:\/\/doi.org\/10.1145\/800070.802201","DOI":"10.1145\/800070.802201"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Kuijer, L.B., Purser, D., Sinclair-Banks, H., Totzke, P.: History-constrained systems (2026). https:\/\/arxiv.org\/abs\/2602.18143","DOI":"10.1007\/978-3-032-26204-2_28"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"K\u00fcnnemann, M., Mazowiecki, F., Sch\u00fctze, L., Sinclair-Banks, H., Wegrzycki, K.: Coverability in VASS revisited: improving Rackoff\u2019s bounds to obtain conditional optimality. J. ACM 72(5), 33:1\u201333:27 (2025). https:\/\/doi.org\/10.1145\/3762178","DOI":"10.1145\/3762178"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"J Lambert","year":"1992","unstructured":"Lambert, J.: A structure to decide reachability in petri nets. Theor. Comput. Sci. 99(1), 79\u2013104 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90173-D","journal-title":"Theor. Comput. Sci."},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The reachability problem for petri nets is not primitive recursive. In: 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pp. 1241\u20131252 (2022)","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 56\u201367. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/LICS.2015.16","DOI":"10.1109\/LICS.2015.16"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, 24\u201327 June 2019, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785796","DOI":"10.1109\/LICS.2019.8785796"},{"key":"28_CR21","unstructured":"Lipton, R.: The Reachability Problem Requires Exponential Space. Department of Computer Science. Yale University 62 (1976)"},{"key":"28_CR22","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1989)"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Mayr, E.W.: An algorithm for the general petri net reachability problem. In: Proceedings of the 13th Annual ACM Symposium on Theory of Computing, Milwaukee, Wisconsin, USA, 11\u201313 May 1981, pp. 238\u2013246. ACM (1981). https:\/\/doi.org\/10.1145\/800076.802477","DOI":"10.1145\/800076.802477"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-319-24024-4_18","volume-title":"Algorithms, Probability, Networks, and Games","author":"O Michail","year":"2015","unstructured":"Michail, O.: An introduction to temporal graphs: an algorithmic perspective. In: Zaroliagis, C., Pantziou, G., Kontogiannis, S. (eds.) Algorithms, Probability, Networks, and Games. LNCS, vol. 9295, pp. 308\u2013343. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24024-4_18"},{"key":"28_CR25","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.\u00a092. Springer, Heidelberg (1980).https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"28_CR26","unstructured":"Minsky, M.L.: Computation. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"28_CR27","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Annual Symposium on Principles of Programming Languages, POPL \u201989, pp. 179\u2013190. Association for Computing Machinery (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"28_CR28","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, SFCS \u201977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2\u20133","key":"28_CR29","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"KVS Prasad","year":"1995","unstructured":"Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2\u20133), 285\u2013327 (1995). https:\/\/doi.org\/10.1016\/0167-6423(95)00017-8","journal-title":"Sci. Comput. Program."},{"key":"28_CR30","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"28_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970). https:\/\/doi.org\/10.1016\/S0022-0000(70)80006-X","journal-title":"J. Comput. Syst. Sci."},{"key":"28_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1007\/978-3-540-27755-2_23","volume-title":"Lectures on Concurrency and Petri Nets","author":"R Valk","year":"2004","unstructured":"Valk, R.: Object petri nets: using the nets-within-nets paradigm. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 819\u2013848. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_23"},{"issue":"1\u20132","key":"28_CR33","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:04:20Z","timestamp":1783015460000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}