pith. sign in

arxiv: 2310.09109 · v6 · submitted 2023-10-13 · 💻 cs.LO

Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata

\'Etienne Andr\'e , Didier Lime , Olivier H. Roux This is my paper

Pith reviewed 2026-05-24 06:36 UTC · model grok-4.3

classification 💻 cs.LO
keywords parametric timed automataparameter synthesisunderapproximationreachabilityextrapolationunavoidabilitytimed automata
0
0 comments X

The pith

Parametric extrapolation produces symbolic sets containing all integer reachability solutions and their convex combinations for bounded parametric timed automata.

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

The paper develops a synthesis technique for finding timing parameter values that make certain locations reachable in parametric timed automata. It focuses on bounded parameter domains and uses a new extrapolation step to generate underapproximations that are dense: they include every integer valuation that works and every convex combination of those integers. This matters because most synthesis problems for these models are undecidable and do not terminate, yet the new operator yields terminating procedures that can get arbitrarily close to the full solution set. The same framework also produces algorithms for unavoidability and for preserving untimed behavior relative to a reference valuation.

Core claim

A parametric extrapolation operator applied to bounded parametric timed automata yields symbolic sets of parameter valuations that contain every integer point ensuring reachability together with every convex combination of those integer points, thereby forming a dense integer-complete underapproximation of the solution set.

What carries the argument

The parametric extrapolation operator, which lifts the classical extrapolation of timed automata to the parametric case so that the resulting symbolic sets are closed under convex combination of integer solutions.

If this is right

  • Terminating synthesis becomes possible for reachability in any bounded parametric timed automaton.
  • The same operator produces terminating algorithms that synthesize parameters guaranteeing unavoidability of a location.
  • The operator also yields terminating synthesis for parameter valuations that preserve the untimed behavior of a reference valuation.
  • The returned symbolic sets can be refined to approximate the complete solution set to any desired precision.

Where Pith is reading between the lines

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

  • The density property may allow direct use of the output sets inside convex optimization routines without further discretization.
  • The method could be combined with existing semi-algorithms for unbounded domains by first restricting to a large enough box and then checking boundary behavior.
  • Because the result is closed under convex combination, any linear objective over the parameter space can be optimized directly on the returned symbolic sets.

Load-bearing premise

The timing parameters must lie inside an explicitly bounded domain.

What would settle it

A concrete bounded parametric timed automaton together with an integer valuation that ensures reachability yet is excluded from the symbolic set returned by the extrapolation.

Figures

Figures reproduced from arXiv: 2310.09109 by Didier Lime, \'Etienne Andr\'e, Olivier H. Roux.

