Affiliations: Institute of Computer Science, PAS, Warsaw, Poland. mknapik@ipipan.waw.pl; penczek@ipipan.waw.pl
Note: [] Address for correspondence: Institute of Computer Science, PAS, Warsaw, Poland
Note: [] Also works: University of Natural Sciences and Humanities, II, Siedlce, Poland
Abstract: 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 brute-force 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 proposed method 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.
