Some results about logical descriptions of non deterministic behaviours

Abstract

Process logics, also called temporal logics, generally rely on an extension of modal logic often called Hennessy and Milner Logic (HML). In this paper, we show how HML modalities induce some semantic overloading of usual logic connectives. We build then a logic of processes that expresses better (deterministic) action choices and (non deterministic) execution choices. We prove that our logic is equivalent, in term of expressivity, to a strict extension of HML, though, in some sense, it still have the same discriminating power, i.e. under usual finiteness assumption, the logical indistinguishability coincides with a natural extension of the bisimulation equivalence.