pith. sign in

arxiv: 1907.01721 · v1 · pith:3FRERIMGnew · submitted 2019-07-03 · 💻 cs.LO · cs.FL

What's decidable about parametric timed automata?

\'Etienne Andr\'e This is my paper

Pith reviewed 2026-05-25 10:10 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords parametric timed automatadecidabilityundecidabilityreal-time systemsformal verificationmodel checking
0
0 comments X

The pith

After 25 years, non-trivial problems for parametric timed automata are undecidable unless clocks or parameters are restricted.

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

The paper surveys decision problems for parametric timed automata, a model for verifying real-time systems with unknown constants. It establishes that general PTAs render most studied problems undecidable. Certain restrictions restore decidability: limiting the number of clocks, restricting how clocks are compared to parameters, and limiting parameters to upper or lower bounds only. The survey also covers related models like parametric hybrid automata and available tools, while listing open questions.

Core claim

Any non-trivial problem studied for parametric timed automata is undecidable in the general case, yet decidability returns when the number of clocks is bounded, when parameters are used only as bounds, or when the domain of parameters is restricted.

What carries the argument

Parametric timed automata, with the boundary between decidable and undecidable cases determined by restrictions on the number of clocks, clock-parameter comparisons, and parameter usage as bounds.

If this is right

  • Verification of real-time systems modeled as PTAs requires imposing bounds on clocks or parameters to obtain decidable procedures.
  • Some reachability and synthesis problems become decidable when parameters appear only as upper bounds.
  • Tools must incorporate these restrictions or risk operating in undecidable fragments.
  • Related formalisms such as parametric interrupt timed automata may inherit similar decidability boundaries.

Where Pith is reading between the lines

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

  • Developers of real-time verification tools can prioritize implementations for the decidable fragments identified.
  • Open problems listed in the survey point to potential new decidable subclasses that could be explored by varying modeling choices beyond the surveyed restrictions.

Load-bearing premise

The problems surveyed are representative of non-trivial questions and the listed restrictions capture the main factors that separate decidable from undecidable cases.

What would settle it

A proof that some non-trivial verification problem remains decidable for PTAs with an arbitrary number of clocks and unrestricted parameter use would falsify the central claim.

Figures

Figures reproduced from arXiv: 1907.01721 by \'Etienne Andr\'e.

Figure 1
Figure 1. Figure 1: A coffee machine modeled using a PTA i. e., a set of alternating locations and actions. This is a nonstandard definition of traces (compared to e. g., [Gla90]), but we keep this term as it is used in, e. g., [And+09; AM15]. A symbolic semantics is also defined for PTAs in [Hun+02; And+09; JLR15] as a parametric zone graph, where a symbolic state is made of a discrete part (the current location) and a symbo… view at source ↗
read the original abstract

Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well-understood that any non-trivial problem studied is undecidable for general PTAs. We provide here a survey of decision and computation problems for PTAs. On the one hand, bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability. On the other hand, restricting the number of clocks, the use of clocks (compared or not with the parameters), and the use of parameters (e.g. used only as upper or lower bounds) leads to decidability of some problems. We also put emphasis on open problems. We also discuss formalisms close to parametric timed automata (such as parametric hybrid automata or parametric interrupt timed automata), and we study tools dedicated to PTAs and their extensions.

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

2 major / 2 minor

Summary. The paper surveys decision and computation problems for parametric timed automata (PTAs). It claims that after 25 years of research, any non-trivial problem studied is undecidable for general PTAs. Bounding time, the number of parameters, or the domain of parameters does not in general yield decidability, whereas restrictions on the number of clocks, the use of clocks versus parameters, and the use of parameters (e.g., only as upper or lower bounds) can restore decidability for some problems. The survey also emphasizes open problems, discusses related formalisms such as parametric hybrid automata and parametric interrupt timed automata, and reviews dedicated tools.

Significance. If the compilation of prior results is accurate, the survey is significant for researchers in real-time verification: it consolidates the known decidability landscape for PTAs, identifies the restrictions that separate decidable from undecidable cases, and flags open problems. The inclusion of tool discussions provides a practical bridge to implementation. Such a reference can help avoid redundant exploration of undecidable fragments and direct attention to decidable restrictions or open questions.

