arXiv subjects

Mikael Bisgaard Dahlsen-Jensen

Publications and source records attributed to Mikael Bisgaard Dahlsen-Jensen.

4 recordsLinked to original sources

arXiv2026

Random Generation of Small Quantitative Automata for Algorithm Debugging

Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches -- benchmarks, mutation testing, uniform random generation -- each fail to expose subtle implementation bugs. We present a framework that repeatedly 1) generates random quantitative automata that are non-degenerate by construction, 2) tests each against a target property, and 3) shrinks any violation to a local minimum, yielding a small, actionable counterexample. We implement the framework for parametric timed automata (PTA) and apply it to IMITATOR, a mature model checker for PTA, uncovering 5 previously unknown bugs, one of which was exposed by a counterexample with just 2 locations and 1 transition.

cs.FL↗

arXiv2026

State-Space Abstractions for Parametric Timed Games

Synthesizing controllers for real-time systems under both timing uncertainty and adversarial environments requires exploring prohibitively large symbolic state spaces. While zone inclusion checking has been applied to Parametric Timed Games, more aggressive abstractions from the Parametric Timed Automata and Timed Games literature -- double inclusion, zone merging, hull abstractions, and location-based abstraction -- have not yet been lifted to the parametric game setting. We define a general abstraction framework for Parametric Timed Games, instantiate it with each of the aforementioned abstractions, and prove that the framework preserves correctness of parameter synthesis and winning strategies. Experimental results on an established production cell benchmark and a novel adversarial IoT case study show that the abstractions significantly improve scalability, solving instances previously intractable for existing techniques.

cs.FL↗

arXiv2025

Controller Synthesis for Parametric Timed Games

We present a (semi)-algorithm to compute winning strategies for parametric timed games. Previous algorithms only synthesized constraints on the clock parameters for which the game is winning. A new definition of (winning) strategies is proposed, and ways to compute them. A transformation of these strategies to (parametric) timed automata allows for building a controller enforcing them. The feasibility of the method is demonstrated by an implementation and experiments for the Production Cell case study.

cs.FL↗

arXiv2024

On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)

Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations ``in the limit''.

cs.FL↗