@inproceedings{22006,
  abstract     = {Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.},
  author       = {Chalupa, Marek and Henzinger, Thomas A and Sarac, Naci E and Yu, Zhengqi},
  booktitle    = {27th International Symposium on Formal Methods},
  isbn         = {9783032262196},
  issn         = {1611-3349},
  keywords     = {Signal first-order logic, Robustness-based quantitative semantics, Online runtime monitoring},
  location     = {Tokyo, Japan},
  pages        = {214--233},
  publisher    = {Springer Nature},
  title        = {{Quantitative monitoring of Signal First-Order logic}},
  doi          = {10.1007/978-3-032-26220-2_11},
  volume       = {16557},
  year         = {2026},
}

@article{21012,
  abstract     = {In certifiable machine learning, AI systems produce not only results but also verifiable certificates that the results can be trusted.},
  author       = {Barrett, Clark and Henzinger, Thomas A and Seshia, Sanjit A.},
  issn         = {1557-7317},
  journal      = {Communications of the ACM},
  number       = {1},
  pages        = {66--75},
  publisher    = {Association for Computing Machinery},
  title        = {{Certificates in AI: Learn but verify}},
  doi          = {10.1145/3737447},
  volume       = {69},
  year         = {2026},
}

@phdthesis{21401,
  abstract     = {Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.

In this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation.

The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.
},
  author       = {Karimi, Mahyar},
  issn         = {2791-4585},
  keywords     = {Privacy-preserving verification, Runtime verification, Monitoring, Reactive functionalities, Cryptographic protocols},
  pages        = {60},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Privacy-preserving runtime verification}},
  doi          = {10.15479/AT-ISTA-21401},
  year         = {2026},
}

@inproceedings{22103,
  abstract     = {Modern AI systems increasingly rely on opaque, highly complex models whose inner workings remain inaccessible even to experts. This opacity creates challenges for trust, accountability, and compliance with
emerging regulatory expectations such as the “right to an explanation”. While traditional explainability methods—feature attributions, counterfactuals, surrogate models—and interpretable model classes provide valuable insights for engineers, they often fall short of delivering the contextual, conversational explanations that
real users expect. Large Language Models (LLMs) offer a promising new avenue for explanation due to their
ability to engage interactively, adapt to user needs, and translate technical outputs into more accessible reasoning. However, their tendencies toward hallucination, conflict avoidance, and oversimplification introduce
serious risks when used as explanatory agents. This paper analyzes these opportunities and limitations, examines verification strategies for ensuring explanation fidelity, and situates LLM-generated explanations within
broader concerns about public trust. The paper concludes by outlining best practices and future research directions for building robust, verifiable, and human-aligned explanation systems.},
  author       = {Cano Cordoba, Filip},
  booktitle    = {Proceedings of the 18th International Conference on Agents and Artificial Intelligence},
  isbn         = {9789897587962},
  issn         = {2184-433X},
  keywords     = {Explainable AI, Large Language Models, Trust in AI},
  location     = {Marbella, Spain},
  pages        = {4689--4696},
  publisher    = {Science and Technology Publications},
  title        = {{Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants}},
  doi          = {10.5220/0014483200004052},
  volume       = {5},
  year         = {2026},
}

@inbook{22300,
  abstract     = {As seen in previous chapters, a graph game proceeds by placing a token on one of the vertices and allowing the players to move it throughout the graph to produce an infinite trace, which determines the winner or payoff of the game.},
  author       = {Avni, Guy and Henzinger, Thomas A},
  booktitle    = {Games on Graphs. From Logic and Automata to Algorithms},
  editor       = {Fijalkow,  ‪Nathanaël},
  isbn         = {9781009500685},
  pages        = {529--569},
  publisher    = {Cambridge University Press},
  title        = {{Bidding Games}},
  doi          = {10.1017/9781009500678.022},
  year         = {2026},
}

