Decidability of Strong Bisimilarity for Timed BPP
We investigate a timed extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends earlier decidability result for plain BPP as well as decidability for timed BPP with strictly positive durations of actions. Both ill-timed and well-timed semantics are treated. Our decision procedure is based on decidability of validity problem for Presburger arithmetic.