Control synthesis for parametric timed automata under reachability
Yıl: 2021 Cilt: 29 Sayı: 3 Sayfa Aralığı: 1751 - 1764 Metin Dili: İngilizce DOI: 10.3906/elk-2007-170 İndeks Tarihi: 23-06-2022
Control synthesis for parametric timed automata under reachability
Öz: 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.
Anahtar Kelime: Belge Türü: Makale Makale Türü: Araştırma Makalesi Erişim Türü: Erişime Açık
- [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.
APA | AYDIN GOL E (2021). Control synthesis for parametric timed automata under reachability . , 1751 - 1764. 10.3906/elk-2007-170 |
Chicago | AYDIN GOL EBRU Control synthesis for parametric timed automata under reachability . (2021): 1751 - 1764. 10.3906/elk-2007-170 |
MLA | AYDIN GOL EBRU Control synthesis for parametric timed automata under reachability . , 2021, ss.1751 - 1764. 10.3906/elk-2007-170 |
AMA | AYDIN GOL E Control synthesis for parametric timed automata under reachability . . 2021; 1751 - 1764. 10.3906/elk-2007-170 |
Vancouver | AYDIN GOL E Control synthesis for parametric timed automata under reachability . . 2021; 1751 - 1764. 10.3906/elk-2007-170 |
IEEE | AYDIN GOL E "Control synthesis for parametric timed automata under reachability ." , ss.1751 - 1764, 2021. 10.3906/elk-2007-170 |
ISNAD | AYDIN GOL, EBRU. "Control synthesis for parametric timed automata under reachability ". (2021), 1751-1764. https://doi.org/10.3906/elk-2007-170 |
APA | AYDIN GOL E (2021). Control synthesis for parametric timed automata under reachability . Turkish Journal of Electrical Engineering and Computer Sciences, 29(3), 1751 - 1764. 10.3906/elk-2007-170 |
Chicago | AYDIN GOL EBRU Control synthesis for parametric timed automata under reachability . Turkish Journal of Electrical Engineering and Computer Sciences 29, no.3 (2021): 1751 - 1764. 10.3906/elk-2007-170 |
MLA | AYDIN GOL EBRU Control synthesis for parametric timed automata under reachability . Turkish Journal of Electrical Engineering and Computer Sciences, vol.29, no.3, 2021, ss.1751 - 1764. 10.3906/elk-2007-170 |
AMA | AYDIN GOL E Control synthesis for parametric timed automata under reachability . Turkish Journal of Electrical Engineering and Computer Sciences. 2021; 29(3): 1751 - 1764. 10.3906/elk-2007-170 |
Vancouver | AYDIN GOL E Control synthesis for parametric timed automata under reachability . Turkish Journal of Electrical Engineering and Computer Sciences. 2021; 29(3): 1751 - 1764. 10.3906/elk-2007-170 |
IEEE | AYDIN GOL E "Control synthesis for parametric timed automata under reachability ." Turkish Journal of Electrical Engineering and Computer Sciences, 29, ss.1751 - 1764, 2021. 10.3906/elk-2007-170 |
ISNAD | AYDIN GOL, EBRU. "Control synthesis for parametric timed automata under reachability ". Turkish Journal of Electrical Engineering and Computer Sciences 29/3 (2021), 1751-1764. https://doi.org/10.3906/elk-2007-170 |