@inproceedings{22294,
  abstract     = {Modern computer systems store vast amounts of personal data, enabling advances in AI and ML but risking user privacy and trust. For privacy reasons, it is sometimes desired for an ML model to forget part of the data it was trained on. In this paper, we introduce a novel unlearning approach based on Forgetting Neural Networks (FNNs), a neuroscience-inspired architecture that explicitly encodes forgetting through multiplicative decay factors. While FNNs had previously been studied as a theoretical construct, we provide the first concrete implementation and demonstrate their effectiveness for targeted unlearning. We propose several variants with per-neuron forgetting factors, including rank-based assignments guided by activation levels, and evaluate them on MNIST and Fashion-MNIST benchmarks. Our method systematically removes information associated with forget sets while preserving performance on retained data. Membership inference attacks confirm the effectiveness of FNN-based unlearning in erasing information about the training data from the neural network. These results establish FNNs as a promising foundation for efficient and interpretable unlearning. },
  author       = {Hatua, Amartya and Nguyen, Trung and Cano Cordoba, Filip and Sung, Andrew},
  booktitle    = {Proceedings of the 18th International Conference on Agents and Artificial Intelligence},
  isbn         = {9789897587962},
  issn         = {2184-433X},
  keywords     = {Machine Unlearning, Neuroscience-Inspired Machine Learning, Membership Inference Attacks},
  location     = {Marbella, Spain},
  pages        = {1536--1546},
  publisher    = {SciTePress},
  title        = {{Machine unlearning using forgetting neural networks}},
  doi          = {10.5220/0014326500004052},
  volume       = {2},
  year         = {2026},
}

@inproceedings{22321,
  abstract     = {Runtime fairness is not a one-time constraint but a dynamic property evaluated over a sequence of decisions. To ensure fairness at runtime, it is necessary to account for past decisions, information neglected by conventional, static classifiers. Traditional fairness shields enforce runtime fairness abruptly, by intervening deterministically whenever a sequence of decisions violates the target for a running fairness measure. This motivates our main conceptual contribution: energy shields. An energy shield is a novel, lightweight, adaptive controller that monitors a sequence of decisions and intervenes probabilistically to ensure runtime fairness smoothly, by utilizing physics-inspired energy functions to nudge the sequence toward fairness: the more unfair the decisions, the stronger the nudging force becomes. This makes energy shields the first fairness shields to provide both short-term safety and long-term liveness guarantees. Safety ensures that the running fairness measure stays within a running target interval with high probability, and liveness ensures that the limit of the fairness measure lies within the limit target interval. Intuitively, the short-term specifies the tolerated fairness values and the long-term specifies the desired fairness values. We also provide a synthesis procedure for constructing the least intrusive energy shield for a given target specification, and demonstrate its efficiency experimentally. We evaluate our energy shields against existing fairness shields through the lens of short- and long-term fairness.},
  author       = {Cano Cordoba, Filip and Henzinger, Thomas A and Kueffner, Konstantin},
  booktitle    = {Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency},
  location     = {Montreal, Canada},
  pages        = {4243 -- 4275},
  publisher    = {Association for Computing Machinery},
  title        = {{Energy shields for fairness}},
  doi          = {10.1145/3805689.3806807},
  year         = {2026},
}

@inproceedings{22617,
  abstract     = {Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says "Heads" or "Tails". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!
We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.},
  author       = {Brice, Leonard J and Henzinger, Thomas A and Thejaswini, K. S.},
  booktitle    = {41st Annual Symposium on Logic in Computer Science},
  isbn         = {9783959774345},
  issn         = {1868-8969},
  keywords     = {Concurrent games, Shared randomness, Topology, Algebraic Geometry},
  location     = {Lisbon, Portugal},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Dicey games: Shared sources of randomness in distributed systems}},
  doi          = {10.4230/LIPIcs.LICS.2026.23},
  volume       = {380},
  year         = {2026},
}

@article{22406,
  abstract     = {It is known that for a uniform morphic sequence 𝒖 =⟨𝑢𝑛⟩∞
𝑛=0 and an algebraic number 𝛽 such that |𝛽| >1, the number [[𝒖]]𝛽 :=∑∞
𝑛=0(𝑢𝑛/𝛽𝑛) either lies in ℚ⁡(𝛽) or is transcendental. In this paper, we show a similar rational–transcendental dichotomy for sequences defined by irreducible Pisot morphisms on binary alphabets. Subject to the Pisot conjecture (an irreducible Pisot morphism has pure discrete spectrum), we generalise the latter result to arbitrary finite alphabets. In certain cases, we are able to show transcendence of [[𝒖]]𝛽 outright. In particular, for 𝑘 ≥2, if 𝒖 is the k-Bonacci word, then [[𝒖]]𝛽 is transcendental.},
  author       = {Kebis, Pavol and LUCA, FLORIAN and OUAKNINE, JOEL and SCOONES, ANDREW and WORRELL, JAMES},
  issn         = {1469-4417},
  journal      = {Ergodic Theory and Dynamical Systems},
  keywords     = {balanced-pair algorithm, Cobham’s conjecture, k-Bonacci words, Pisot conjecture, subspace theorem},
  pages        = {1--22},
  publisher    = {Cambridge University Press},
  title        = {{Transcendence for Pisot morphic words over an algebraic base}},
  doi          = {10.1017/etds.2026.10324},
  year         = {2026},
}

