Behavioural Equivalence for Infinite Systems—Partially Decidable!

Mogens Nielsen, Kim Sunesen


For finite-state systems non-interleaving equivalences are computationally
at least as hard as interleaving equivalences. In this paper we show
that when moving to infinite-state systems, this situation may change
We compare standard language equivalence for process description languages with two generalizations based on traditional approaches capturing non-interleaving behaviour, pomsets representing global causal dependency, and locality representing spatial distribution of events.
We first study equivalences on Basic Parallel Processes, BPP, a process
calculus equivalent to communication free Petri nets. For this simple
process language our two notions of non-interleaving equivalences agree.
More interestingly, we show that they are decidable, contrasting a result of
Hirshfeld that standard interleaving language equivalence is undecidable.
Our result is inspired by a recent result of Esparza and Kiehn, showing
the same phenomenon in the setting of model checking.
We follow up investigating to which extent the result extends to larger
subsets of CCS and TCSP. We discover a significant difference between
our non-interleaving equivalences. We show that for a certain non-trivial
subclass of processes between BPP and TCSP, not only are the two equivalences different, but one (locality) is decidable whereas the other (pomsets) is not. The decidability result for locality is proved by a reduction to the reachability problem for Petri nets.

Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library