We address the problem of deciding performance equivalence for a timed process algebra in which actions are urgent and durational, and where parallel components have independent local clocks. This process algebra can be seen as a timed extension of BPP, a process algebra giving rise to infinite-state processes. While bisimulaiton was known to be decidable for BPP with a non elementary complexity, our main and surprising result is that, for the timed extension, performance equivalence is decidable in polynomial time.
展开▼
