[{"publication":"Acta Informatica","ec_funded":1,"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"article_number":"43","ddc":["000"],"file_date_updated":"2026-01-05T12:26:43Z","article_type":"original","publisher":"Springer Nature","volume":62,"article_processing_charge":"Yes (via OA deal)","date_created":"2025-12-29T12:07:12Z","OA_type":"hybrid","oa":1,"quality_controlled":"1","abstract":[{"lang":"eng","text":"In this work, we present hypernode automata 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 hypernode logic 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’s declarative nature with automata’s 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’s executions, but not both."}],"status":"public","month":"12","arxiv":1,"publication_status":"published","author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"first_name":"Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","first_name":"Ana","last_name":"Oliveira da Costa","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4"}],"citation":{"apa":"Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Hypernode automata. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>","ieee":"E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” <i>Acta Informatica</i>, vol. 62, no. 4. Springer Nature, 2025.","ama":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. <i>Acta Informatica</i>. 2025;62(4). doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","chicago":"Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>.","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025).","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>Acta Informatica</i>, vol. 62, no. 4, 43, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>."},"OA_place":"publisher","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"corr_author":"1","title":"Hypernode automata","type":"journal_article","oa_version":"Published Version","_id":"20866","intvolume":"        62","department":[{"_id":"ToHe"}],"issue":"4","language":[{"iso":"eng"}],"acknowledgement":"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. Open access funding provided by Institute of Science and Technology (IST Austria).","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"earlier_version","id":"14405","status":"public"}]},"scopus_import":"1","doi":"10.1007/s00236-025-00509-8","day":"09","year":"2025","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"arxiv":["2305.02836"]},"file":[{"access_level":"open_access","date_created":"2026-01-05T12:26:43Z","creator":"dernst","success":1,"file_id":"20944","relation":"main_file","date_updated":"2026-01-05T12:26:43Z","content_type":"application/pdf","checksum":"06ed45a1218ad8464818803ae2968aaf","file_name":"2025_ActaInformatica_Bartocci.pdf","file_size":7117003}],"date_published":"2025-12-09T00:00:00Z","date_updated":"2026-01-05T12:27:41Z"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","has_accepted_license":"1","scopus_import":"1","isi":1,"issue":"3","language":[{"iso":"eng"}],"acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","file":[{"success":1,"file_id":"20267","access_level":"open_access","date_created":"2025-09-02T05:53:47Z","creator":"dernst","content_type":"application/pdf","file_name":"2025_ActaInformatica_Hsu.pdf","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","file_size":6505049,"relation":"main_file","date_updated":"2025-09-02T05:53:47Z"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"external_id":{"isi":["001546115300001"]},"date_updated":"2025-09-30T14:20:11Z","date_published":"2025-09-01T00:00:00Z","doi":"10.1007/s00236-025-00502-1","year":"2025","day":"01","author":[{"first_name":"Tzu Han","last_name":"Hsu","full_name":"Hsu, Tzu Han"},{"full_name":"Oliveira Da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","last_name":"Oliveira Da Costa","first_name":"Ana A"},{"full_name":"Wintenberg, Andrew","last_name":"Wintenberg","first_name":"Andrew"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour","first_name":"Borzoo"}],"citation":{"ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025.","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>.","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30."},"publication_status":"published","corr_author":"1","OA_place":"publisher","project":[{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"}],"title":"Gray-box runtime enforcement of hyperproperties","_id":"20186","intvolume":"        62","department":[{"_id":"ToHe"}],"type":"journal_article","oa_version":"Published Version","article_processing_charge":"Yes (via OA deal)","volume":62,"date_created":"2025-08-17T22:01:36Z","oa":1,"PlanS_conform":"1","OA_type":"hybrid","quality_controlled":"1","ddc":["000"],"article_number":"30","file_date_updated":"2025-09-02T05:53:47Z","article_type":"original","publisher":"Springer Nature","abstract":[{"lang":"eng","text":"Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants."}],"status":"public","month":"09","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"publication":"Acta Informatica"},{"quality_controlled":"1","date_created":"2022-01-06T12:37:27Z","oa":1,"article_processing_charge":"Yes (via OA deal)","volume":59,"publisher":"Springer Nature","article_type":"original","file_date_updated":"2022-01-07T07:50:31Z","ddc":["000"],"page":"585-618","month":"10","status":"public","abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"publication":"Acta Informatica","scopus_import":"1","keyword":["computer networks and communications","information systems","software"],"has_accepted_license":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","language":[{"iso":"eng"}],"isi":1,"date_updated":"2025-04-15T06:53:08Z","date_published":"2022-10-01T00:00:00Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"file":[{"date_created":"2022-01-07T07:50:31Z","creator":"cchlebak","access_level":"open_access","file_id":"10603","success":1,"date_updated":"2022-01-07T07:50:31Z","relation":"main_file","file_size":1066082,"content_type":"application/pdf","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_name":"2021_ActaInfor_Křetínský.pdf"}],"external_id":{"isi":["000735765500001"]},"year":"2022","day":"01","doi":"10.1007/s00236-021-00412-y","title":"Index appearance record with preorders","project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"corr_author":"1","citation":{"mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>"},"publication_status":"published","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881"},{"first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"},{"first_name":"Clara","last_name":"Waldmann","full_name":"Waldmann, Clara"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"}],"intvolume":"        59","department":[{"_id":"KrCh"}],"_id":"10602","oa_version":"Published Version","type":"journal_article"}]