@inproceedings{22717,
  abstract     = {We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other.

We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (ER) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is NP-hard. For the almost-sure reachability problem, we prove NP-completeness.

We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.},
  author       = {Brice, Leonard J and Henzinger, Thomas A and Montaseri, Alipasha and Shafiee, Ali and Thejaswini, K. S.},
  booktitle    = {38th International Conference on Computer Aided Verification},
  isbn         = {9783032325181},
  issn         = {1611-3349},
  location     = {Lisbon, Portugal},
  pages        = {215--236},
  publisher    = {Springer Nature},
  title        = {{Randomise alone, reach as a team}},
  doi          = {10.1007/978-3-032-32519-8_12},
  volume       = {16682},
  year         = {2026},
}

@inproceedings{22719,
  abstract     = {We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.},
  author       = {Avni, Guy and Henzinger, Thomas A and Mallik, Kaushik and Sadhukhan, Suman and Thejaswini, K. S.},
  booktitle    = {38th International Conference on Computer Aided Verification},
  isbn         = {9783032325181},
  issn         = {1611-3349},
  location     = {Lisbon, Portugal},
  pages        = {237--257},
  publisher    = {Springer Nature},
  title        = {{Decoupled planning for multiple omega-regular objectives}},
  doi          = {10.1007/978-3-032-32519-8_13},
  volume       = {16682},
  year         = {2026},
}

@inproceedings{22754,
  abstract     = {Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite infixes and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date.

We close this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK’s existing decision procedures. These reductions preserve the answers to threshold decision problems, while allowing users to specify properties in the more expressive NQA formalism. The tool handles all combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations) for which emptiness and universality are known to be decidable. Experiments on response-time and resource-consumption benchmarks demonstrate QuAK’s effectiveness.},
  author       = {Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E and Yılmaz, Harun},
  booktitle    = {38th International Conference on Computer Aided Verification},
  isbn         = {9783032325259},
  issn         = {1611-3349},
  location     = {Lisbon, Portugal},
  pages        = {418--432},
  publisher    = {Springer Nature},
  title        = {{Extending QuAK with nested quantitative automata}},
  doi          = {10.1007/978-3-032-32526-6_20},
  volume       = {16683},
  year         = {2026},
}

@inproceedings{22920,
  abstract     = {Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.
In this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.
Finally, we study a repair problem that asks whether bidding vertices can be assigned "owners" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete.},
  author       = {Asadi, Ali and Henzinger, Thomas A and Kafshdar Goharshadi, Ehsan and Kebis, Pavol and Mallik, Kaushik},
  booktitle    = {37th International Conference on Concurrency Theory},
  isbn         = {9783959774475},
  issn         = {1868-8969},
  keywords     = {Bidding Games, Stochastic Games},
  location     = {Liverpool, United Kingdom},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Generalized bidding games: Where bidding and stochastic games meet}},
  doi          = {10.4230/LIPIcs.CONCUR.2026.13},
  volume       = {391},
  year         = {2026},
}

@inproceedings{22919,
  abstract     = {Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability.},
  author       = {Asadi, Ali and Chatterjee, Krishnendu and Kebis, Pavol},
  booktitle    = {37th International Conference on Concurrency Theory},
  isbn         = {9783959774475},
  issn         = {1868-8969},
  keywords     = {formal methods, games and logic, logical aspects of AI, model checking},
  location     = {Liverpool, United Kingdom},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{PAC learning in turn-based stochastic games with reachability objectives: A decentralized private approach via expected conditional distance}},
  doi          = {10.4230/LIPIcs.CONCUR.2026.12},
  volume       = {391},
  year         = {2026},
}

