Bernd Finkbeiner

FM Conference 2026 Conference Paper

Pacing Types for Asynchronous Stream Equations

• Florian Kohn
• Arthur Correnson
• Jan Baumeister
• Bernd Finkbeiner

Abstract Stream-based monitoring is a runtime verification approach where a monitor aggregates streams of input data from sensors and other sources to give real-time statistics and assessments of a system’s health. One of the central challenges in designing reliable stream-based monitors is to deal with the asynchronous nature of data streams: in concrete applications, the different sensors being monitored produce values at different speeds, and it is the monitor’s responsibility to correctly react to the asynchronous arrival of different streams of values. To ease this process, modern frameworks for stream-based monitoring such as RTLola enable users to finely specify data synchronization policies via a system of pacing annotations. While this feature simplifies the design of monitors, it can also lead users to write inconsistent policies, where synchronization between two streams is explicitly requested via annotations, but cannot always be achieved. To mitigate this issue, this paper presents pacing types, a novel type system implemented in RTLola to ensure that monitors for asynchronous streams are free of timing inconsistencies. We give a formal semantics to pacing annotations for a core fragment of RTLola, and present a soundness proof of the pacing type system. For an additional level of guarantees, we machine-checked the soundness proof using the Rocq proof assistant.

TACAS Conference 2026 Conference Paper

Trace Repair for Temporal Behavior Trees

• Sebastian Schirmer
• Philipp Schitz
• Johann C. Dauer
• Bernd Finkbeiner
• Sriram Sankaranarayanan

AAAI Conference 2026 Conference Paper

Universal Safety Controllers with Learned Prophecies

• Bernd Finkbeiner
• Niklas Metzger
• Satya Prakash Nayak
• Anne-Kathrin Schmuck

Universal Safety Controllers (USCs) are a promising logical control framework that guarantees the satisfaction of a given temporal safety specification when applied to any realizable plant model. Unlike traditional methods, which synthesize one logical controller over a given detailed plant model, USC synthesis constructs a generic controller whose outputs are conditioned by plant behavior, called prophecies. Thereby, USCs offer strong generalization and scalability benefits over classical logical controllers. However, the exact computation and verification of prophecies remain computationally challenging. In this paper, we introduce an approximation algorithm for USC synthesis that addresses these limitations via learning. Instead of computing exact prophecies, which reason about sets of trees via automata, we only compute under- and over-approximations from (small) example plants and infer computation tree logic (CTL) formulas as representations of prophecies. The resulting USC generalizes to unseen plants via a verification step and offers improved efficiency and explainability through small and concise CTL prophecies, which remain human-readable and interpretable. Experimental results demonstrate that our learned prophecies remain generalizable, yet are significantly more compact and interpretable than their exact tree automata representations.

KR Conference 2025 Conference Paper

An Information-Flow Perspective on Explainability Requirements: Specification and Verification

• Bernd Finkbeiner
• Hadar Frenkel
• Julian Siber

Explainable systems expose information about why certain observed effects are happening to the agents interacting with them. We argue that this constitutes a positive flow of information that needs to be specified, verified, and balanced against negative information flow that may, e. g. , violate privacy guarantees. Since both explainability and privacy require reasoning about knowledge, we tackle these tasks with epistemic temporal logic extended with quantification over counterfactual causes. This allows us to specify that a multi-agent system exposes enough information such that agents acquire knowledge on why some effect occurred. We show how this principle can be used to specify explainability as a system-level requirement and provide an algorithm for checking finite-state models against such specifications. We present a prototype implementation of the algorithm and evaluate it on several benchmarks, illustrating how our approach distinguishes between explainable and unexplainable systems, and how it allows to pose additional privacy requirements.

AAMAS Conference 2025 Conference Paper

Multiplayer Games With Incomplete Information for Hyperproperty Verification

• Raven Beutner
• Bernd Finkbeiner

Hyperproperties are system properties that relate multiple execution traces in a system and can, e. g. , express security policies, knowledge properties, path planning, and robustness requirements. Logics for expressing temporal hyperproperties - such as Hyper- LTL - extend LTL by quantifying over executions of a system. Many properties used in practice require one or more quantifier alternations, which presents a major challenge for verification. Complete verification methods require a system complementation for each quantifier alternation, making it infeasible in practice. A cheaper method interprets the verification of a HyperLTL formula as a twoplayer parity game between universal and existential quantifiers. This game-based approach is very efficient and allows for interactive proofs, but is limited to ∀∗∃∗ HyperLTL formulas, leaving important properties out of reach. In this paper, we argue that we can extend the game-based verification approach to arbitrary HyperLTL formulas, by utilizing multiple players and incomplete information.

ECAI Conference 2025 Conference Paper

On Conformant Planning and Model-Checking of ∃ * ∀ * Hyperproperties

• Raven Beutner
• Bernd Finkbeiner

We study the connection of two problems within the planning and verification community: Conformant planning and model-checking of hyperproperties. Conformant planning is the task of finding a sequential plan that achieves a given objective independent of non-deterministic action effects during the plan’s execution. Hyperproperties are system properties that relate multiple execution traces of a system and, e. g. , capture information-flow and fairness policies. In this paper, we show that model-checking of ∃*∀* hyperproperties is closely related to the problem of computing a conformant plan. Firstly, we show that we can efficiently reduce a hyperproperty model-checking instance to a conformant planning instance, and prove that our encoding is sound and complete. Secondly, we establish the converse direction: Every conformant planning problem is, itself, a hyperproperty model-checking task.

KR Conference 2025 Conference Paper

Strategy Logic, Imperfect Information, and Hyperproperties

• Raven Beutner
• Bernd Finkbeiner

Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strategies) cannot observe the global state of the system, leading to many extensions of SL centered around imperfect information, such as strategy logic with imperfect information (SL_ii). Along orthogonal lines, researchers have studied the combination of strategic behavior and hyperproperties. Hyperproperties are system properties that relate multiple executions in a system and commonly arise when specifying security policies. Hyper Strategy Logic (HyperSL) is a temporal logic that combines quantification over strategies with the ability to express hyperproperties on the executions of different strategy profiles. In this paper, we study the relation between SL_ii and HyperSL. Our main result is that both logics (restricted to formulas where no state formulas are nested within path formulas) are equivalent in the sense that we can encode SL_ii instances into HyperSL instances and vice versa. For the former direction, we build on the well-known observation that imperfect information is a hyperproperty. For the latter direction, we construct a self-composition of MASs and show how we can simulate hyperproperties using imperfect information.

AAMAS Conference 2024 Conference Paper

Hyper Strategy Logic

• Raven Beutner
• Bernd Finkbeiner

Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and provides a logical framework to express many important properties such as Nash equilibria, dominant strategies, etc. While in SL the same strategy can be used in multiple strategy profiles, each such profile is evaluated w. r. t. a pathproperty, i. e. , a property that considers the single path resulting from a particular strategic interaction. In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the outcome of multiple strategy profiles can be compared w. r. t. a hyperproperty, i. e. , a property that relates multiple paths. We show that HyperSL can capture important properties that cannot be expressed in SL, including non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.

GandALF Workshop 2024 Invited Paper

Hyperproperties: the Exciting World Beyond k-Hypersafety

• Bernd Finkbeiner

System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such requirements belong to the class of hyperproperties, which generalize classic trace properties to properties of sets of traces. A key idea in the verification of hyperproperties has been to analyze self-compositions of programs. Hyperproperties that need to hold for all possible combinations of k traces, such as k-hypersafety properties, can be analyzed as standard trace properties of the k-fold self-composition. The implicit universal quantification over the traces is, however, an inherent limitation of this paradigm, which makes it difficult to abstract in an existential manner from phenomena like scheduling in concurrent programs, nondeterministic choice, or speed of execution in asynchronous computations. Alternations between quantifiers are furthermore essential for counterfactual reasoning about causation and blame. In this talk, we will explore the exciting world of hyperproperties beyond k-hypersafety. I will discuss the decidability and complexity of reasoning about such hyperproperties and present algorithmic techniques for the effective resolution of quantifier alternations. I will also give an overview of recently introduced logics for the specification of hyperproperties beyond k-hypersafety, including logics that combine hyperproperties with reasoning over strategies, and logics for second-order hyperproperties.

NeurIPS Conference 2024 Conference Paper

Learning Better Representations From Less Data For Propositional Satisfiability

