Decidability of performance equivalence for basic parallel processes

被引：6

作者：

Lasota, Slawomir ^{[1
]}

机构：

[1] Warsaw Univ, Inst Informat, PL-02097 Warsaw, Poland

来源：

THEORETICAL COMPUTER SCIENCE | 2006年 / 360卷 / 1-3期

关键词：

process algebra; basic parallel processes; bisimulation equivalence; performance equivalence; equivalence checking;

D O I：

10.1016/j.tcs.2006.02.020

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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 Berard et al. Both ill-timed and well-timed semantics are treated. (C) 2006 Elsevier B.V. All rights reserved.

引用

页码：172 / 192

页数：21

共 29 条

[1] Aceto L., 1992, Fundamenta Informaticae, V17, P319
[2] Timing and causality in process algebra
Aceto, L
Murphy, D
[J]. ACTA INFORMATICA, 1996, 33 (04) : 317 - 350
[3] Baeten J.C.M., 2001, HDB PROCESS ALGEBRA, P627
[4] Bednarczyk Marek A., 1991, HEREDITARY HIST PRES
[5] Bérard B, 2000, LECT NOTES COMPUT SC, V1784, P35
[6] Burkart O., 2001, Handbook of Process Algebra, P545
[7] CASTELLANI I, 1988, THESIS U EDINBURG
[8] Castellani Ilaria, 2001, Handbook of Process Algebra, P945, DOI [10.1016/b978-044482830-9/50033-3, DOI 10.1016/B978-044482830-9/50033-3]
[9] CANONIC GRAPHS OF ALGEBRAIC GRAPHS
CAUCAL, D
[J]. RAIRO-INFORMATIQUE THEORIQUE ET APPLICATIONS-THEORETICAL INFORMATICS AND APPLICATIONS, 1990, 24 (04): : 339 - 352
[10] CERANS K, 1992, LECT NOTES COMPUTER, V663

← 1 2 3 →