@phdthesis{22808,
  abstract     = {As automated decision-makers have become ubiquitous in many domains of life,
their decisions have become increasingly consequential. Recent years have shown
that such systems can exhibit discriminatory behaviour against individuals and
social groups alike, thereby amplifying existing biases and entrenching
socio-economic disparities over time. Algorithmic fairness addresses this
problem by developing methods to quantify and mitigate unfair behaviour.
However, much of the existing literature studies fairness in a static
pre-deployment setting and, therefore, neglects that automated decision-makers are
often deployed in dynamic environments, where their behaviour and the
populations they affect may change over time.

This thesis addresses this gap through the lens of runtime verification.
Instead of treating fairness as a property of a classifier together with a fixed
input distribution, it reframes fairness as a property of the interaction trace
between the decision-maker and its deployment environment. To evaluate such
sequential fairness properties, the thesis develops runtime monitors that
observe the evolving interaction between the system and the environment and
issue verdicts after each new observation. Because, these monitors are designed to detect
unfair behaviour during deployment, they complement fair training,
auditing, verification, and enforcement by providing an additional layer of mathematically rigorous fairness assurance.

In summary, the thesis develops quantitative, trace-based analogues of
classical group and individual fairness measures and constructs monitors for
them. This includes monitors for long-run group fairness over Markovian traces,
for the time-varying welfare of a changing population in a dynamical system, and
for the individual fairness of an arbitrary system generating a trace of inputs
and outputs. To achieve this, the monitors combine ideas from runtime
verification, sequential statistics, and nearest-neighbour search. In the
group-fairness settings, monitoring is primarily a sequential statistical
estimation problem: the monitor must construct statistically sound interval
estimates of fairness values from dependent and partially observed interactions.
In the individual-fairness setting, the main challenge is computational
efficiency: the monitor must detect individual fairness violations by efficiently comparing the
current decision with all previously observed decisions.
},
  author       = {Kueffner, Konstantin},
  isbn         = {978-3-99078-089-3},
  issn         = {2663-337X},
  pages        = {183},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Monitoring algorithmic fairness in sequential decision making}},
  doi          = {10.15479/AT-ISTA-22808},
  year         = {2026},
}

@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},
}

@inproceedings{21020,
  abstract     = {Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.
In this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation.
The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.},
  author       = {Henzinger, Thomas A and Karimi, Mahyar and Thejaswini, K. S.},
  booktitle    = {Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security},
  isbn         = {9798400715259},
  location     = {Taipei, Taiwan},
  pages        = {2774--2787},
  publisher    = {Association for Computing Machinery},
  title        = {{Privacy-preserving runtime verification}},
  doi          = {10.1145/3719027.3765137},
  year         = {2025},
}

@inproceedings{21089,
  abstract     = {Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results.},
  author       = {Chalupa, Marek and Henzinger, Thomas A and Oliveira da Costa, Ana A},
  booktitle    = {45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  location     = {Pilani, India},
  pages        = {20:1--20:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Flavors of quantifiers in hyperlogics}},
  doi          = {10.4230/LIPICS.FSTTCS.2025.20},
  volume       = {360},
  year         = {2025},
}

@inproceedings{21091,
  abstract     = {Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.},
  author       = {Henzinger, Thomas A and Kueffner, Konstantin and Yu, Zhengqi},
  booktitle    = {25th International Conference on Runtime Verification},
  issn         = {1611-3349},
  location     = {Graz, Austria},
  pages        = {54--72},
  publisher    = {Springer Nature},
  title        = {{Formal verification of neural certificates done dynamically}},
  doi          = {10.1007/978-3-032-05435-7_4},
  volume       = {16087},
  year         = {2025},
}

@inproceedings{21092,
  abstract     = {Formal verification provides assurances that a probabilistic system satisfies its specification—conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model’s predicted and the system’s (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.},
  author       = {Henzinger, Thomas A and Kueffner, Konstantin and Singh, Vasu and Sun, I},
  booktitle    = {25th International Conference on Runtime Verification},
  issn         = {1611-3349},
  location     = {Graz, Austria},
  pages        = {140--159},
  publisher    = {Springer Nature},
  title        = {{Alignment monitoring}},
  doi          = {10.1007/978-3-032-05435-7_9},
  volume       = {16087},
  year         = {2025},
}