Decidability of performance equivalence for basic parallel processes |
| |
Authors: | Sawomir Lasota |
| |
Affiliation: | aInstitute of Informatics, Warsaw University, 02-097 Warszawa, ul. Banacha 2, Poland |
| |
Abstract: | We study an 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 the earlier decidability result for plain BPP by Christensen et al. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic. We prove also polynomial complexity in positive-duration fragment, thus properly extending a previous result by Bérard et al. Both ill-timed and well-timed semantics are treated. |
| |
Keywords: | Process algebra Basic parallel processes Bisimulation equivalence Performance equivalence Equivalence checking |
本文献已被 ScienceDirect 等数据库收录! |
|