{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T09:18:19Z","timestamp":1765531099660,"version":"3.48.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T00:00:00Z","timestamp":1765238400000},"content-version":"vor","delay-in-days":8,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014988","name":"Institute of Science and Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100014988","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In this work, we present\n                    <jats:italic>hypernode automata<\/jats:italic>\n                    as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with\n                    <jats:italic>hypernode logic<\/jats:italic>\n                    formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic\u2019s declarative nature with automata\u2019s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system\u2019s executions, but not both.\n                  <\/jats:p>","DOI":"10.1007\/s00236-025-00509-8","type":"journal-article","created":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T06:30:57Z","timestamp":1765261857000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Hypernode automata"],"prefix":"10.1007","volume":"62","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[]},{"given":"Marek","family":"Chalupa","sequence":"additional","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Nickovic","sequence":"additional","affiliation":[]},{"given":"Ana","family":"Oliveira da Costa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,12,9]]},"reference":[{"key":"509_CR1","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification (CAV), pp. 694\u2013717 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"509_CR2","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Henzinger, T.A., Nickovic, D., Costa, A.O.: Hypernode automata. In: P\u00e9rez, G.A., Raskin, J. (eds.) 34th International Conference on Concurrency Theory (CONCUR), pp. 21\u201312116 (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.21","DOI":"10.4230\/LIPICS.CONCUR.2023.21"},{"key":"509_CR3","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Ferr\u00e8re, T., Henzinger, T.A., Nickovic, D., Oliveira da Costa, A.: Flavors of sequential information flow. In: Proc. of VMCAI 2022: the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 13182, pp. 1\u201319 (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_1","DOI":"10.1007\/978-3-030-94583-1_1"},{"key":"509_CR4","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: Enea, C., Lal, A. (eds.) Computer Aided Verification (CAV), pp. 309\u2013332 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"509_CR5","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS \u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999,Proceedings. Lecture Notes in Computer Science, pp. 193\u2013207 (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"509_CR6","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Asynchronous extensions of HyperLTL. In: 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201313 (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"509_CR7","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 243, pp. 27\u201312716 (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.27","DOI":"10.4230\/LIPIcs.CONCUR.2022.27"},{"key":"509_CR8","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Sheinvald, S.: Finite-word hyperlanguages. In: Proc. of LATA 2021: the 15th International Conference on Language and Automata Theory and Applications. Lecture Notes in Computer Science, vol. 12638, pp. 173\u2013186 (2021). https:\/\/doi.org\/10.1007\/978-3-030-68195-1","DOI":"10.1007\/978-3-030-68195-1"},{"key":"509_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(86)90088-5","volume":"48","author":"G Berry","year":"1986","unstructured":"Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theoret. Comput. Sci. 48, 117\u2013126 (1986)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"509_CR10","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983). https:\/\/doi.org\/10.1145\/322374.322380","journal-title":"J. ACM"},{"issue":"4","key":"509_CR11","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. Journal of the ACM 11(4), 481\u2013494 (1964)","journal-title":"Journal of the ACM"},{"issue":"6","key":"509_CR12","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"509_CR13","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Henzinger, T.A., Costa, A.: Monitoring extended hypernode logic. In: Kosmatov, N., Kov\u00e1cs, L. (eds.) Integrated Formal Methods, pp. 151\u2013171 (2024). https:\/\/doi.org\/10.1007\/978-3-031-76554-4_9","DOI":"10.1007\/978-3-031-76554-4_9"},{"key":"509_CR14","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., nchez, C.S.: Temporal logics for hyperproperties. In: Proc. of POST 2014: the Third International Conference on Principles of Security and Trust. Lecture Notes in Computer Science, vol. 8414, pp. 265\u2013284 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8","DOI":"10.1007\/978-3-642-54792-8"},{"key":"509_CR15","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: Proc. of LICS: the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 1\u201313 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"509_CR16","volume-title":"Automata Theory: An Algorithmic Approach","author":"J Esparza","year":"2023","unstructured":"Esparza, J., Blondin, M.: Automata Theory: An Algorithmic Approach. MIT Press, Cambridge, MA (2023)"},{"key":"509_CR17","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pp. 110\u2013121 (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"509_CR18","unstructured":"Furia, C.A.: A survey of multi-tape automata. CoRR abs\/1205.0178 (2012) arXiv:1205.0178"},{"issue":"POPL","key":"509_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434319","volume":"5","author":"JO Gutsfeld","year":"2021","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434319","journal-title":"Proc. ACM Program. Lang."},{"issue":"8","key":"509_CR20","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"509_CR21","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 273\u2013284 (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"509_CR22","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 273\u2013284 (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"509_CR23","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.tcs.2012.04.006","volume":"449","author":"OH Ibarra","year":"2012","unstructured":"Ibarra, O.H., Tr\u00e2n, N.Q.: On synchronized multi-tape and multi-head automata. Theor. Comput. Sci. 449, 74\u201384 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"509_CR24","doi-asserted-by":"publisher","unstructured":"Ibarra, O.H., Tr\u00e2n, N.Q.: On synchronized multitape and multihead automata. In: Holzer, M., Kutrib, M., Pighizzini, G. (eds.) Descriptional Complexity of Formal Systems - 13th International Workshop, DCFS 2011, Gie\u00dfen\/Limburg, Germany, July 25-27, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6808, pp. 184\u2013197 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22600-7_15","DOI":"10.1007\/978-3-642-22600-7_15"},{"key":"509_CR25","doi-asserted-by":"publisher","unstructured":"Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team Semantics for the Specification and Verification of Hyperproperties. In: Potapov, I., Spirakis, P., Worrell, J. (eds.) 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 117, pp. 10\u201311016 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2018.10","DOI":"10.4230\/LIPIcs.MFCS.2018.10"},{"key":"509_CR26","doi-asserted-by":"publisher","unstructured":"Morin, R.: Decompositions of asynchronous systems. In: Sangiorgi, D., Simone, R. (eds.) CONCUR \u201998: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1466, pp. 549\u2013564 (1998). https:\/\/doi.org\/10.1007\/BFB0055647","DOI":"10.1007\/BFB0055647"},{"key":"509_CR27","unstructured":"OpenMP. accessed 2025-06-23. https:\/\/www.openmp.org\/"},{"issue":"4","key":"509_CR28","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(4), 264\u2013268 (1946)","journal-title":"Bull. Am. Math. Soc."},{"key":"509_CR29","doi-asserted-by":"crossref","unstructured":"Samadi, M., Bastany, A., Hojjat, H.: Compositional learning for synchronous parallel automata. In: Boronat, A., Fraser, G. (eds.) Fundamental Approaches to Software Engineering, pp. 101\u2013121 (2025)","DOI":"10.1007\/978-3-031-90900-9_6"},{"key":"509_CR30","doi-asserted-by":"publisher","unstructured":"Stutz, F.: Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States. LIPIcs, vol. 263, pp. 32\u201313231 (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.32","DOI":"10.4230\/LIPICS.ECOOP.2023.32"},{"issue":"6","key":"509_CR31","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1145\/363347.363387","volume":"11","author":"K Thompson","year":"1968","unstructured":"Thompson, K.: Regular expression search algorithm. Commun. ACM 11(6), 419\u2013422 (1968). https:\/\/doi.org\/10.1145\/363347.363387","journal-title":"Commun. ACM"},{"key":"509_CR32","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Symposium on Principles of Programming Languages (POPL), pp. 250\u2013259 (1988). https:\/\/doi.org\/10.1145\/73560.73582","DOI":"10.1145\/73560.73582"},{"key":"509_CR33","unstructured":"Watson, B.W.: A taxonomy of finite automata construction algorithms (1993)"},{"issue":"8","key":"509_CR34","doi-asserted-by":"publisher","first-page":"1909","DOI":"10.1142\/S0129054111009112","volume":"22","author":"F Yu","year":"2011","unstructured":"Yu, F., Bultan, T., Ibarra, O.H.: Relational string verification using multi-track automata. Int. J. Found. Comput. Sci. 22(8), 1909\u20131924 (2011)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"2","key":"509_CR35","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1051\/ita\/1987210200991","volume":"21","author":"W Zielonka","year":"1987","unstructured":"Zielonka, W.: Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl. 21(2), 99\u2013135 (1987)","journal-title":"RAIRO Theor. Informatics Appl."},{"key":"509_CR36","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., pp. 29\u201343 (2003).https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00509-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00509-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00509-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T09:14:31Z","timestamp":1765530871000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00509-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["509"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00509-8","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"6 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 December 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776\/F85, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant VAMOS 101020093.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"43"}}