major comments (2)
  1. [Abstract] Abstract: The central framing that 'any non-trivial problem studied is undecidable for general PTAs' is load-bearing for the survey's narrative and for the subsequent classification of restrictions, yet the manuscript provides no explicit definition or criteria for what counts as 'non-trivial.' Without this, it is impossible to verify that the listed problems exhaust the relevant cases or that other modeling choices (e.g., specific guard forms or reset policies) do not produce additional decidable instances.
  2. [Abstract] Abstract: The claim that 'bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability' is presented as an established negative result, but the abstract (and thus the survey framing) does not cite the specific undecidability theorems or reductions that support each such statement; in a survey paper these pointers are necessary to substantiate the boundaries drawn.
minor comments (2)
  1. [Abstract] The abstract contains two consecutive sentences beginning 'We also,' which could be rephrased for smoother readability.
  2. A compact table or diagram summarizing which restrictions yield decidability for which problems would improve clarity and make the survey easier to use as a reference.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments and positive overall assessment of the survey. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central framing that 'any non-trivial problem studied is undecidable for general PTAs' is load-bearing for the survey's narrative and for the subsequent classification of restrictions, yet the manuscript provides no explicit definition or criteria for what counts as 'non-trivial.' Without this, it is impossible to verify that the listed problems exhaust the relevant cases or that other modeling choices (e.g., specific guard forms or reset policies) do not produce additional decidable instances.

    Authors: We agree that the informal use of 'non-trivial' in the abstract would benefit from clarification. The term is intended to denote the core decision and computation problems (reachability, emptiness, synthesis, etc.) that have been the focus of PTA research for 25 years, as opposed to trivial syntactic checks. The survey systematically covers all such problems from the literature. We will revise the abstract and/or introduction to include a short clarifying phrase or examples. revision: yes

  2. Referee: [Abstract] Abstract: The claim that 'bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability' is presented as an established negative result, but the abstract (and thus the survey framing) does not cite the specific undecidability theorems or reductions that support each such statement; in a survey paper these pointers are necessary to substantiate the boundaries drawn.

    Authors: The abstract is a high-level summary; the specific undecidability results and reductions for bounded time, bounded parameters, and bounded domains are stated and cited in the main body. Abstracts conventionally omit citations. We will add a brief pointer in the introduction to the relevant sections and key references to make the supporting results more immediately traceable. revision: partial

Circularity Check

0 steps flagged

No circularity: survey compiles external results without internal derivation

full rationale

This is a survey paper summarizing 25 years of external research on parametric timed automata. The central claim that non-trivial problems are undecidable for general PTAs is stated as a consensus from prior literature rather than derived via any equations, parameters, or self-referential definitions within the paper itself. No load-bearing step reduces by construction to the paper's own inputs, and references point outside the current work. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The survey relies on standard definitions and prior results in automata theory and timed systems; no new free parameters, axioms beyond standard mathematics, or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard definitions of parametric timed automata, clocks, parameters, and decidability from automata theory and prior PTA literature
    The survey builds directly on these established concepts without re-deriving them.

pith-pipeline@v0.9.0 · 5682 in / 1203 out tokens · 34012 ms · 2026-05-25T10:10:14.462853+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

