Name
Abstract | ||
|---|---|---|
We have shown that bisimulation equivalence is decidable for BPA. As the proof involves two semi-decision procedures it is
not obvious how to determine the complexity of solving this problem. Moreover it does not provide us with an intuitive technique
for deciding bisimilarity as does the tableau method in [14, 13] which also has the advantage of providing us with a way of
extracting a complete axiomatization for normed BPA processes. A similar result for full BPA would be a proper extension of
Milner's axiom system for regular processes [16].
More generally this work addresses the area of infinite-state processes. Besides deciding equivalences there is also the question
of model checking: a recent result
Of more interest to concurrency theory are process languages with parallel combinators. Although bisimulation equivalence
is undecidable for ACP, CCS, and CSP it is unclear if this must be true of all parallel models with full Turing power (especially
those that lack abstraction mechanisms). Moreover there may be finer useful equivalences which permit general decidability
results: for instance in [8] it is shown that distributed bisimulation equivalence is decidable for a recursive fragment of
CCS with parallel.
|
Year | DOI | Venue |
|---|---|---|
1995 | 10.1006/inco.1995.1129 | Information & Computation |
Keywords | DocType | Volume |
bisimulation equivalence,context-free process,model checking | Journal | 121 |
Issue | ISSN | ISBN |
2 | Information and Computation | 3-540-55822-5 |
Citations | PageRank | References |
108 | 8.32 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Søren Christensen | 1 | 108 | 8.32 |
| Hans Hüttel | 2 | 317 | 40.54 |
| Colin Stirling | 3 | 934 | 102.50 |