On fixpoint logics and equivalences for processes with restricted nondeterminism

摘要

In concurrency, processes can be studied using a partial order or an interleaving semantics. In partial order semantics, at least four different kinds of behaviour can be recognized: concurrency, causality, conflict and confusion. In interleaving semantics, only conflicts can be observed. All these features can be characterized in logical terms, and various logics have been defined for this purpose. For instance, Hennessy-Milner logic is a modal language that captures strong bisimilarity, the standard bisimulation equivalence for processes with interleaving semantics. However, when considering processes with partial order semantics, stronger equivalences are used and more discriminating logics are needed. In the present article, we study conditions to ease the definition of such logics and equivalences for processes with partial order semantics. More specifically, we study the impact that nondeterminism can have on some fixpoint modal logics and bisimulation equivalences for concurrent and multi-agent systems, when it is systematically restricted within the four kinds of behaviours mentioned above. Our results show that when the concurrency and confusion relations are taken to be deterministic, then the main equivalence for causal behaviour can be completely captured (even in logical and game-theoretic terms) by a simpler, weaker, more local bisimulation relation. We also provide key examples of the kinds of processes that can be modelled using deterministic confusion to illustrate the expressive power of the general framework defined here.