38 extracted references · 38 canonical work pages

  1. [1]

    Model-Checking in Dense Real-Time

    [ACD93] Rajeev Alur, Costas Courcoubetis, and David L. Dill. “Model-Checking in Dense Real-Time”. In: Information and Compu- tation 104.1 (May 1993), pp. 2–34 . doi: 10.1006/inco.1993.1024 (cit. on p. 7). [Ace+03] Luca Aceto, Patricia Bouyer, Augusto Burgue˜ no, and Kim Guldstrand Larsen. “The power of reachability testing for timed automata”. In: Theoret...

    work page doi:10.1006/inco.1993.1024 1993

  2. [2]

    Liveness in L/U-Parametric Timed Automata

    Ed. by S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal. San Diego, California, United States: ACM, 1993, pp. 592–601. isbn: 0-89791-591-7 . doi: 10.1145/167088.167242 (cit. on pp. 2, 4–8, 10, 14, 15). [AL17a] ´Etienne Andr´ e and Didier Lime. “Liveness in L/U-Parametric Timed Automata”. In: Pro- ceedings of the 17th International Conference on Applic...

    work page doi:10.1145/167088.167242 1993

  3. [3]

    Learning- based compositional parameter synthesis for event-recording automata

    Ed. by Alex Legay and Klaus Schneider. Zaragoza, Spain: IEEE, 2017, pp. 9–18 . doi: 10.1109/ACSD.2017.19 (cit. on pp. 6, 7, 10–12). [AL17b] ´Etienne Andr´ e and Shang-Wei Lin. “Learning- based compositional parameter synthesis for event-recording automata”. In: Proceedings of the 37th IFIP WG 6.1 International Conference on Formal Techniques for Dis- trib...

    work page doi:10.1109/acsd.2017.19 2017

  4. [4]

    Integer-Complete Synthesis for Bounded Parametric Timed Automata

    Ed. by Ahmed Bouaj- jani and Silva Alexandra. Vol. 10321. Lec- ture Notes in Computer Science. Neuchˆ atel, Switzerland: Springer, 2017, pp. 17–32 . doi: 10.1007/978-3-319-60225-7_2 (cit. on p. 15). [ALM18] ´Etienne Andr´ e, Didier Lime, and Nicolas Markey. Language Preservation Problems in Parametric Timed Automata . 2018 . arXiv: 1807.07091 (cit. on p. ...

    work page doi:10.1007/978-3-319-60225-7_2 2017

  5. [5]

    Decision Problems for Parametric Timed Automata

    Lec- ture Notes in Computer Science. Warsaw, Poland: Springer, Sept. 2015, pp. 7–19 . doi: 10.1007/978-3-319-24537-9_2 (cit. on pp. 4, 15). [ALR16a] ´Etienne Andr´ e, Didier Lime, and Olivier H. Roux. “Decision Problems for Parametric Timed Automata”. In: Proceedings of the 18th International Conference on Formal Engineer- ing Methods (ICFEM

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

  6. [6]

    On the Expressiveness of Parametric Timed Automata

    Ed. by Kazuhiro Ogata, Mark Lawford, and Shaoying Liu. Vol. 10009. Lecture Notes in Computer Sci- ence. Tokyo, Japan: Springer, 2016, pp. 400– 416 . doi: 10.1007/978-3-319-47846-3_25 (cit. on pp. 4, 6, 7, 13, 14). [ALR16b] ´Etienne Andr´ e, Didier Lime, and Olivier H. Roux. “On the Expressiveness of Parametric Timed Automata”. In: Proceedings of the 14th ...

    work page doi:10.1007/978-3-319-47846-3_25 2016

  7. [7]

    Parametric temporal logic for “model measuring

    Lecture Notes in Computer Science. Qu´ ebec, Canada: Springer, 2016, 15 pp. 19–34 . doi: 10.1007/978-3-319-44878-7_2 (cit. on p. 4). [Alu+01] Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron Peled. “Parametric temporal logic for “model measuring””. In: ACM Trans- actions on Computational Logic 2.3 (2001), pp. 388–407 . doi: 10.1145/377978.37799...

    work page doi:10.1007/978-3-319-44878-7_2 2016

  8. [8]

    Decision Problems for Timed Automata: A Survey

    Lecture Notes in Computer Science. Lyngby, Denmark: Springer, 1993, pp. 209–229 . doi: 10.1007/3-540-57318-6_30 (cit. on p. 12). [AM04] Rajeev Alur and P. Madhusudan. “Decision Problems for Timed Automata: A Survey”. In: Formal Methods for the Design of Real- Time Systems, International School on For- mal Methods for the Design of Computer, Communication ...

    work page doi:10.1007/3-540-57318-6_30 1993

  9. [9]

    Lan- guage Preservation Problems in Paramet- ric Timed Automata

    Lecture Notes in Computer Science. Berti- noro, Italy: Springer, 2004, pp. 1–24 . doi: 10.1007/978-3-540-30080-9_1 (cit. on pp. 1, 2). [AM15] ´Etienne Andr´ e and Nicolas Markey. “Lan- guage Preservation Problems in Paramet- ric Timed Automata”. In: Proceedings of the 13th International Conference on For- mal Modeling and Analysis of Timed Systems (FORMATS

    work page doi:10.1007/978-3-540-30080-9_1 2004

  10. [10]

    An Inverse Method for Parametric Timed Automata

    Lecture Notes in Computer Science. Madrid, Spain: Springer, Sept. 2015, pp. 27–43 . doi: 10.1007/978-3-319-22975-1_3 (cit. on pp. 4–9, 11, 12, 14). [And+09] ´Etienne Andr´ e, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. “An Inverse Method for Parametric Timed Automata”. In: International Journal of Foundations of Com- puter Science 20.5 (Oct...

    work page doi:10.1007/978-3-319-22975-1_3 2015

  11. [11]

    Parameter Synthesis for Hier- archical Concurrent Real-Time Systems

    Lecture Notes in Computer Science. Paris, France: Springer, Aug. 2012, pp. 33–36 . doi: 10.1007/978-3-642-32759-9_6 (cit. on p. 14). [And+12b] ´Etienne Andr´ e, Yang Liu, Jun Sun, and Jin Song Dong. “Parameter Synthesis for Hier- archical Concurrent Real-Time Systems”. In: Proceedings of the 17th IEEE International Conference on Engineering of Complex Com...

    work page doi:10.1007/978-3-642-32759-9_6 2012

  12. [12]

    PSyH- CoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems

    Ed. by Isabelle Perseil, Marc Pouzet, and Karin Breitman. Paris, France: IEEE Computer Society, July 2012, pp. 253–262 . doi: 10.1109/ICECCS.2012.29 (cit. on p. 13). [And+13] ´Etienne Andr´ e, Yang Liu, Jun Sun, Jin Song Dong, and Shang-Wei Lin. “PSyH- CoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems”. In: Pro- ceedings of the 25th I...

    work page doi:10.1109/iceccs.2012.29 2012

  13. [13]

    Parametric model checking timed automata under non-Zenoness assumption

    Lecture Notes in Computer Science. Saint Petersburg, Rus- sia: Springer, July 2013, pp. 984–989 . doi: 10.1007/978-3-642-39799-8_70 (cit. on p. 13). [And+17] ´Etienne Andr´ e, Hoang Gia Nguyen, Laure Petrucci, and Jun Sun. “Parametric model checking timed automata under non-Zenoness assumption”. In: Proceedings of the 9th NASA Formal Methods Symposium (NFM

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

  14. [14]

    Parametric Deadlock- Freeness Checking Timed Automata

    Ed. by Clark Barrett and Temesghen Kahsai. Vol. 10227. Lecture Notes in Computer Sci- ence. Moffett Field, CA, USA: Springer, 2017, pp. 35–51 . doi: 10.1007/978-3-319-57288-8_3 (cit. on p. 14). [And16a] ´Etienne Andr´ e. “Parametric Deadlock- Freeness Checking Timed Automata”. In: Proceedings of the 13th International Collo- quium on Theoretical Aspects of...

    work page doi:10.1007/978-3-319-57288-8_3 2017

  15. [15]

    What’s decidable about para- metric timed automata?

    Lec- ture Notes in Computer Science. Taipei, Taiwan: Springer, 2016, pp. 469–478 . doi: 10.1007/978-3-319-46750-4_27 (cit. on p. 14). [And16b] ´Etienne Andr´ e. “What’s decidable about para- metric timed automata?” In: Proceedings of the 4th International Workshop on For- mal Techniques for Safety-Critical Systems (FTSCS

    work page doi:10.1007/978-3-319-46750-4_27 2016

  16. [16]

    Low di- mensional hybrid systems – Decidable, un- decidable, don’t know

    Communications in Computer and Information Science. Paris, France: Springer, Jan. 2016, pp. 52–68 . doi: 10.1007/978-3-319-29510-7_3 (cit. on p. 2). [Asa+12] Eugene Asarin, Venkatesh Mysore, Amir Pnueli, and Gerardo Schneider. “Low di- mensional hybrid systems – Decidable, un- decidable, don’t know”. In: Information and Computation 211 (2012), pp. 138–159...

    work page doi:10.1007/978-3-319-29510-7_3 2016

  17. [17]

    Language Emptiness of Continuous-Time Parametric Timed Au- 16 tomata

    Lecture Notes in Computer Science. 2016, pp. 60–68 . doi: 10.1007/978-3-319-48989-6_4 (cit. on p. 15). [Ben+15] Nikola Beneˇ s, Peter Bezdˇ ek, Kim Gulstrand Larsen, and Jiˇ r ´ ı Srba. “Language Emptiness of Continuous-Time Parametric Timed Au- 16 tomata”. In: Proceedings of the 42nd Inter- national Colloquium on Automata, Languages, and Programming (ICA...

    work page doi:10.1007/978-3-319-48989-6_4 2016

  18. [18]

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

    Lecture Notes in Computer Science. Kyoto, Japan: Springer, July 2015, pp. 69–81 . doi: 10.1007/978-3-662-47666-6_6 (cit. on pp. 4, 7–9). [B´ er+05] B´ eatrice B´ erard, Franck Cassez, Serge Had- dad, Didier Lime, and Olivier H. Roux. “Com- parison of the Expressiveness of Timed Au- tomata and Time Petri Nets”. In: Proceed- ings of the Third International ...

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

  19. [19]

    The expressive power of time Petri nets

    Lecture Notes in Computer Science. Uppsala, Sweden: Springer, 2005, pp. 211–225 . doi: 10.1007/11603009_17 (cit. on pp. 13, 14). [B´ er+13] B´ eatrice B´ erard, Franck Cassez, Serge Had- dad, Didier Lime, and Olivier H. Roux. “The expressive power of time Petri nets”. In: Theo- retical Computer Science 474 (2013), pp. 1–20 . doi: 10.1016/j.tcs.2012.12.005...

    work page doi:10.1007/11603009_17 2005

  20. [20]

    Interrupt Timed Automata with Auxiliary Clocks and Parame- ters

    Lecture Notes in Computer Science. War- saw, Poland: Springer, 2015, pp. 20–32 . doi: 10.1007/978-3-319-24537-9_3 (cit. on pp. 13, 15). [B´ er+16] B´ eatrice B´ erard, Serge Haddad, Aleksandra Jovanovic, and Didier Lime. “Interrupt Timed Automata with Auxiliary Clocks and Parame- ters”. In: Fundamenta Informormatica 143.3-4 (2016), pp. 235–259 . doi: 10.3...

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

  21. [21]

    Ad- vances in Parametric Real-Time Reasoning

    Lecture Notes in Com- puter Science. Invited paper. Uppsala, Swe- den: Springer, Sept. 2013, pp. 1–18 . doi: 10.1007/978-3-642-41036-9_1 (cit. on pp. 1, 2, 14). [BO14] Daniel Bundala and Jo¨ el Ouaknine. “Ad- vances in Parametric Real-Time Reasoning”. In: Proceedings of the 39th International Sym- posium on Mathematical Foundations of Com- puter Science (...

    work page doi:10.1007/978-3-642-41036-9_1 2013

  22. [22]

    Real-Time Model-Checking: Parameters ev- erywhere

    Lecture Notes in Computer Science. Budapest, Hungary: Springer, 2014, pp. 123–134. isbn: 978-3-662- 44521-1 . doi: 10.1007/978-3-662-44522-8 (cit. on pp. 8, 14). [BR07] V´ eronique Bruy` ere and Jean-Francois Raskin. “Real-Time Model-Checking: Parameters ev- erywhere”. In: Logical Methods in Com- puter Science 3.1:7 (2007), pp. 1–30 . doi: 10.2168/LMCS-3(...

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

  23. [23]

    Time-Bounded Reacha- bility for Monotonic Hybrid Automata: Com- plexity and Fixed Points

    Lecture Notes in Com- puter Science. Springer, 2004, pp. 219–233 . doi: 10.1007/978-3-540-24743-2_15 (cit. on pp. 12, 15). [Bri+13] Thomas Brihaye, Laurent Doyen, Gilles Geer- aerts, Jo¨ el Ouaknine, Jean-Francois Raskin, and James Worrell. “Time-Bounded Reacha- bility for Monotonic Hybrid Automata: Com- plexity and Fixed Points”. In: Proceedings of the 1...

    work page doi:10.1007/978-3-540-24743-2_15 2004

  24. [24]

    Timed Verification of the Generic Architec- ture of a Memory Circuit Using Parametric Timed Automata

    Lec- ture Notes in Computer Science. Hanoi, Vietnam: Springer, 2013, pp. 55–70 . doi: 10.1007/978-3-319-02444-8_6 (cit. on pp. 7, 12). [Che+09] R´ emy Chevallier, Emmanuelle Encrenaz- Tiph` ene, Laurent Fribourg, and Weiwen Xu. “Timed Verification of the Generic Architec- ture of a Memory Circuit Using Parametric Timed Automata”. In: Formal Methods in Syst...

    work page doi:10.1007/978-3-319-02444-8_6 2013

  25. [25]

    Struc- tural translation from Time Petri Nets to Timed Automata

    Lecture Notes in Computer Sci- 17 ence. Springer, 2000, pp. 138–152 . doi: 10.1007/3-540-44618-4_12 (cit. on p. 12). [CR06] Franck Cassez and Olivier H. Roux. “Struc- tural translation from Time Petri Nets to Timed Automata”. In: Journal of Systems and Software 79.10 (2006), pp. 1456–1468 . doi: 10.1016/j.jss.2005.12.021 (cit. on p. 13). [DLN15] Barbara D...

    work page doi:10.1007/3-540-44618-4_12 2000

  26. [26]

    Robustness Analysis for Scheduling Problems using the Inverse Method

    Perth, Australia: Michigan Publishing, Aug. 2013 (cit. on p. 14). [Fri+12] Laurent Fribourg, David Lesens, Pierre Moro, and Romain Soulat. “Robustness Analysis for Scheduling Problems using the Inverse Method”. In: Proceedings of the 19th Inter- national Symposium on Temporal Represen- tation and Reasoning (TIME

    work page 2013

  27. [27]

    The Linear Time- Branching Time Spectrum (Extended Ab- stract)

    Ed. by Mark Reynolds, Paolo Terenziani, and Ben Moszkowski. Leicester, UK: IEEE Computer Society Press, Sept. 2012, pp. 73–80 . doi: 10.1109/TIME.2012.10 (cit. on p. 14). [Gla90] Rob J. van Glabbeek. “The Linear Time- Branching Time Spectrum (Extended Ab- stract)”. In: Proceedings of CONCUR 1990, Theories of Concurrency: Unification and Ex- tension. Ed. by...

    work page doi:10.1109/time.2012.10 2012

  28. [28]

    Symbolic Model Checking for Real-Time Systems

    Lecture Notes in Computer Science. Amsterdam, The Nether- lands: Springer, 1990, pp. 278–297 . doi: 10.1007/BFb0039066 (cit. on p. 4). [Hen+94] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. “Symbolic Model Checking for Real-Time Systems”. In: In- formation and Computation 111.2 (1994), pp. 193–244 . doi: 10.1006/inco.1994.1045 (...

    work page doi:10.1007/bfb0039066 1990

  29. [29]

    HyTech: A Model Checker for Hybrid Systems

    Ed. by Moshe Y. Vardi and Edmund M. Clarke. New Brunswick, New Jersey, USA: IEEE Computer Society, 1996, pp. 278–292 . doi: 10.1109/LICS.1996.561342 (cit. on p. 12). [HHW97] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. “HyTech: A Model Checker for Hybrid Systems”. In: Inter- national Journal on Software Tools for Technology Transfer 1.1-2 (1997)...

    work page doi:10.1109/lics.1996.561342 1996

  30. [30]

    Communicating sequential processes

    Lecture Notes in Computer Science. Szeged, Hungary: Springer, 1995, pp. 417–428 . doi: 10.1007/3-540-60084-1_93 (cit. on p. 4). [Hoa78] C.A.R. Hoare. “Communicating sequential processes”. In: Communications of the ACM 21 (8 1978), pp. 666–677. issn: 0001-0782. doi: 10.1145/359576.359585 (cit. on p. 13). [Hun+02] Thomas Hune, Judi Romijn, Mari¨ elle Stoeli...

    work page doi:10.1007/3-540-60084-1_93 1995

  31. [31]

    UPPAAL in a Nutshell

    Lecture Notes in Computer Science. York, United Kingdom: Springer, Mar. 2009, pp. 54– 57 . doi: 10.1007/978-3-642-00768-2_6 (cit. on p. 14). [LPY97] Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. “UPPAAL in a Nutshell”. In: Inter- 18 national Journal on Software Tools for Tech- nology Transfer 1.1-2 (1997), pp. 134–152 . doi: 10.1007/s100090050010 (...

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

  32. [32]

    A study of the recov- erability of computing systems

    Ed. by Iain Bate and Roberto Passerone. V¨ aster ˚ as, Sweden: IEEE Computer Society Press, June 2011, pp. 28–34 . doi: 10.1109/SIES.2011.5953652 (cit. on pp. 1, 2, 14). [Mer74] Philip Meir Merlin. “A study of the recov- erability of computing systems.” PhD the- sis. University of California, Irvine, CA, USA, 1974 (cit. on p. 13). [Mil00] Joseph S. Miller...

    work page doi:10.1109/sies.2011.5953652 2011

  33. [33]

    Pittsburgh, PA, USA: Springer, 2000, pp

    Lecture Notes in Com- puter Science. Pittsburgh, PA, USA: Springer, 2000, pp. 296–309. isbn: 3-540-67259-1 . doi: 10.1007/3-540-46430-1_26 (cit. on pp. 3, 4, 6– 8). [Min67] Marvin L. Minsky. Computation: Finite and infinite machines . Upper Saddle River, NJ, USA: Prentice-Hall, Inc.,

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

  34. [34]

    On the decidability and complexity of Metric Tem- poral Logic over finite words

    isbn: 0-13- 165563-9 (cit. on p. 5). [OW07] Jo¨ el Ouaknine and James Worrell. “On the decidability and complexity of Metric Tem- poral Logic over finite words”. In: Logical Methods in Computer Science 3.1 (2007) . doi: 10.2168/LMCS-3(1:8)2007 (cit. on p. 9). [OW10] Jo¨ el Ouaknine and James Worrell. “Towards a Theory of Time-Bounded Verification”. In: Proc...

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

  35. [35]

    MTL-Model Checking of One- Clock Parametric Timed Automata is Un- decidable

    Lecture Notes in Com- puter Science. July 6-10, 2010: Springer, 2010, pp. 22–37 . doi: 10.1007/978-3-642-14162-1_3 (cit. on p. 6). [Qua14] Karin Quaas. “MTL-Model Checking of One- Clock Parametric Timed Automata is Un- decidable”. In: Proceedings of the 1st In- ternational Workshop on Synthesis of Con- tinuous Parameters (SynCoP

    work page doi:10.1007/978-3-642-14162-1_3 2010

  36. [36]

    Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets

    EPTCS. Grenoble, France, 2014, pp. 5–17 . doi: 10.4204/EPTCS.145.3 (cit. on p. 9). [Srb08] Jiˇ r ´ ı Srba. “Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets”. In: Proceedings of the 6th In- ternational Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2008). Ed. by Franck Cassez and Claude Jard. Vol

    work page doi:10.4204/eptcs.145.3 2014

  37. [37]

    PAT: Towards Flexible Verification un- der Fairness

    Lecture Notes in Computer Science. Saint-Malo, France: Springer, 2008, pp. 15– 32 . doi: 10.1007/978-3-540-85778-5_3 (cit. on p. 13). [Sun+09] Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. “PAT: Towards Flexible Verification un- der Fairness”. In: Proceedings of the 21st Inter- national Conference on Computer Aided Veri- fication (CA V 2009). Ed. by Ahmed...

    work page doi:10.1007/978-3-540-85778-5_3 2008

  38. [38]

    Modeling and Verifying Hierarchical Real-time Systems us- ing Stateful Timed CSP

    Lecture Notes in Computer Science. Grenoble, France: Springer, 2009, pp. 709–714. isbn: 978-3-642-02657- 7 . doi: 10.1007/978-3-642-02658-4_59 (cit. on p. 1). [Sun+13] Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, and ´Etienne Andr´ e. “Modeling and Verifying Hierarchical Real-time Systems us- ing Stateful Timed CSP”. In: ACM Trans- actions on Soft...

    work page doi:10.1007/978-3-642-02658-4_59 2009