@article{20866,
  abstract     = {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.},
  author       = {Bartocci, Ezio and Chalupa, Marek and Henzinger, Thomas A and Nickovic, Dejan and Oliveira da Costa, Ana},
  issn         = {1432-0525},
  journal      = {Acta Informatica},
  number       = {4},
  publisher    = {Springer Nature},
  title        = {{Hypernode automata}},
  doi          = {10.1007/s00236-025-00509-8},
  volume       = {62},
  year         = {2025},
}

@article{20186,
  abstract     = {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.},
  author       = {Hsu, Tzu Han and Oliveira Da Costa, Ana A and Wintenberg, Andrew and Bartocci, Ezio and Bonakdarpour, Borzoo},
  issn         = {1432-0525},
  journal      = {Acta Informatica},
  number       = {3},
  publisher    = {Springer Nature},
  title        = {{Gray-box runtime enforcement of hyperproperties}},
  doi          = {10.1007/s00236-025-00502-1},
  volume       = {62},
  year         = {2025},
}

@article{10602,
  abstract     = {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.},
  author       = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian},
  issn         = {1432-0525},
  journal      = {Acta Informatica},
  keywords     = {computer networks and communications, information systems, software},
  pages        = {585--618},
  publisher    = {Springer Nature},
  title        = {{Index appearance record with preorders}},
  doi          = {10.1007/s00236-021-00412-y},
  volume       = {59},
  year         = {2022},
}