Decidability of Strong Bisimilarity for Timed BPP Slawomir Lasota
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.
|
concur02@fi.muni.cz |