@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}, } @article{1351, abstract = {The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.}, author = {Giacobbe, Mirco and Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Paixao, Tiago and Petrov, Tatjana}, issn = {0001-5903}, journal = {Acta Informatica}, number = {8}, pages = {765 -- 787}, publisher = {Springer}, title = {{Model checking the evolution of gene regulatory networks}}, doi = {10.1007/s00236-016-0278-x}, volume = {54}, year = {2017}, } @article{719, abstract = {The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains.}, author = {Chatterjee, Krishnendu and Ehlers, Rüdiger}, issn = {0001-5903}, journal = {Acta Informatica}, number = {6}, pages = {543 -- 544}, publisher = {Springer}, title = {{Special issue: Synthesis and SYNT 2014}}, doi = {10.1007/s00236-017-0299-0}, volume = {54}, year = {2017}, }