Control synthesis for parametric timed automata under reachability

Timed automata is a fundamental modeling formalism for real-time systems. During the design of such real-time systems, often the system information is incomplete, and design choices can vary. These uncertainties can be integrated to the model via parameters and labelled transitions. Then, the design can be completed by tuning the parameters and restricting the transitions via controller synthesis. These problems, namely parameter synthesis and controller synthesis, are studied separately in the literature. Herein, these are combined to generate an automaton satisfying the given specification by both parameter tuning and controller synthesis, thus exploring all design choices. First, it is shown that the negative decidability results derived for the parameter synthesis problem apply to the proposed problem. Then, a specific version of the problem is studied, where the specification is to reach a target set and parameters can take values from bounded integer sets. An algorithm based on depth first analysis combined with an iterative feasibility check is presented to solve the proposed problem. The correctness and the completeness (under mild assumptions) of the developed algorithm are proven. The findings of the paper are illustrated on an example drawn from scheduling.

PDF

___

[1] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science 1994; 126 (2): 183–235.
[2] Fehnker A. Scheduling a steel plant with timed automata. In: Proceedings Sixth International Conference on Real-Time Computing Systems and Applications; Hong Kong, China; 1999. pp. 280-286.
[3] David A, Illum J, Larsen K G, Skou A. Model-based framework for schedulability analysis using UPPAAL 4.1. In: Model-based design for embedded systems. CRC Press, 2009, pp. 117-144.
[4] Guan N, Gu Z, Deng Q, Gao S, Yu G. Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking. In: Software Technologies for Embedded and Ubiquitous Systems; Santorini Island, Greece; 2007. pp. 263-272.
[5] Kwiatkowska M, Mereacre A, Paoletti N, Patanè A. Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques. In: Abate, A., Šafránek, D. (editors). Hybrid Systems Biology. Lecture Notes in Computer Science, vol 9271. Cham, Switzerland: Springer, 2015, pp. 119-140.
[6] Jiang Z, Pajic M, Alur R, Mangharam R. Closed-loop verification of medical devices with model abstraction and refinement. International Journal on Software Tools for Technology Transfer 2014; 16 (2): 191-213. doi.org/10.1007/s10009-013-0289-7
[7] Wang F. Formal verification of timed systems: a survey and perspective. Proceedings of the IEEE 2004; 92 (8): 1283–1305. 0.1109/JPROC.2004.831197
[8] Behrmann G, David A, Larsen K G, Hakansson J, Petterson P et al. Uppaal 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems; Washington, DC, USA; 2006. pp. 125-126.
[9] André É, Fribourg L, Kühne U, Soulat R. Imitator 2.5: A tool for analyzing robustness in scheduling problems. In: Formal Methods; Paris, France; 2012. pp. 33-36.
[10] Henzinger T A, Preussig J, Wong-Toi H. Some lessons from the hytech experience. In: Proceedings of the 40th IEEE Conference on Decision and Control; Orlando, FL, USA; 2001. pp. 2887–2892.
[11] André É, Fribourg L, Mota J-M, Soulats R. Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In: Verification, Model Checking, and Abstract Interpretation; Cascais, Portugal; 2019. pp. 409-424.
[12] André E. What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer 2019; 21 (2): 203–219.
[13] Bezděk P, Beneš N, Barnat J, Černá I. Ltl parameter synthesis of parametric timed automata. In: Software Engineering and Formal Methods; Vienna, Austria; 2016. pp. 172-187.
[14] Jovanovic A, Lime D, Roux, O H. Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engineering 2015; 41 (5): 445-461.
[15] André É. A benchmark library for parametric timed model checking. In: Formal Techniques for Safety-Critical Systems; Shenzhen, China; 2019. pp. 75-83.
[16] Asarin E, Maler O, Pnueli A, Sifakis J. Controller synthesis for timed automata. In: 5th IFAC Conference on System Structure and Control; Nantes, France; 1998. pp. 447-452.
[17] Bouyer P, Fahrenberg U, Larsen KG, Markey N, Ouaknine J et al. Model Checking Real-Time Systems, pp. 1001– 1046. Cham, Switzerland: Springer International Publishing, 2018.
[18] Alur R, La Torre S, Pappas G J. Optimal paths in weighted timed automata. Theoretical Computer Science 2004; 318 (3): 297-322.
[19] Étienne A, Knapik M, Penczek W, Petrucci L. Controlling actions and time in parametric timed automata. In: 16th International Conference on Application of Concurrency to System Design; Torun, Poland ; 2016. pp. 45-54.
[20] Kara M Y, Gol E A. Adaptive cruise control with timed automata. In: 21th IFAC World Congress; Berlin, Germany (online), 2020. pp. 1-6.
[21] Alur R. Timed automata. In: International Conference on Computer Aided Verification; Trento Italy; 1999. pp.8-22.
[22] Larsen K G, Yi W. Time abstracted bisimulation: Implicit specifications and decidability. In: International Conference on Mathematical Foundations of Programming Semantics; New Orleans, LA, USA; 1993. pp. 160-176.
[23] Baier C, Katoen J-P, Larsen K G. Principles of Model Checking. Cambridge, MA, USA: The MIT Press, 2008.
[24] Bouyer P, Brihaye T, Bruyère V, Raskin J-F. On the optimal reachability problem of weighted timed automata. Formal Methods in System Design 2007; 31 (2): 135-175.
[25] Ober I. Revisiting bounded reachability analysis of timed automata based on milp. In: Formal Methods for Industrial Critical Systems; Maynooth, Ireland; 2018. pp. 269-283.