4 citations · 22 across the 18 of their papers we have counts for
19 papers
Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking
Janis Kröger, Paul Kröger, Martin Fränzle
Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge d…
Stream-based Online and Offline Monitoring under Measurement Noise
Bernd Finkbeiner, Martin Fränzle, Florian Kohn +1
Stream-based monitoring is a runtime verification approach for cyber-physical systems that translates streams of input data, such as sensor readings, into streams of aggregate stat…
Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment
S. Bensalem, Y. Dong, M. Franzle +6
This position paper argues that enforcing LLM agent safety within a single abstraction layer is not merely suboptimal but categorically insufficient for deployed LLM agents -- a st…
Cutting Corners on Uncertainty: Zonotope Abstractions for Stream-based Runtime Monitoring
Bernd Finkbeiner, Martin Fränzle, Florian Kohn +1
Stream-based monitoring assesses the health of safety-critical systems by transforming input streams of sensor measurements into output streams that determine a verdict. These inpu…
Counterfactual-based Root Cause Analysis for Dynamical Systems
Juliane Weilbach, Sebastian Gerwinn, Karim Barsim +1
Identifying the underlying reason for a failing dynamic process or otherwise anomalous observation is a fundamental challenge, yet has numerous industrial applications. Identifying…
Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays
Martin Fränzle, Thomas M. Grosen, Kim G. Larsen +1
Timed Büchi automata provide a very expressive formalism for expressing requirements of real-time systems. Online monitoring and active testing of embedded real-time systems can th…
Estimation of Counterfactual Interventions under Uncertainties
Juliane Weilbach, Sebastian Gerwinn, Melih Kandemir +1
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…
Safety Shielding under Delayed Observation
Filip Cano Córdoba, Alexander Palmisano, Martin Fränzle +2
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…
On the Existence of Reactive Strategies Resilient to Delay
Martin Fränzle, Paul Kröger, Sarah Winter +1
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 suff…
Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach
Björn Koopmann, Stefan Puch, Günter Ehmen +1
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…
Reach-avoid Verification Based on Convex Optimization
Bai Xue, Naijun Zhan, Martin Fränzle +2
In this paper we propose novel optimization-based methods for verifying reach-avoid (or, eventuality) properties of continuous-time systems modelled by ordinary differential equati…
Reach-Avoid Analysis for Polynomial Stochastic Differential Equations
Bai Xue, Naijun Zhan, Martin Fränzle
In this paper we propose a novel semi-definite programming approach that solves reach-avoid problems over open (i.e., not bounded a priori) time horizons for dynamical systems mode…
Verification of Sigmoidal Artificial Neural Networks using iSAT
Dominik Grundt, Sorin Liviu Jurj, Willem Hagemann +2
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…
Phase transition in the bipartite z-matching
Till Kahlke, Martin Fränzle, Alexander K. Hartmann
We study numerically the maximum -matching problems on ensembles of bipartite random graphs. The -matching problems describes the matching between two types of nodes, users a…
Safe, Deterministic Trajectory Planning for Unstructured and Partially Occluded Environments
Sebastian vom Dorff, Maximilian Kneissl, Martin Fränzle
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 sol…
Dynamic Conflict Resolution Using Justification Based Reasoning
Werner Damm, Martin Fränzle, Willem Hagemann +2
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 l…
Integrating Neurophysiological Sensors and Driver Models for Safe and Performant Automated Vehicle Control in Mixed Traffic
Werner Damm, Martin Fränzle, Andreas Lüdtke +3
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 in…
Costs and Rewards in Priced Timed Automata
Martin Fränzle, Mahsa Shirmohammadi, Mani Swaminathan +1
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) an…
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
Tino Teige, Martin Fränzle
The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability t…