The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found in the linear-time / branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.

We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity $λ$ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders ($λ=ω$) or metric spaces ($λ=ω_1$). We establish a bijective correspondence between $λ$-accessible enriched monads on the given category of relational structures and a notion of $λ$-ary algebraic theories (i.e. with operations of arity $

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 Pos of partially ordered sets following the paradigm of universal coalgebra, while behavioural preorders are captured as graded monads on Pos, in generalization of a previous approach to notions of process equivalence. We show that graded monads on 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.

Abstract Finitary monads on Pos are characterized as precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analogously, finitary enriched monads on Pos are characterized: here we work with varieties of coherent algebras which means that their operations are monotone.