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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Parameter synthesis for LTLSynCoP at S10
09:00
45m
Talk
Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties
SynCoP
09:45
45m
Talk
Pruning NDFS for Parametric Timed Automata
SynCoP
Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University