Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties
The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. We introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. Clock-Aware LTL is an extension of LTL that allows to reason about the clock values in the atomic propositions. We propose a symbolic zone-based method for the problem which can be significantly faster than the naive parameter scan solution. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata.