Basic Parallel Processes (BPP) are a very natural subclass of the class of CCS processes. They are a simple model for the description of infinite state concurrent systems. BPPs are closely related to communication-free Petri nets, a special class of labeled Petri nets, where every transition has exactly one place in its preset. Unlike for general Petri nets, it is decidable if a BPP and a finite state labeled transition system are weakly bisimulation equivalent. This is the first time that weak bisimulation equivalence to a finite state labeled transition system is proved decidable for a non-trivial model of infinite state concurrent systems. While language equivalence is undecidable for communication-free nets and so far only non-primitive recursive algorithms exist for deciding strong bisimulation equivalence, in the subcase of one-to-one labeled communication-free nets the strong bisimulation/language equivalence problem is decidable in polynomial time. For communication-free nets a model checking problem for a weak branching time temporal logic is shown to be PSPACE-complete. Moreover, subproblems of this model checking problem for communication-free nets are complete for the n-th order of the polynomial time hierarchy.     «

Basic Parallel Processes (BPP) are a very natural subclass of the class of CCS processes. They are a simple model for the description of infinite state concurrent systems. BPPs are closely related to communication-free Petri nets, a special class of labeled Petri nets, where every transition has exactly one place in its preset. Unlike for general Petri nets, it is decidable if a BPP and a finite state labeled transition system are weakly bisimulation equivalent. This is the first time that weak...     »