pith. sign in

arxiv: 2606.21516 · v1 · pith:NHUMS7GBnew · submitted 2026-06-19 · 💻 cs.FL

State-Space Abstractions for Parametric Timed Games

Mikael Bisgaard Dahlsen-Jensen (1) , Laure Petrucci (2) , Jaco van de Pol (1) ((1) Aarhus University , Aarhus , Denmark , (2) Universit\'e Sorbonne Paris Nord CNRS , Villetaneuse , France) This is my paper

Pith reviewed 2026-06-26 12:33 UTC · model grok-4.3

classification 💻 cs.FL
keywords parametric timed gamesstate-space abstractionsparameter synthesiswinning strategieszone abstractionstimed automatacontroller synthesis
0
0 comments X

The pith

A general abstraction framework for Parametric Timed Games preserves correctness of parameter synthesis and winning strategies when using standard reductions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines a general abstraction framework for Parametric Timed Games and shows it can be instantiated with double inclusion, zone merging, hull abstractions, and location-based abstraction. It proves these instantiations preserve the ability to synthesize correct parameters and winning strategies. This matters because synthesizing controllers for real-time systems facing both timing uncertainty and adversaries produces state spaces too large for direct exploration. The work demonstrates concrete scalability gains by solving previously intractable cases on a production cell benchmark and a new adversarial IoT case study.

Core claim

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.

What carries the argument

A general abstraction framework for Parametric Timed Games that supports lifting existing abstractions while maintaining properties for parameter synthesis and strategy existence.

If this is right

  • The abstractions significantly improve scalability on production cell and adversarial IoT benchmarks.
  • Instances previously intractable for existing techniques become solvable.
  • Correctness holds simultaneously for parameter synthesis and for existence of winning strategies.
  • The same framework applies uniformly to the four listed abstractions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The framework could serve as a template for adding new abstractions beyond the four tested here.
  • Similar lifting arguments might apply to other parametric game models that combine timing and discrete choices.
  • The resulting smaller state spaces could be combined with existing on-the-fly or symbolic techniques for further gains.

Load-bearing premise

Abstractions developed for non-game parametric timed automata can be lifted to the two-player game setting while preserving the necessary properties for both parameter synthesis and strategy existence.

What would settle it

A concrete Parametric Timed Game example in which applying one of the abstractions (such as zone merging) produces a different set of valid parameters or a different winning strategy than the unabstracted model.

Figures

Figures reproduced from arXiv: 2606.21516 by (2) Universit\'e Sorbonne Paris Nord CNRS, Aarhus, Denmark, France), Jaco van de Pol (1) ((1) Aarhus University, Laure Petrucci (2), Mikael Bisgaard Dahlsen-Jensen (1), Villetaneuse.

Figure 1
Figure 1. Figure 1: Consequence of Lemma 1. Win∗ α[(ℓ ′ , Z′ img)] (light and dark green) extends into the region Z ′ img \ Zimg, but states from Z map only into Zimg (image￾preserving, dashed arrows). Restricted to Zimg, the abstract and full winning sets coincide (dark green), so the predecessor computation restricted to Z recovers exactly Win∗ [(ℓ, Z)]. Role of the abstraction. The abstraction changes only which symbolic s… view at source ↗
Figure 2
Figure 2. Figure 2: Scheduler automaton. device_0 U Init True Waiting True request_incoming_0 queue_push(0, requests); U Granted True grant_0 x_0 <- 0; Transmitting p_active >= x_0 count <- count + 1; x_0 <- 0; Delaying p_max_delay >= x_0 energy > 0 delay_0 count <- count + 1; energy <- energy - 1; x_0 <- 0; Done True p_active = x_0 count <- count - 1; stop_delay_0 x_0 <- 0; energy > 0 delay_0 energy <- energy - 1; x_0 <- 0; … view at source ↗
Figure 3
Figure 3. Figure 3: Device automata (device 0 and device 1). 19 [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Overview of the adversarial IoT scheduling scenario. [PITH_FULL_IMAGE:figures/full_fig_p020_4.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper defines a general abstraction framework for Parametric Timed Games, instantiates it with double inclusion, zone merging, hull, and location-based abstractions from the PTA and TG literature, and supplies explicit proofs that the framework preserves correctness for both parameter synthesis and winning strategies. Experiments on a production cell benchmark and a novel adversarial IoT case study demonstrate improved scalability over prior techniques.

Significance. If the proofs hold, the work is significant: it directly lifts established state-space abstractions to the two-player parametric game setting while preserving the required properties for synthesis and strategies. The explicit proofs and the resolution of the lifting question from non-game PTA/TG settings constitute a clear technical advance, with the reported scalability gains on established and new benchmarks indicating practical utility for controller synthesis under timing uncertainty and adversaries.

minor comments (1)
  1. The experimental section would benefit from a brief table or paragraph clarifying which specific parameter domains or instance sizes became newly solvable due to each abstraction.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept. The review accurately captures the contributions of the general abstraction framework, the correctness proofs for parameter synthesis and strategies, and the experimental improvements on the production cell and IoT benchmarks.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper defines a general abstraction framework for Parametric Timed Games, instantiates it with abstractions (double inclusion, zone merging, hull, location-based) drawn from prior PTA/TG literature, and supplies explicit proofs that the framework preserves correctness of parameter synthesis and winning strategies. These steps are self-contained mathematical arguments and do not reduce by construction to fitted parameters, self-definitions, or load-bearing self-citations. The central claims rest on independent proofs rather than renaming or smuggling ansatzes via author-overlapping citations. This matches the default expectation of a non-circular theoretical contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard mathematical properties of zones and abstractions in timed automata theory; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard properties of zone abstractions and inclusion in timed automata
    Invoked implicitly when lifting abstractions from prior PTA and TG literature.

pith-pipeline@v0.9.1-grok · 5682 in / 1045 out tokens · 24069 ms · 2026-06-26T12:33:54.752336+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 1 canonical work pages

  1. [1]

    Rajeev Alur and David L. Dill. A theory of timed automata.Theoretical Computer Science, 126(2):183–235, 1994

    1994

  2. [2]

    Henzinger, and Moshe Y

    Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. InSTOC, pages 592–601. ACM, 1993

    1993

  3. [3]

    IMITATOR 3: Synthesis of timing parameters beyond decidability

    ´Etienne Andr´ e. IMITATOR 3: Synthesis of timing parameters beyond decidability. InCAV (1), volume 12759 ofLecture Notes in Computer Science, pages 552–565. Springer, 2021

    2021

  4. [4]

    Merge and conquer: State merging in parametric timed automata

    ´Etienne Andr´ e, Laurent Fribourg, and Romain Soulat. Merge and conquer: State merging in parametric timed automata. InATVA, Lecture Notes in Computer Science, pages 381–396. Springer, 2013

    2013

  5. [5]

    ´Etienne Andr´ e, Didier Lime, and Olivier H. Roux. Integer-complete synthesis for bounded parametric timed automata. InRP, volume 9328 ofLecture Notes in Computer Science, pages 7–19. Springer, 2015

    2015

  6. [6]

    Efficient convex zone merging in parametric timed automata

    ´Etienne Andr´ e, Dylan Marinho, Laure Petrucci, and Jaco van de Pol. Efficient convex zone merging in parametric timed automata. InFORMATS, volume 13465 ofLecture Notes in Computer Science, pages 200–218. Springer, 2022

    2022

  7. [7]

    Zone extrapolations in parametric timed au- tomata

    Johan Arcile and ´Etienne Andr´ e. Zone extrapolations in parametric timed au- tomata. InNFM, Lecture Notes in Computer Science, pages 451–469. Springer, 2022

    2022

  8. [8]

    Hill, and Enea Zaffanella

    Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and ver- ification of hardware and software systems.Sci. Comput. Program., 72(1-2):3–21, 2008

    2008

  9. [9]

    Approximate reachability analysis of timed automata

    Felice Balarin. Approximate reachability analysis of timed automata. InRTSS, pages 52–61. IEEE Computer Society, 1996

    1996

  10. [10]

    Lower and upper bounds in zone based abstractions of timed automata

    Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pel´ anek. Lower and upper bounds in zone based abstractions of timed automata. InTACAS, Lecture Notes in Computer Science, pages 312–326. Springer, 2004

    2004

  11. [11]

    LTL parameter synthe- sis of parametric timed automata

    Peter Bezdek, Nikola Benes, Jiri Barnat, and Ivana Cern´ a. LTL parameter synthe- sis of parametric timed automata. InSEFM, Lecture Notes in Computer Science, pages 172–187. Springer, 2016

    2016

  12. [12]

    Efficient on-the-fly algorithms for the analysis of timed games

    Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In CONCUR, Lecture Notes in Computer Science, pages 66–80. Springer, 2005

    2005

  13. [13]

    Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InPOPL, pages 238–252. ACM, 1977

    1977

  14. [14]

    Automatic discovery of linear restraints among variables of a program

    Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. InPOPL, pages 84–96. ACM Press, 1978

    1978

  15. [15]

    Saßnick and C

    Mikael B. Dahlsen-Jensen, Laure Petrucci, and J.C. van de Pol. Artifact for ”state-space abstractions for parametric timed games”. Zenodo, 10.5281/zen- odo.19680181, April 2026

    work page doi:10.5281/zen- 2026

  16. [16]

    On-the-fly algorithm for reachability in parametric timed games

    Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, and Jaco van de Pol. On-the-fly algorithm for reachability in parametric timed games. InTACAS (3), Lecture Notes in Computer Science, pages 194–212. Springer, 2024

    2024

  17. [17]

    Controller synthesis for parametric timed games

    Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, and Jaco van de Pol. Controller synthesis for parametric timed games. InQEST+FORMATS, Lecture Notes in Computer Science, pages 314–332. Springer, 2025. 17

    2025

  18. [18]

    Three-valued abstrac- tions of games: Uncertainty, but with precision

    Luca de Alfaro, Patrice Godefroid, and Radha Jagadeesan. Three-valued abstrac- tions of games: Uncertainty, but with precision. InLICS, pages 170–179. IEEE Computer Society, 2004

    2004

  19. [19]

    David L. Dill. Timing assumptions and verification of finite-state concurrent sys- tems. InAutomatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, pages 197–212. Springer, 1989

    1989

  20. [20]

    Henzinger, Rupak Majumdar, Freddy Y

    Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, and Jean-Fran¸ cois Raskin. Abstract interpretation of game properties. InSAS, Lecture Notes in Computer Science, pages 220–239. Springer, 2000

    2000

  21. [21]

    Vaandrager

    Thomas Hune, Judi Romijn, Mari¨ elle Stoelinga, and Frits W. Vaandrager. Lin- ear parametric model checking of timed automata. InTACAS, Lecture Notes in Computer Science, pages 189–203. Springer, 2001

    2001

  22. [22]

    Jensen, Kim G

    Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jir´ ı Srba. On-the-fly symbolic algorithm for timed ATL with abstractions. InCONCUR, volume 348 ofLIPIcs, pages 25:1–25:19. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2025

    2025

  23. [23]

    Aleksandra Jovanovic, S´ ebastien Faucou, Didier Lime, and Olivier H. Roux. Real- time control with parametric timed reachability games. InIFAC WODES, pages 323–330. Elseviers, 2012

    2012

  24. [24]

    Aleksandra Jovanovic, Didier Lime, and Olivier H. Roux. A game approach to the parametric control of real-time systems.Int. J. Control, 92(9):2025–2036, 2019

    2025

  25. [25]

    UPPAAL in a nutshell

    Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf., 1(1-2):134–152, 1997

    1997

  26. [26]

    production cell

    Claus Lewerentz and Thomas Lindner.Case study “production cell”: A compara- tive study in formal specification and verification, pages 388–416. Springer Berlin Heidelberg, Berlin, Heidelberg, 1995

    1995

  27. [27]

    On the synthesis of discrete con- trollers for timed systems

    Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete con- trollers for timed systems. In Ernst W. Mayr and Claude Puech, editors,STACS 95, pages 229–242, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg

    1995

  28. [28]

    The octagon abstract domain

    Antoine Min´ e. The octagon abstract domain. InWCRE, page 310. IEEE Computer Society, 2001

    2001

  29. [29]

    Synthia: Verification and synthesis for timed automata

    Hans-J¨ org Peter, R¨ udiger Ehlers, and Robert Mattm¨ uller. Synthia: Verification and synthesis for timed automata. InCAV, Lecture Notes in Computer Science, pages 649–655. Springer, 2011. 18 A Case Study Model Figs. 2 and 3 show the IMITATOR models for the two-device instance of the Malicious Synchronization case study. Urgent locations (U, yellow) dis...

    2011