ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 09:00 - 09:45 at S10 - Parameter synthesis for LTL

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.

Sun 7 Apr (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30: SynCoP - Parameter synthesis for LTL at S10
syncop-2019-papers09:00 - 09:45
syncop-2019-papers09:45 - 10:30
Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University