• Mohamed Ghanem
• Frederik Schmitt
• Julian Siber
• Bernd Finkbeiner

Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by $\sim$$32$% after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

AAMAS Conference 2024 Conference Paper

Monitoring Second-Order Hyperproperties

• Raven Beutner
• Bernd Finkbeiner
• Hadar Frenkel
• Niklas Metzger

Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge, information flow, and privacy. In this paper, we study the monitoring of complex hyperproperties at runtime. Previous work in this area has either focused on the simpler problem of monitoring trace properties (which are sets of traces, while hyperproperties are sets of sets of traces) or on monitoring first-order hyperproperties, which are expressible in temporal logics with first-order quantification over traces, such as Hyper- LTL. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. Second-order hyperproperties include system properties like common knowledge, which cannot be expressed in first-order logics like HyperLTL. We introduce Hyper2LTL𝑓, a temporal logic over finite traces that allows for second-order quantification over sets of traces. We study the monitoring problem in two fundamental execution models: (1) the parallel model, where a fixed number of traces is monitored in parallel, and (2) the sequential model, where an unbounded number of traces is observed sequentially, one trace after the other. For the parallel model, we show that the monitoring of the secondorder hyperproperties of Hyper2LTL𝑓 can be reduced to monitoring first-order hyperproperties. For the sequential model, we present a monitoring algorithm that handles second-order quantification efficiently, exploiting optimizations based on the monotonicity of subformulas, graph-based storing of executions, and fixpoint hashing. We present experimental results from a range of benchmarks, including examples from common knowledge and planning.

ICAPS Conference 2024 Conference Paper

Non-deterministic Planning for Hyperproperty Verification

• Raven Beutner
• Bernd Finkbeiner

Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e. g. , capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.

AAAI Conference 2024 Conference Paper

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

• Raven Beutner
• Bernd Finkbeiner

