Seminaria ogólnoinstytutowe:

Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose two new exploration orders, i.e. the “ranking strategy" and the "priority based strategy", and compare them with existing strategies. We consider both complete parameter synthesis, and counterexample synthesis where the analysis stops as soon as some parameter valuations are found. Besides, the ranking will be adapted in order to first synthesize only our desired parameters. Here, we discuss exploring strategy making parameter synthesizing more efficient. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches, especially in the counterexample synthesis.