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.