Alternating-time temporal logic (ATL*) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL* can reason about the strategic ability of agents (e.g., some coalition A can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition A can reach a goal sooner (or more often) than some other coalition A'. In this paper, we propose HyperATL*_S, an extension of ATL* in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL*_S is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL*_S on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.

LPAR Conference 2023 Conference Paper

Counterfactuals Modulo Temporal Logics

• Bernd Finkbeiner
• Julian Siber

Lewis’ theory of counterfactuals is the foundation of many contemporary notions of causality. In this paper, we extend this theory in the temporal direction to enable symbolic counterfactual reasoning on infinite sequences, such as counterexamples found by a model checker and trajectories produced by a reinforcement learning agent. In particular, our extension considers a more relaxed notion of similarity between worlds and proposes two additional counterfactual operators that close a semantic gap between the previous two in this more general setting. Further, we consider versions of counterfactuals that minimize the distance to the witnessing counterfactual worlds, a common requirement in causal analysis. To automate counterfactual reasoning in the temporal domain, we introduce a logic that combines temporal and counterfactual operators, and outline decision procedures for the satisfiability and trace-checking problems of this logic.

ICLR Conference 2023 Conference Paper

Iterative Circuit Repair Against Formal Specifications

• Matthias Cosler
• Frederik Schmitt
• Christopher Hahn
• Bernd Finkbeiner

We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by $6.8$ percentage points on held-out instances and $11.8$ percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.

Highlights Conference 2023 Conference Abstract

Logics and Algorithms for Hyperproperties (Part 1)

• Bernd Finkbeiner

System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such requirements belong to the class of hyperproperties, which generalize classic trace properties to properties of sets of traces. During the past decade, a range of new specification logics has been introduced with the goal of providing a unified theory for reasoning about hyperproperties. This tutorial gives an overview of the current landscape of logics for the specification of hyperproperties and algorithms for satisfiability checking, model checking, monitoring, and synthesis.

Highlights Conference 2023 Conference Abstract

Logics and Algorithms for Hyperproperties (Part 2)

• Bernd Finkbeiner

LPAR Conference 2023 Conference Paper

Model Checking Omega-Regular Hyperproperties with AutoHyperQ

• Raven Beutner
• Bernd Finkbeiner

Hyperproperties are commonly used to define information-flow policies and other re- quirements that reason about the relationship between multiple traces in a system. We consider HyperQPTL – a temporal logic for hyperproperties that combines explicit quan- tification over traces with propositional quantification as, e. g. , found in quantified proposi- tional temporal logic (QPTL). HyperQPTL therefore truly captures ω-regular relations on multiple traces within a system. As such, HyperQPTL can, e. g. , express promptness prop- erties, which state that there exists a common bound on the number of steps up to which an event must have happened. While HyperQPTL has been studied and used in various prior works, thus far, no model-checking tool for it exists. This paper presents AutoHyperQ, a fully-automatic automata-based model checker for HyperQPTL that can cope with arbitrary combinations of trace and propositional quantification. We evaluate AutoHyperQ on a range of benchmarks and, e. g. , use it to analyze promptness requirements in a diverse collection of reactive systems. Moreover, we demonstrate that the core of AutoHyperQ can be reused as an effective tool to translate QPTL formulas into ω-automata.

CSL Conference 2022 Conference Paper

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

• Bernd Finkbeiner
• Manuel Gieseking
• Jesko Hecking-Harbusch
• Ernst-Rüdiger Olderog

In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i. e. , conditions that only refer to individual components. In this paper, we consider global winning conditions such as mutual exclusion, i. e. , conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.

NeurIPS Conference 2021 Conference Paper

Neural Circuit Synthesis from Specification Patterns

• Frederik Schmitt
• Christopher Hahn
• Markus N Rabe
• Bernd Finkbeiner

We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic (LTL). The LTL synthesis problem is a well-known algorithmic challenge with a long history and an annual competition is organized to track the improvement of algorithms and tooling over time. New approaches using machine learning might open a lot of possibilities in this area, but suffer from the lack of sufficient amounts of training data. In this paper, we consider a method to generate large amounts of additional training data, i. e. , pairs of specifications and circuits implementing them. We ensure that this synthetic data is sufficiently close to human-written specifications by mining common patterns from the specifications used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.

ICLR Conference 2021 Conference Paper

Teaching Temporal Logics to Neural Networks

• Christopher Hahn
• Frederik Schmitt
• Jens U. Kreber
• Markus N. Rabe
• Bernd Finkbeiner

We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.

I&C Journal 2017 Journal Article

Petri games: Synthesis of distributed systems with causal memory

• Bernd Finkbeiner
• Ernst-Rüdiger Olderog

We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.

Highlights Conference 2016 Conference Abstract

Deciding Hyperproperties

• Bernd Finkbeiner
• Christopher Hahn

This talk is based on the paper “Deciding Hyperproperties” by Bernd Finkbeiner and Christopher Hahn, which appeared on the 27th International Conference on Concurrency Theory (CONCUR 2016). Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. We study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall formulas, and undecidable for forall-exists formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.

SAT Conference 2014 Conference Paper

Fast DQBF Refutation

• Bernd Finkbeiner
• Leander Tentrup

Abstract Dependency Quantified Boolean Formulas (DQBF) extend QBF with Henkin quantifiers, which allow for non-linear dependencies between the quantified variables. This extension is useful in verification problems for incomplete designs, such as the partial equivalence checking (PEC) problem, where a partial circuit, with some parts left open as “black boxes”, is compared against a full circuit. The PEC problem is to decide whether the black boxes in the partial circuit can be filled in such a way that the two circuits become equivalent, while respecting that each black box only observes the subset of the signals that are designated as its input. We present a new algorithm that efficiently refutes unsatisfiable DQBF formulas. The algorithm detects situations in which already a subset of the possible assignments of the universally quantified variables suffices to rule out a satisfying assignment of the existentially quantified variables. Our experimental evaluation on PEC benchmarks shows that the new algorithm is a significant improvement both over approximative QBF-based methods, where our results are much more accurate, and over precise methods based on variable elimination, where the new algorithm scales better in the number of Henkin quantifiers.

Highlights Conference 2014 Conference Abstract

Petri Games: Synthesis of Distributed Systems with Causal Memory

• Bernd Finkbeiner

We present Petri games as a new foundation for the synthesis of distributed systems. The players of a Petri game are tokens on a Petri net. Petri games differ from the standard Pnueli/Rosner model for distributed synthesis, which is based on the notion of partial observability, i. e. , the strategy of each process of the implementation may only depend on a subset of the system variables. Synthesis under the Pnueli/Rosner model is only decidable for restricted system architectures like pipelines and rings. Instead of partial observation, Petri games are based on causality. This change leads to new decidability results and algorithms for the synthesis of distributed systems.

GandALF Workshop 2014 Workshop Paper

Petri Games: Synthesis of Distributed Systems with Causal Memory

• Bernd Finkbeiner
• Ernst-Rüdiger Olderog

We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.

GandALF Workshop 2011 Workshop Paper

Reactive Safety

• Rüdiger Ehlers
• Bernd Finkbeiner

The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i. e. , for systems whose behavior is characterized by the interplay of uncontrolled environment inputs and controlled system outputs. We show that reactive safety is a strictly larger class of properties than standard safety. We provide algorithms for checking if a property, given as a temporal formula or as a word or tree automaton, is a reactive safety property and for translating such properties into safety automata. Based on this construction, the standard verification and synthesis algorithms for safety properties immediately extend to the larger class of reactive safety.

CSL Conference 2010 Conference Paper

Coordination Logic

• Bernd Finkbeiner
• Sven Schewe

Abstract We introduce Coordination Logic (CL), a new temporal logic that reasons about the interplay between behavior and informedness in distributed systems. CL provides a logical representation for the distributed realizability problem and extends the game-based temporal logics, including the alternating-time temporal logics, strategy logic, and game logic, with quantification over strategies under incomplete information. We show that the structure in CL that results from the nesting of the quantifiers is sufficient to guarantee the decidability of the logic and at the same time general enough to subsume and extend all previously known decidable cases of the distributed realizability problem.

CSL Conference 2006 Conference Paper

Satisfiability and Finite Model Property for the Alternating-Time mu -Calculus

• Sven Schewe
• Bernd Finkbeiner

Abstract This paper presents a decision procedure for the alternating-time μ -calculus. The algorithm is based on a representation of alternating-time formulas as automata over concurrent game structures. We show that language emptiness of these automata can be checked in exponential time. The complexity of our construction meets the known lower bounds for deciding the satisfiability of the classic μ -calculus. It follows that the satisfiability problem is EXPTIME-complete for the alternating-time μ -calculus.

LOPSTR Conference 2006 Conference Paper

Synthesis of Asynchronous Systems

• Sven Schewe
• Bernd Finkbeiner

Abstract This paper addresses the problem of synthesizing an asynchronous system from a temporal specification. We show that the cost of synthesizing a single-process implementation is the same for synchronous and asynchronous systems (2EXPTIME-complete for CTL* and EXPTIME-complete for the μ -calculus) if we assume a full scheduler (i. e. , a scheduler that allows every possible scheduling), and exponentially more expensive for asynchronous systems without this assumption (3EXPTIME-complete for CTL* and 2EXPTIME-complete for the μ -calculus). While multi-process synthesis for synchronous distributed systems is possible for certain architectures (like pipelines and rings), we show that the synthesis of asynchronous distributed systems is decidable if and only if at most one process implementation is unknown.

TIME Conference 2005 Conference Paper

LOLA: Runtime Monitoring of Synchronous Systems

• Ben D'Angelo
• Sriram Sankaranarayanan 0001
• César Sánchez 0001
• Will Robinson
• Bernd Finkbeiner
• Henny B. Sipma
• Sandeep Mehrotra
• Zohar Manna

We present a specification language and algorithms for the online and offline monitoring of synchronous systems including circuits and embedded systems. Such monitoring is useful not only for testing, but also under actual deployment. The specification language is simple and expressive; it can describe both correctness/failure assertions along with interesting statistical measures that are useful for system profiling and coverage analysis. The algorithm for online monitoring of queries in this language follows a partial evaluation strategy: it incrementally constructs output streams from input streams, while maintaining a store of partially evaluated expressions for forward references. We identify a class of specifications, characterized syntactically, for which the algorithm's memory requirement is independent of the length of the input streams. Being able to bound memory requirements is especially important in online monitoring of large input streams. We extend the concepts used in the online algorithm to construct an efficient offline monitoring algorithm for large traces. We have implemented our algorithm and applied it to two industrial systems, the PCI bus protocol and a memory controller. The results demonstrate that our algorithms are practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.