Preserving Partial Order Runs in Parametric Time Petri Nets.

Parameter synthesis for timed systems aims at deriving parameter valuationssatisfying a given property. In this paper we target concurrent systems; it iswell known that concurrency is a source of state-space explosion, and partialorder techniques were defined to cope with this problem. Here we use partialorder semantics for parametric time Petri nets as a way to significantly enhancethe result of an existing synthesis algorithm. Given a reference parametervaluation, our approach synthesizes other valuations preserving, up tointerleaving, the behavior of the reference parameter valuation. We show theapplicability of our approach using acyclic asynchronous circuits.