Behavioural Preorders via Graded Monads

TL;DR

This paper introduces a unified semantic framework using graded monads on posets to characterize various behavioural preorders and their modal logics, generalizing existing process equivalence theories.

Contribution

It develops a general approach to model behavioural preorders with graded monads on posets and links them to graded inequational theories and characteristic modal logics.

Findings

Framework applies to labelled transition systems

Framework extends to probabilistic transition systems

Provides criteria for logic expressiveness

Abstract

Like notions of process equivalence, behavioural preorders on processes come in many flavours, ranging from fine-grained comparisons such as ready simulation to coarse-grained ones such as trace inclusion. Often, such behavioural preorders are characterized in terms of theory inclusion in dedicated characteristic logics; e.g. simulation is characterized by theory inclusion in the positive fragment of Hennessy-Milner logic. We introduce a unified semantic framework for behavioural preorders and their characteristic logics in which we parametrize the system type as a functor on the category $\mathsf{Pos}$ of partially ordered sets following the paradigm of universal coalgebra, while behavioural preorders are captured as graded monads on $\mathsf{Pos}$, in generalization of a previous approach to notions of process equivalence. We show that graded monads on $\mathsf{Pos}$ are induced by a form of graded inequational theories that we introduce here. Moreover, we provide a general notion of modal logic compatible with a given graded behavioural preorder, along with a criterion for expressiveness, in the indicated sense of characterization of the behavioural preorder by theory inclusion. We illustrate our main result on various behavioural preorders on labelled transition systems and probabilistic transition systems.