Behavioural Equivalence for Infinite Systems—Partially Decidable!

Resumé

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
dramatically.
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.