-
Counterfactual-based Root Cause Analysis for Dynamical Systems
Authors:
Juliane Weilbach,
Sebastian Gerwinn,
Karim Barsim,
Martin Fränzle
Abstract:
Identifying the underlying reason for a failing dynamic process or otherwise anomalous observation is a fundamental challenge, yet has numerous industrial applications. Identifying the failure-causing sub-system using causal inference, one can ask the question: "Would the observed failure also occur, if we had replaced the behaviour of a sub-system at a certain point in time with its normal behavi…
▽ More
Identifying the underlying reason for a failing dynamic process or otherwise anomalous observation is a fundamental challenge, yet has numerous industrial applications. Identifying the failure-causing sub-system using causal inference, one can ask the question: "Would the observed failure also occur, if we had replaced the behaviour of a sub-system at a certain point in time with its normal behaviour?" To this end, a formal description of behaviour of the full system is needed in which such counterfactual questions can be answered. However, existing causal methods for root cause identification are typically limited to static settings and focusing on additive external influences causing failures rather than structural influences. In this paper, we address these problems by modelling the dynamic causal system using a Residual Neural Network and deriving corresponding counterfactual distributions over trajectories. We show quantitatively that more root causes are identified when an intervention is performed on the structural equation and the external influence, compared to an intervention on the external influence only. By employing an efficient approximation to a corresponding Shapley value, we also obtain a ranking between the different subsystems at different points in time being responsible for an observed failure, which is applicable in settings with large number of variables. We illustrate the effectiveness of the proposed method on a benchmark dynamic system as well as on a real world river dataset.
△ Less
Submitted 12 June, 2024;
originally announced June 2024.
-
Monitoring Real-Time Systems under Parametric Delay
Authors:
Martin Fränzle,
Thomas M. Grosen,
Kim G. Larsen,
Martin Zimmermann
Abstract:
Online monitoring of embedded real-time systems can be achieved by reduction of an adequate property language, like Metric Interval Temporal Logic, to timed automata and symbolic execution of the resulting automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time sta…
▽ More
Online monitoring of embedded real-time systems can be achieved by reduction of an adequate property language, like Metric Interval Temporal Logic, to timed automata and symbolic execution of the resulting automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring procedure and its implementation which handle such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata.
△ Less
Submitted 28 April, 2024;
originally announced April 2024.
-
Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games
Authors:
Martin Fränzle,
Sarah Winter,
Martin Zimmermann
Abstract:
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We fu…
▽ More
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyze existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down.
△ Less
Submitted 2 October, 2023;
originally announced October 2023.
-
Estimation of Counterfactual Interventions under Uncertainties
Authors:
Juliane Weilbach,
Sebastian Gerwinn,
Melih Kandemir,
Martin Fraenzle
Abstract:
Counterfactual analysis is intuitively performed by humans on a daily basis eg. "What should I have done differently to get the loan approved?". Such counterfactual questions also steer the formulation of scientific hypotheses. More formally it provides insights about potential improvements of a system by inferring the effects of hypothetical interventions into a past observation of the system's b…
▽ More
Counterfactual analysis is intuitively performed by humans on a daily basis eg. "What should I have done differently to get the loan approved?". Such counterfactual questions also steer the formulation of scientific hypotheses. More formally it provides insights about potential improvements of a system by inferring the effects of hypothetical interventions into a past observation of the system's behaviour which plays a prominent role in a variety of industrial applications. Due to the hypothetical nature of such analysis, counterfactual distributions are inherently ambiguous. This ambiguity is particularly challenging in continuous settings in which a continuum of explanations exist for the same observation. In this paper, we address this problem by following a hierarchical Bayesian approach which explicitly models such uncertainty. In particular, we derive counterfactual distributions for a Bayesian Warped Gaussian Process thereby allowing for non-Gaussian distributions and non-additive noise. We illustrate the properties our approach on a synthetic and on a semi-synthetic example and show its performance when used within an algorithmic recourse downstream task.
△ Less
Submitted 15 September, 2023;
originally announced September 2023.
-
Safety Shielding under Delayed Observation
Authors:
Filip Cano Córdoba,
Alexander Palmisano,
Martin Fränzle,
Roderick Bloem,
Bettina Könighofer
Abstract:
Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guaran…
▽ More
Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guarantees, shields should interfere minimally with the agent. Therefore, shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. Current shielding approaches do not consider possible delays in the input signals in their safety analyses. In this paper, we address this issue. We propose synthesis algorithms to compute \emph{delay-resilient shields} that guarantee safety under worst-case assumptions on the delays of the input signals. We also introduce novel heuristics for deciding between multiple corrective actions, designed to minimize future shield interferences caused by delays. As a further contribution, we present the first integration of shields in a realistic driving simulator. We implemented our delayed shields in the driving simulator \textsc{Carla}. We shield potentially unsafe autonomous driving agents in different safety-critical scenarios and show the effect of delays on the safety analysis.
△ Less
Submitted 5 July, 2023;
originally announced July 2023.
-
On the Existence of Reactive Strategies Resilient to Delay
Authors:
Martin Fränzle,
Paul Kröger,
Sarah Winter,
Martin Zimmermann
Abstract:
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of…
▽ More
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in $[0,1]$. We show that for any rational threshold $θ\in [0,1]$ there is a game that can be won by the protagonist with exactly probability $θ$ under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined.
△ Less
Submitted 12 March, 2024; v1 submitted 31 May, 2023;
originally announced May 2023.
-
Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach
Authors:
Björn Koopmann,
Stefan Puch,
Günter Ehmen,
Martin Fränzle
Abstract:
In this paper, we propose an approach how connected and highly automated vehicles can perform cooperative maneuvers such as lane changes and left-turns at urban intersections where they have to deal with human-operated vehicles and vulnerable road users such as cyclists and pedestrians in so-called mixed traffic. In order to support cooperative maneuvers the urban intersection is equipped with an…
▽ More
In this paper, we propose an approach how connected and highly automated vehicles can perform cooperative maneuvers such as lane changes and left-turns at urban intersections where they have to deal with human-operated vehicles and vulnerable road users such as cyclists and pedestrians in so-called mixed traffic. In order to support cooperative maneuvers the urban intersection is equipped with an intelligent controller which has access to different sensors along the intersection to detect and predict the behavior of the traffic participants involved. Since the intersection controller cannot directly control all road users and - not least due to the legal situation - driving decisions must always be made by the vehicle controller itself, we focus on a decentralized control paradigm. In this context, connected and highly automated vehicles use some carefully selected game theory concepts to make the best possible and clear decisions about cooperative maneuvers. The aim is to improve traffic efficiency while maintaining road safety at the same time. Our first results obtained with a prototypical implementation of the approach in a traffic simulation are promising.
△ Less
Submitted 3 November, 2022;
originally announced November 2022.
-
Verification of Sigmoidal Artificial Neural Networks using iSAT
Authors:
Dominik Grundt,
Sorin Liviu Jurj,
Willem Hagemann,
Paul Kröger,
Martin Fränzle
Abstract:
This paper presents an approach for verifying the behaviour of nonlinear Artificial Neural Networks (ANNs) found in cyber-physical safety-critical systems. We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT and compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and a…
▽ More
This paper presents an approach for verifying the behaviour of nonlinear Artificial Neural Networks (ANNs) found in cyber-physical safety-critical systems. We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT and compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and an approximating approach. Our experimental results show that the dedicated and the compositional approach clearly outperform the approximating approach. Throughout all our benchmarks, the dedicated approach showed an equal or better performance compared to the compositional approach.
△ Less
Submitted 14 July, 2022;
originally announced July 2022.
-
Safe, Deterministic Trajectory Planning for Unstructured and Partially Occluded Environments
Authors:
Sebastian vom Dorff,
Maximilian Kneissl,
Martin Fränzle
Abstract:
Ensuring safe behavior for automated vehicles in unregulated traffic areas poses a complex challenge for the industry. It is an open problem to provide scalable and certifiable solutions to this challenge. We derive a trajectory planner based on model predictive control which interoperates with a monitoring system for pedestrian safety based on cellular automata. The combined planner-monitor syste…
▽ More
Ensuring safe behavior for automated vehicles in unregulated traffic areas poses a complex challenge for the industry. It is an open problem to provide scalable and certifiable solutions to this challenge. We derive a trajectory planner based on model predictive control which interoperates with a monitoring system for pedestrian safety based on cellular automata. The combined planner-monitor system is demonstrated on the example of a narrow indoor parking environment. The system features deterministic behavior, mitigating the immanent risk of black boxes and offering full certifiability. By using fundamental and conservative prediction models of pedestrians the monitor is able to determine a safe drivable area in the partially occluded and unstructured parking environment. The information is fed to the trajectory planner which ensures the vehicle remains in the safe drivable area at any time through constrained optimization. We show how the approach enables solving plenty of situations in tight parking garage scenarios. Even though conservative prediction models are applied, evaluations indicate a performant system for the tested low-speed navigation.
△ Less
Submitted 30 September, 2021; v1 submitted 9 September, 2021;
originally announced September 2021.
-
Dynamic Conflict Resolution Using Justification Based Reasoning
Authors:
Werner Damm,
Martin Fränzle,
Willem Hagemann,
Paul Kröger,
Astrid Rakow
Abstract:
We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epi…
▽ More
We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epistemic and modal logic, justification and temporal logic. Using this framework, we illustrate how conflicts can be identified and how we derive a chain of justifications leading to this conflict. We discuss how conflict resolution can be done when a vehicle has local, incomplete information, vehicle to vehicle communication (V2V) and partially ordered goals.
△ Less
Submitted 30 October, 2019;
originally announced November 2019.
-
Verifying Reachability Properties in Markov Chains via Incremental Induction
Authors:
Elizabeth Polgreen,
Martin Brain,
Martin Fraenzle,
Alessandro Abate
Abstract:
There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal) Binary Decision Diagrams. These structures are complemented in areas of non-probabilistic verification by more scalable techniques, such as IC3. We present a symbolic probabilistic model checking algorithm based on IC3-l…
▽ More
There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal) Binary Decision Diagrams. These structures are complemented in areas of non-probabilistic verification by more scalable techniques, such as IC3. We present a symbolic probabilistic model checking algorithm based on IC3-like incremental construction of inductive clauses to partition the state space, interleaved with incremental construction of a system of linear inequalities. This paper compares our implementation to standard quantitative verification alternatives: our experiments show that our algorithm is a step to more scalable symbolic verification of rare events in finite-state Markov chains.
△ Less
Submitted 19 September, 2019; v1 submitted 17 September, 2019;
originally announced September 2019.
-
Justification Based Reasoning in Dynamic Conflict Resolution
Authors:
Werner Damm,
Martin Fränzle,
Willem Hagemann,
Paul Kröger,
Astrid Rakow
Abstract:
We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epi…
▽ More
We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epistemic and modal logic, justification and temporal logic. Using this framework, we illustrate how conflicts can be identified and how we derive a chain of justifications leading to this conflict. We discuss how conflict resolution can be done when a vehicle has local, incomplete information, vehicle to vehicle communication (V2V) and partially ordered goals.
△ Less
Submitted 28 May, 2019;
originally announced May 2019.
-
Effective Definability of the Reachability Relation in Timed Automata
Authors:
Martin Fränzle,
Karin Quaas,
Mahsa Shirmohammadi,
James Worrell
Abstract:
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
△ Less
Submitted 23 March, 2019;
originally announced March 2019.
-
Integrating Neurophysiological Sensors and Driver Models for Safe and Performant Automated Vehicle Control in Mixed Traffic
Authors:
Werner Damm,
Martin Fränzle,
Andreas Lüdtke,
Jochem W. Rieger,
Alexander Trende,
Anirudh Unni
Abstract:
In future mixed traffic Highly Automated Vehicles (HAV) will have to resolve interactions with human operated traffic. A particular problem for HAVs is detection of human states influencing safety critical decisions and driving behavior of humans. We demonstrate the value proposition of neurophysiological sensors and driver models for optimizing performance of HAVs under safety constraints in mixe…
▽ More
In future mixed traffic Highly Automated Vehicles (HAV) will have to resolve interactions with human operated traffic. A particular problem for HAVs is detection of human states influencing safety critical decisions and driving behavior of humans. We demonstrate the value proposition of neurophysiological sensors and driver models for optimizing performance of HAVs under safety constraints in mixed traffic applications.
△ Less
Submitted 13 February, 2019;
originally announced February 2019.
-
Costs and Rewards in Priced Timed Automata
Authors:
Martin Fränzle,
Mahsa Shirmohammadi,
Mani Swaminathan,
James Worrell
Abstract:
We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA.
We study the Pareto Domination Problem, which asks whether it is possi…
▽ More
We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA.
We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers.
We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
△ Less
Submitted 15 May, 2018; v1 submitted 5 March, 2018;
originally announced March 2018.
-
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
Authors:
Tino Teige,
Martin Fränzle
Abstract:
The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of Craig interp…
▽ More
The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolation-based approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.
△ Less
Submitted 25 June, 2012; v1 submitted 20 June, 2012;
originally announced June 2012.
