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

We consider parametric timed automata (PTA), in which parameters are used for lower and upper bounds of clock values. In particular, we improve algorithms to synthesise the parameter constraints for which a given LTL property would hold.

Since the problem is undecidable, we rely on semi-algorithms that explore a possibly infinite state space of symbolic zones, represented by polyhedra. The basic algorithm applies a cumulative version of Nested Depth First Search. Its successful termination depends crucially on heuristics for pruning the state space.

In cumulative NDFS, the current set of parameter constraints that violate the property is maintained, and can be used to limit the search to new parameter valuations. Another method is to discard states that are subsumed by states that have already been explored before. However, in order to preserve LTL properties we can only apply subsumption with special care.

We analyse cumulative NDFS, introduce some optimisations, and propose a more aggressive subsumption method. We illustrate the improved termination capability of the improved algorithm by synthesising new parameter constraints for the well known Bounded Retransmission Protocol.

Sun 7 Apr

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

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