Figure 1
Figure 1. Figure 1: Motivating PTA the number of possible symbolic states. Let us first show that this does not hold anymore over rational-valued parameters, which motivates the use of an extrapolation. Example 2. Consider the PTA in [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example illustrating the non-convex parametric extrapolation consists in unconstraining variable ν. The result Cylν (C) for a polyhedron C is a polyhedron: one just need to project out variable ν (e.g., with the Fourier-Motzkin algorithm), and then add it back unconstrained. 3.1.1. Defining extrapolation. Let us first introduce our concept of (M, x)-extrapolation for a single clock. Definition 7 ((M, x)-ex… view at source ↗
Figure 3
Figure 3. Figure 3: Counter-example to the density of the result of IAF. The first case must happen at least once, otherwise by Lemma 1 we have a deadlocked run in v(A) never reaching G. Therefore we have v ∈ Klive at the end of the foreach loop, and for all successors we have v either in Kgood or in Kblock . It follows that v is in the returned value of K. Example 7. Consider the PTA in [PITH_FULL_IMAGE:figures/full_fig_p01… view at source ↗
Figure 4
Figure 4. Figure 4: Example for which RITP terminates but not TP ℓ1 ℓ2 ℓ3 x ≤ 2p x = 1 x ← 0 x = 1 ∧ x ≤ p x ← 0 p = x = q − 1 [PITH_FULL_IMAGE:figures/full_fig_p021_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Example illustrating the need of IH in the result of RITP needed, because both clocks are always ≤ 5 due to the invariants and the bounded parameter domain); in Fig. 4b, we give two such sets of parameter valuations, i.e., 6p2 ≥ 5p1 and 7p2 ≥ 6p1, that indeed contain the same set of integer points within [0, 5]2 , and hence the integer hull (of their extrapolation) is equal.5 Eventually, RITP returns 0 ≤ p… view at source ↗
Figure 6
Figure 6. Figure 6: Example illustrating the need for an integer valuation in RITP When visiting ℓ2 for the second time (via the self-loop over ℓ2), the associated set of valuations C′ 2 is: 1 ≤ p ≤ 2. Observe that IH(C2) = IH(C′ 2 ). Therefore, RITP does not explore the successors of C′ 2 ; if RITP returned C↓P at line 3, then the result would be q = p + 1 ∧ 1 2 ≤ p ≤ 1—which is wrong. Now, RITP actually returns  IH ExtM X … view at source ↗
Figure 7
Figure 7. Figure 7: A PTA s.t. IEF ℓ4 is false and EF and RIEF give a ∈ [ 1 4 , 1 3 ] and b ∈ [ 1 4 , 1 3 ] and b ≥ a that the system does not reach a deadline violation.6 Algorithm EF does not terminate. Algorithm IEF produces the set of parameter valuations a ≥ 34∧b ≥ 10∧a−b ≥ 24 in 13.5 s, while algorithm RIEF produces the set of parameter valuations a > 562 17 ∧b ≥ 10∧a−b > 392 17 in 14.3 s. As illustrated here, the resul… view at source ↗
read the original abstract

Ensuring the correctness of critical real-time systems, involving concurrent behaviours and timing requirements, is crucial. Timed automata extend finite-state automata with clocks, compared in guards and invariants with integer constants. Parametric timed automata (PTAs) extend timed automata with timing parameters. Parameter synthesis aims at computing dense sets of valuations for the timing parameters, guaranteeing a good behaviour. However, in most cases, the emptiness problem for reachability (i.e., the emptiness of the parameter valuations set for which some location is reachable) is undecidable for PTAs and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of symbolic sets of valuations containing not only all the integer points ensuring reachability, but also all the (non-necessarily integer) convex combinations of these integer points, for general PTAs with a bounded parameter domain. We also propose two further algorithms synthesizing parameter valuations guaranteeing unavoidability, and preservation of the untimed behaviour w.r.t. a reference parameter valuation, respectively. Our algorithms terminate and can output sets of valuations arbitrarily close to the complete result. We demonstrate their applicability and efficiency using the tools Rom\'eo and IMITATOR on several benchmarks.

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 / 3 minor

Summary. The paper claims that a parametric extrapolation yields a terminating algorithm producing a dense integer-complete underapproximation (symbolic sets containing all integer valuations ensuring reachability together with all their convex combinations) for general PTAs over bounded parameter domains. It further claims two additional terminating algorithms for unavoidability synthesis and untimed-behavior preservation, with outputs refinable to arbitrary closeness, and demonstrates the approach on benchmarks via Romeo and IMITATOR.

Significance. If the claims hold, the result is significant: it supplies sound, terminating underapproximations with a strong density guarantee (integer points plus convex hull) precisely where full synthesis is undecidable, while respecting the explicit bounded-domain prerequisite. Credit is due for the algorithmic construction that avoids circularity, the termination guarantee, and the reproducible tool-based evaluation.

minor comments (3)
  1. [§3] §3 (parametric extrapolation definition): the transition from the integer-point set to the symbolic convex-combination representation would benefit from an explicit small example immediately after the formal definition to improve readability.
  2. [Table 1] Table 1 (benchmark results): the column reporting distance to the exact set should include the precise metric used (e.g., Hausdorff distance on the parameter space) rather than a qualitative label.
  3. [§4] The proof of termination for the extrapolation operator (likely in §4) relies on the boundedness assumption; a short remark on why the same construction fails without boundedness would clarify the scope without lengthening the text.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, recognition of the significance of the result, and recommendation of minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a parametric extrapolation operator as an algorithmic construction for bounded PTAs, deriving terminating synthesis procedures that produce sound underapproximations containing integer points and their convex combinations. No equations or claims reduce the result to a fitted quantity defined from the same data, a self-citation chain, or a renamed known result; the central claims rest on the explicit definition of the extrapolation and its termination properties within the stated bounded-domain scope, making the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the assumption that the parameter domain is bounded; no free parameters or invented entities are mentioned in the abstract.

axioms (1)
  • domain assumption Parameter domain is bounded
    Required for the extrapolation to guarantee the dense integer-complete underapproximation.

pith-pipeline@v0.9.0 · 5764 in / 1063 out tokens · 20122 ms · 2026-05-24T06:36:31.045503+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

37 extracted references · 37 canonical work pages

  1. [1]

    Zone extrapolations in parametric timed automata

    Johan Arcile and \'E tienne Andr \'e . Zone extrapolations in parametric timed automata. In Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez, editors, NFM , volume 13260 of , pages 451--469. Springer, 2022. https://doi.org/10.1007/978-3-031-06773-0_24 doi:10.1007/978-3-031-06773-0_24

    work page doi:10.1007/978-3-031-06773-0_24 2022

  2. [2]

    An inverse method for parametric timed automata

    \'E tienne Andr \'e , Th omas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science , 20(5):819--836, 10 2009. https://doi.org/10.1142/S0129054109006905 doi:10.1142/S0129054109006905

    work page doi:10.1142/s0129054109006905 2009

  3. [3]

    Rajeev Alur and David L. Dill. A theory of timed automata. , 126(2):183--235, April 1994. https://doi.org/10.1016/0304-3975(94)90010-8 doi:10.1016/0304-3975(94)90010-8

    work page doi:10.1016/0304-3975(94)90010-8 1994

  4. [4]

    Liveness in L/U-Parametric Timed Automata

    Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC , pages 592--601, New York, NY, USA, 1993. ACM. https://doi.org/10.1145/167088.167242 doi:10.1145/167088.167242

    work page doi:10.1145/167088.167242 1993

  5. [5]

    Language preservation problems in parametric timed automata

    \'E tienne Andr \'e , Didier Lime, and Nicolas Markey. Language preservation problems in parametric timed automata. , 16, 1 2020. URL: https://lmcs.episciences.org/6042

    work page 2020

  6. [6]

    \'E tienne Andr \'e , Didier Lime, and Olivier H. Roux. Integer-complete synthesis for bounded parametric timed automata. In Miko aj Boja\'nczyk, S awomir Lasota, and Igor Potapov, editors, RP , volume 9328 of , pages 7--19. Springer, 9 2015. https://doi.org/10.1007/978-3-319-24537-9_2 doi:10.1007/978-3-319-24537-9_2

    work page doi:10.1007/978-3-319-24537-9_2 2015

  7. [7]

    TCTL model checking lower/upper-bound parametric timed automata without invariants

    \'E tienne Andr \'e , Didier Lime, and Mathias Ramparison. TCTL model checking lower/upper-bound parametric timed automata without invariants. In David N. Jansen and Pavithra Prabhakar, editors, FORMATS , volume 11022 of , pages 1--17. Springer, 2018. https://doi.org/10.1007/978-3-030-00151-3_3 doi:10.1007/978-3-030-00151-3_3

    work page doi:10.1007/978-3-030-00151-3_3 2018

  8. [8]

    \'E tienne Andr \'e , Didier Lime, and Olivier H. Roux. Reachability and liveness in parametric timed automata. , 18(1):31:1--31:41, February 2022. URL: https://lmcs.episciences.org/9070/pdf, https://doi.org/10.46298/lmcs-18(1:31)2022 doi:10.46298/lmcs-18(1:31)2022

    work page doi:10.46298/lmcs-18(1:31)2022 2022

  9. [9]

    Efficient convex zone merging in parametric timed automata

    \'E tienne Andr \'e , Dylan Marinho, Laure Petrucci, and Jaco van de Pol. Efficient convex zone merging in parametric timed automata. In Sergiy Bogomolov and David Parker, editors, FORMATS , volume 13465 of , pages 1--19. Springer, 2022. https://doi.org/10.1007/978-3-031-15839-1_12 doi:10.1007/978-3-031-15839-1_12

    work page doi:10.1007/978-3-031-15839-1_12 2022

  10. [10]

    What's decidable about parametric timed automata? , 21(2):203--219, 4 2019

    \'E tienne Andr \'e . What's decidable about parametric timed automata? , 21(2):203--219, 4 2019. https://doi.org/10.1007/s10009-017-0467-0 doi:10.1007/s10009-017-0467-0

    work page doi:10.1007/s10009-017-0467-0 2019

  11. [11]

    IMITATOR 3: Synthesis of timing parameters beyond decidability

    \'E tienne Andr \'e . IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva, editors, CAV , volume 12759 of , pages 1--14. Springer, 2021. https://doi.org/10.1007/978-3-030-81685-8_26 doi:10.1007/978-3-030-81685-8_26

    work page doi:10.1007/978-3-030-81685-8_26 2021

  12. [12]

    Precise robustness analysis of time P etri nets with inhibitor arcs

    \'E tienne Andr \'e , Laure Petrucci, and Giuseppe Pellegrino. Precise robustness analysis of time P etri nets with inhibitor arcs. In V\'ictor Braberman and Laurent Fribourg, editors, FORMATS , volume 8053 of , pages 1--15. Springer, 8 2013. https://doi.org/10.1007/978-3-642-40229-6_1 doi:10.1007/978-3-642-40229-6_1

    work page doi:10.1007/978-3-642-40229-6_1 2013

  13. [13]

    LTL parameter synthesis of parametric timed automata

    Peter Bezděk, Nikola Bene s , Ji r \'i Barnat, and Ivana C erná. LTL parameter synthesis of parametric timed automata. In Rocco De Nicola and eva K \" u hn, editors, SEFM , volume 9763 of , pages 172--187. Springer, 2016. https://doi.org/10.1007/978-3-319-41591-8_12 doi:10.1007/978-3-319-41591-8_12

    work page doi:10.1007/978-3-319-41591-8_12 2016

  14. [14]

    Lower and upper bounds in zone-based abstractions of timed automata

    Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pel \' a nek. Lower and upper bounds in zone-based abstractions of timed automata. , 8(3):204--215, 2006. https://doi.org/10.1007/s10009-005-0190-0 doi:10.1007/s10009-005-0190-0

    work page doi:10.1007/s10009-005-0190-0 2006

  15. [15]

    Com- parison of the Expressiveness of Timed Au- tomata and Time Petri Nets

    Nikola Bene s , Peter Bezd e k, Kim Gulstrand Larsen, and Ji r \'i Srba. Language emptiness of continuous-time parametric timed automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP, Part II , volume 9135 of , pages 69--81. Springer, July 2015. https://doi.org/10.1007/978-3-662-47666-6_6 doi:10.1007/978-3-...

    work page doi:10.1007/978-3-662-47666-6_6 2015

  16. [16]

    Durations and parametric model-checking in timed automata

    Véronique Bruyère, Emmanuel Dall'Olio, and Jean-Francois Raskin. Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic , 9(2):12:1--12:23, 2008. https://doi.org/10.1145/1342991.1342996 doi:10.1145/1342991.1342996

    work page doi:10.1145/1342991.1342996 2008

  17. [17]

    Timed State Spac e Analysis of Real-Time Preemptive Systems

    Giacomo Bucci, Andrea Fedeli, Luigi Sassoli, and Enrico Vicario. Timed state space analysis of real-time preemptive systems. , 30(2):97--111, 2004. https://doi.org/10.1109/TSE.2004.1265815 doi:10.1109/TSE.2004.1265815

    work page doi:10.1109/tse.2004.1265815 2004

  18. [18]

    Srivathsan

    Patricia Bouyer, Paul Gastin, Frédéric Herbreteau, Ocan Sankur, and B. Srivathsan. Zone-based verification of timed automata: Extrapolations, simulations and what next? In Sergiy Bogomolov and David Parker, editors, FORMATS , volume 13465 of , pages 16--42. Springer, 2022. https://doi.org/10.1007/978-3-031-15839-1_2 doi:10.1007/978-3-031-15839-1_2

    work page doi:10.1007/978-3-031-15839-1_2 2022

  19. [19]

    Hill, and Enea Zaffanella

    Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The P arma P olyhedra L ibrary: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming , 72(1--2):3--21, 2008. https://doi.org/10.1016/j.scico.2007.08.001 doi:10.1016/j.scico.2007.08.001

    work page doi:10.1016/j.scico.2007.08.001 2008

  20. [20]

    Decision problems for lower/upper bound parametric timed automata

    Laura Bozzelli and Salvatore La Torre . Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design , 35(2):121--151, 2009

    work page 2009

  21. [21]

    Real-Time Model-Checking: Parameters ev- erywhere

    Daniel Bundala and Joël Ouaknine. Advances in parametric real-time reasoning. In Erzs \' e bet Csuhaj - Varj \' u , Martin Dietzfelbinger, and Zolt \' a n \' E sik, editors, MFCS, Part I , volume 8634 of , pages 123--134. Springer, 2014. https://doi.org/10.1007/978-3-662-44522-8 doi:10.1007/978-3-662-44522-8

    work page doi:10.1007/978-3-662-44522-8 2014

  22. [22]

    Real-time model-checking: Parameters everywhere

    V \'e ronique Bruy \`e re and Jean-Fran c ois Raskin. Real-time model-checking: Parameters everywhere. Logical Methods in Computer Science , 3(1:7):1--30, 2007. https://doi.org/10.2168/LMCS-3(1:7)2007 doi:10.2168/LMCS-3(1:7)2007

    work page doi:10.2168/lmcs-3(1:7)2007 2007

  23. [23]

    State class constructions for branching analysis of time P etri nets

    Bernard Berthomieu and François Vernadat. State class constructions for branching analysis of time P etri nets. In Hubert Garavel and John Hatcliff, editors, TACAS , volume 2619 of , pages 442--457. Springer, 2003. https://doi.org/10.1007/3-540-36577-X_33 doi:10.1007/3-540-36577-X_33

    work page doi:10.1007/3-540-36577-x_33 2003

  24. [24]

    Timed automata: Semantics, algorithms and tools

    Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Jöörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and P etri Nets, Advances in P etri Nets , volume 3098 of , pages 87--124. Springer, 2003. https://doi.org/10.1007/978-3-540-27755-2_3 doi:10.1007/978-3-540-27755-2_3

    work page doi:10.1007/978-3-540-27755-2_3 2003

  25. [25]

    Robust parametric reachability for timed automata

    Laurent Doyen. Robust parametric reachability for timed automata. , 102(5):208--213, 2007. https://doi.org/10.1016/j.ipl.2006.11.018 doi:10.1016/j.ipl.2006.11.018

    work page doi:10.1016/j.ipl.2006.11.018 2007

  26. [26]

    Model checking of real-time reachability properties using abstractions

    Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. In Bernhard Steffen, editor, TACAS , volume 1384 of , pages 313--329. Springer, 1998. https://doi.org/10.1007/BFb0054180 doi:10.1007/BFb0054180

    work page doi:10.1007/bfb0054180 1998

  27. [27]

    Reachability in two-parametric timed automata with one parameter is EXPSPACE -complete

    Stefan Göller and Mathieu Hilaire. Reachability in two-parametric timed automata with one parameter is EXPSPACE -complete. In Markus Bläser and Benjamin Monmege, editors, STACS , volume 187 of LIPIcs , pages 36:1--36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. https://doi.org/10.4230/LIPIcs.STACS.2021.36 doi:10.4230/LIPIcs.STACS.2021.36

    work page doi:10.4230/lipics.stacs.2021.36 2021

  28. [28]

    Verification of linear hybrid systems by means of convex approximations

    Nicolas Halbwachs, Yann - Éric Proy, and Pascal Raymond. Verification of linear hybrid systems by means of convex approximations. In Baudouin Le Charlier, editor, SAS , volume 864 of , pages 223--237. Springer, 1994. https://doi.org/10.1007/3-540-58485-4_43 doi:10.1007/3-540-58485-4_43

    work page doi:10.1007/3-540-58485-4_43 1994

  29. [29]

    Vaandrager

    Thomas Hune, Judi Romijn, Mari \"e lle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. , 52-53:183--220, 2002. https://doi.org/10.1016/S1567-8326(02)00037-1 doi:10.1016/S1567-8326(02)00037-1

    work page doi:10.1016/s1567-8326(02)00037-1 2002

  30. [30]

    Srivathsan, and Igor Walukiewicz

    Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Lazy abstractions for timed automata. In Natasha Sharygina and Helmut Veith, editors, CAV , volume 8044 of , pages 990--1005. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_71 doi:10.1007/978-3-642-39799-8_71

    work page doi:10.1007/978-3-642-39799-8_71 2013

  31. [31]

    Srivathsan, and Igor Walukiewicz

    Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. Information and Computation , 251:67--90, 2016. https://doi.org/10.1016/j.ic.2016.07.004 doi:10.1016/j.ic.2016.07.004

    work page doi:10.1016/j.ic.2016.07.004 2016

  32. [32]

    Aleksandra Jovanovi \'c , Didier Lime, and Olivier H. Roux. Integer parameter synthesis for real-time systems. , 41(5):445--461, 2015. https://doi.org/10.1109/TSE.2014.2357445 doi:10.1109/TSE.2014.2357445

    work page doi:10.1109/tse.2014.2357445 2015

  33. [33]

    UPPAAL in a Nutshell

    Didier Lime, Olivier H. Roux, Charlotte Seidner, and Louis-Marie Traonouez. R omeo: A parametric model-checker for P etri nets with stopwatches. In Stefan Kowalewski and Anna Philippou, editors, TACAS , volume 5505 of , pages 54--57. Springer, March 2009. https://doi.org/10.1007/978-3-642-00768-2_6 doi:10.1007/978-3-642-00768-2_6

    work page doi:10.1007/978-3-642-00768-2_6 2009

  34. [34]

    A study of the recov- erability of computing systems

    Nicolas Markey. Robustness in real-time systems. In Iain Bate and Roberto Passerone, editors, SIES , pages 28--34. IEEE Computer Society Press, June 2011. https://doi.org/10.1109/SIES.2011.5953652 doi:10.1109/SIES.2011.5953652

    work page doi:10.1109/sies.2011.5953652 2011

  35. [35]

    Joseph S. Miller. Decidability and complexity results for timed automata and semi-linear hybrid automata. In Nancy A. Lynch and Bruce H. Krogh, editors, HSCC , volume 1790 of , pages 296--309. Springer, 2000. https://doi.org/10.1007/3-540-46430-1_26 doi:10.1007/3-540-46430-1_26

    work page doi:10.1007/3-540-46430-1_26 2000

  36. [36]

    Theory of linear and integer programming

    Alexander Schrijver. Theory of linear and integer programming . John Wiley & Sons, Inc., New York, NY, USA, 1986

    work page 1986

  37. [37]

    Parametric timing analysis for real-time systems

    Farn Wang. Parametric timing analysis for real-time systems. Information and Computation , 130(2):131--150, 1996. https://doi.org/10.1006/inco.1996.0086 doi:10.1006/inco.1996.0086

    work page doi:10.1006/inco.1996.0086 1996