Parameter Synthesis for Timed Kripke Structures

• Autorzy: Knapik M. , Penczek W.

Identyfikatory

DOI

10.3233/FI-2014-1072

• Języki publikacji: EN

Abstrakty

EN

We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL, called RTCTLP, holds in a parametric timed Kripke structure. We prove the decidability of parameter synthesis for RTCTLP by showing how to restrict the infinite space of parameter valuations to its finite subset and employ a brute-force algorithm. The bruteforce approach soon becomes intractable, therefore we propose a symbolic algorithm for RTCTLP parameter synthesis. Similarly to the fixed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a translation from the RTCTLP parameter synthesis problem to a discrete optimization task. We show that the proposedmethod is sound and complete and provide some complexity results. We argue that this approach leads to new opportunities in model checking, including the use of integer programming and related tools.

Słowa kluczowe

EN

Kripke semantics; integer programming; parameter estimation; computer algorithms; combinatorial optimization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 133, nr 2/3
• Strony: 211--226
• Opis fizyczny: Bibliogr. 12 poz., rys.

Twórcy

autor

Knapik M.

• Institute of Computer Science, PAS, Warsaw, Poland

autor

Penczek W.

• Institute of Computer Science, PAS, Warsaw, Poland

Bibliografia

• [1] É. André, T. Chatain, E. Encrenaz, and L. Fribourg, An inverse method for parametric timed automata, International Journal of Foundations of Computer Science 20 (2009), no. 5, 819–836.
• [2] É. André, L. Fribourg, U. Kühne, and R. Soulat, Imitator 2.5: A tool for analyzing robustness in scheduling problems, Proc. of the Formal Methods - 18th International Symposium, LNCS, vol. 7436, Springer-Verlag, 2012, pp. 33–36.
• [3] R. Alur, T. Henzinger, and M. Vardi, Parametric real-time reasoning, Proc. of the 25th Ann. Symp. On Theory of Computing (STOC’93), ACM, 1993, pp. 592–601.
• [4] L. Doyen, Robust parametric reachability for timed automata, Inf. Process. Lett. 102 (2007), 208–213.
• [5] E. A. Emerson and R. Trefler, Parametric quantitative temporal reasoning, Proc. of the 14th Symp. on Logic in Computer Science (LICS’99), IEEE Computer Society, July 1999, pp. 336–343.
• [6] T. Henzinger, P. Ho, and H. Wong-Toi, HyTech: A model checker for hybrid systems, Proc. of the 9th Int. Conf. on Computer Aided Verification (CAV’97), LNCS, vol. 1254, Springer-Verlag, 1997, pp. 460–463.
• [7] T. Hune, J. Romijn, M. Stoelinga, and F. Vaandrager, Linear parametric model checking of timed automata, Proc. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), LNCS, vol. 2031, Springer-Verlag, 2001, pp. 189–203.
• [8] A. V. Jones, M. Knapik, A. Lomuscio, andW. Penczek, Group synthesis for parametric temporal-epistemic logic, Proc. of the 11th Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS’12), IFAAMAS, 2012, pp. 1107–1114.
• [9] A. V. Jones, A. Lomuscio,M. Knapik, andW. Penczek, Group synthesis for alternating-time temporal logic, Tech. report, Department of Computing, Imperial College, London, 2013.
• [10] A. Jovanović, D. Lime, and O. H. Roux, Integer parameter synthesis for timed automata, Proc. of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems (Berlin, Heidelberg), TACAS’13, Springer-Verlag, 2013, pp. 401–415.
• [11] M. Knapik and W. Penczek, Bounded model checking for parametric timed automata, T. Petri Nets and Other Models of Concurrency 5 (2012), 141–159.
• [12] L-M. Tranouez, D. Lime, and O. H. Roux, Parametric model checking of time Petri nets with stopwatches using the state-class graph, Proc. of the 6th Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS’08), LNCS, vol. 5215, Springer-Verlag, 2008, pp. 280–294.