{'fraction_non_alphanumeric': 0.057600373119825875, 'fraction_numerical': 0.011523961288818066, 'mean_word_length': 3.7063288823852205, 'pattern_counts': {'":': 0, '<': 12, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 33, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Behavioural Preorders via Graded Monads

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 in the coalgebraic paradigm while behavioural preorders are captured as graded monads on the category Pos of partially ordered sets, in generalization of a previous approach to notions of process equivalence. We show the equivalence of graded monads on Pos with theories in a form of graded ordered algebra 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.


Introduction
Notions of process equivalence, e.g. cast as notions of state equivalence on labelled transition systems, vary on a broad scale from bisimilarity to trace equivalence, referred to as the linear-time branching-time spectrum [7]. Similar phenomena arise in other system types, e.g. in probabilistic transition systems [13], where the spectrum ranges from probabilistic bisimilarity to probabilistic trace equivalence. In the present paper, we are concerned with spectra of behavioural preorders (rather than equivalences), in which a process A is considered to be 'above' a process B if A can, in some sense, match all behaviours of B. Wellknown behavioural preorders on labelled transition systems include simulation and variants thereof such as ready or complete simulation, as well as various notions of trace inclusion.
Previous work [5,23] has shown that graded monads on the category Set of sets provide a useful generic framework that captures the most important equivalences on the linear-time branching-time spectrum, as well as the mentioned equivalences on probabilistic systems. Graded monads thus put process equivalences on an algebraic footing. We now extend this paradigm to behavioural preorders on processes, using graded monads on the category Pos of partial orders. We provide a notion of graded ordered algebraic theory and show such theories are equivalent to finitary graded monads on Pos in the same sense as standard algebraic theories are equivalent to monads on Set. We illustrate this framework by showing that it subsumes well-known notions of simulation and trace inclusion on labelled transition systems and on probabilistic transition systems.
Both equivalences and preorders on processes can often be characterized in terms of theory coincidence or theory inclusion in dedicated modal logics, which are then called characteristic logics. The archetypal result of this type is the classical Hennessy-Milner theorem, which states that states in finitely branching labelled transition systems are bisimilar iff they satisfy the same formulae of Hennessy-Miler logic, i.e. if the theories of the two states coincide [9]; similarly, a state y in a finitely branching labelled transition system simulates a state x iff the theory of x in the positive fragment of Hennessy-Milner logic is included in that of y. We lift generic results on characteristic logics for process equivalences [5,23] to the setting of behavioural preorders, obtaining a general criterion that covers numerous characteristic logics for simulation-and trace-type behavioural preorders on labelled transition systems and probabilistic transition systems.
Related Work There have been a number of approaches to capturing process equivalences coalgebraically, e.g. based on distributive laws inducing liftings of functors to Kleisli [8] or Eilenberg-Moore [11] categories of a monad split off from the type functor, and corecursive algebras [10], whose precise relationship to graded monads has been discussed in previous work [5,23]; roughly speaking, these approaches cover bisimulation-type equivalences and trace-type equivalences but do not appear to subsume intermediate equivalences such as simulation equivalence. Equivalences may be defined by distinguishing suitable modal logics [18], while we pursue the opposite approach of designing characteristic logics for given equivalences or preorders. Variations within trace-type equivalences, such as complete or ready trace semantics, can be captured via so-called decorations [4]. In recent work [19], Kupke and Rot present a highly general fibrational framework for coinductive predicates and their characteristic logics. The focus on coinductive predicates implies a certain degree of orthogonality to the fundamentally inductive framework of graded monads; e.g. trace equivalence is not a coinductive predicate. On the other hand, the cited framework does cover simulation-type equivalences. The fibrational setup implies a very high level of generality, while the framework of graded monads aims at encapsulating as much proof work as possible at the generic level. Levy [21] presents a unified approach to simulation-type equivalences, based on so-called relators. Kapulkin et al. [14] give a coalgebraic generic criterion for expressiveness of characteristic logics for notions of simulation that are uniquely induced from the system type, given as a functor on Pos (while graded monads allow varying behavioural preorders on a given system type). This criterion in fact turns out to be a special case of our main result.
Graded monads originally go back to Smirnov [29], and have subsequently been generalized to indices from a monoidal category [15,22]. Our (graded) ordered algebraic theories generalize existing systems with only discrete arities [2], which correspond to strongly finitary monads [14].

Preliminaries
We begin by recalling some basic results on the category Pos of posets and monotone maps and in (universal) coalgebra [26] -a framework allowing for the unified treatment of a variety of reactive system types -paying special attention to the basic theory of coalgebras on Pos.
Notation 2.1. Throughout this paper, we denote by 1 the terminal object of Pos, the one element poset, and we write ! : X → 1 to denote the unique morphism from a poset X into 1.

Posets
Recall that the category Pos of posets and monotone maps is a cartesian closed category with exponentials given by the hom-sets Pos(X, Y ) of all monotone maps f : X → Y , ordered point-wise. For a monotone map g : Definition 2.2. A functor F : Pos → Pos is locally monotone (or enriched ) if, for every pair f, g ∈ Pos(X, Y ), we have F f ≤ F g whenever f ≤ g. Example 2.3. (1) A convex subset of a poset X is a set S ⊆ X such that x, y ∈ S implies that every z ∈ X with x ≤ z ≤ y lies in S. We say that S is finitely generated if there exists n ∈ ω and s 1 , . . . , s n ∈ S such that S is the convex hull conv(s 1 , . . . , s n ) of the s i . That is, S is finitely generated if it admits a finite subset such that for all s ∈ S either s = s i for some i ≤ n or there exists i, j such that s i ≤ s ≤ s j .
(2) We denote by C ω : Pos → Pos the functor which assigns to each poset X the poset C ω X of finitely generated convex subsets of X, ordered by the Egli-Milner ordering. That is, for all A, B ∈ C ω X, we put The action of C ω on a monotone map f : X → Y is given via the assignment conv(s 1 , . . . , s n ) → conv(f (s 1 ), . . . , f (s n )).
Then C ω is locally monotone.
Proposition 2.5. A monotone map f : X → Y is an embedding if and only if it is a regular mono in Pos.

Coalgebras on Pos
Given a functor G : Pos → Pos, a G-coalgebra is a pair (X, γ) consisting of a poset X of states and a monotone map γ : X → GX, the successor map, assigning to each state x ∈ X its collection γ(x) ∈ GX of successors.
Just as in the Set-based setting, coalgebras over posets come with a natural notion of behavioural equivalence of states. Moreover, as coalgebras over posets enjoy the additional structure of a partial ordering on their states, they also come equipped with a notion of behavioural order on states. A coalgebra morphism from (X, γ) to a G-coalgebra (Y, δ) is a monotone map h : X → Y such that δ · h = Gh · γ holds. We say that y ∈ Y simulates x ∈ X if there exist coalgebra morphisms f : (X, γ) → (Z, ζ), g : (Y, δ) → (Z, ζ) such that f (x) ≤ g(y); we say that x and y are behaviourally equivalent if f, g can be chosen so that f (x) = g(y).
Example 2.6. Building on Example 2.3, we now introduce a notion of Alabelled transition system (A-LTS) in Pos.
(1) Fix a set A of actions. By A × (−) we denote the product functor, which maps a poset X to the poset A × X whose underlying partial order is given by product ordering with A viewed as a discretely ordered poset. Thus, for all (a, x), (b, y) ∈ A × X, we put (a, x) ≤ (b, y) if and only if a = b and x ≤ y.
(2) By an A-LTS, we understand a coalgebra for the functor C ω (A × (−)). Such a coalgebra γ : X → C ω (A × X) assigns to each state x ∈ X a finitely generated convex set γ(x) ∈ C ω (A × X) of pairs (a, y) representing that y is an a-successor of x.
It is not hard to see that for an A-LTS (X, γ), states x, y ∈ X are bisimilar if x ≤ y. Indeed, the underlying partial ordering on the poset X of states is itself a witnessing bisimulation. In particular, the notions of similarity and behavioural equivalence for C ω (A × (−))-coalgebras coincide, and both correspond to bisimulation in the usual coalgebraic sense.
Remark 2.7. Ordered transition systems appear in the context of the more restrictive well-structured transition systems (e.g. [27]). They are defined as triples (X, ≤, →) where (X, ≤) is a poset and → is an accessibility relation satisfying a compatibility condition requiring that ≤ is a simulation relation on the transition system (X, →). These correspond to coalgebras for the finitely generated downwards-closed powerset functor P ↓ ω which assigns a poset to its set of finitely generated downsets ordered by set inclusion. A-LTS on Pos as defined above are precisely ordered transition systems satisfying a stronger bi-compatability condition requiring that ≤ is even a bisimulation on (X, →).
In the sequel, we will be interested in an alternative notion of simulation which only accounts for the finite-step behaviours of states in G-coalgebras. Explicitly, for a G-coalgebra γ : X → GX, we inductively define a sequence γ n : X → G n 1 of maps by taking γ 0 to be the unique map X → 1 and γ n+1 = Gγ n · γ. For states x ∈ X, y ∈ Y in G-coalgebras γ : X → GX and δ : Y → GY , we say that x is ω-similar to y if γ n (x) ≤ δ n (y) for all n ∈ ω. Extending a wellknown result of Worrell [30], Adámek [1,Thm. 4.6] showed that ω-simulation and coalgebraic simulation coincide for every finitary functor G on Pos preserving epis (i.e. surjections) and regular monos (i.e. embeddings).
Convention 2.8. For the remainder of this paper, we work with finitary enriched functors G preserving epis and regular monos. This means that the final G-coalgebra exists and characterizes ω-simulation in the sense described above.

Graded Monads and Graded Algebras
We now recall the necessary background on graded monads and their algebras.  (1) For every endofunctor G on C , the n-fold composition M n = G n defines a graded monad with unit η = id and multiplication µ n,k = id G n+k .
(2) Every monad (M, η, µ) on Pos defines a graded monad with M n X := M (A n × X) [23]. In the Set-based setting, the instantiation of this example to the finite power set monad M = P ω is related to trace equivalence on labelled transition systems.

Graded Algebras
Just as in the case of plain monads, graded monads enjoy both Eilenberg-Moore and Kleisli-style constructions [6]. In particular, graded monads come equipped with a notion of graded algebras, which we recall presently for later use in the semantics of graded logics.
Definition 3.3. Let n ∈ ω and let M be a graded monad on a category C . A M n -algebra A = ((A k ) k≤n , (a mk ) m+k≤n ) consists of a family (A k ) k≤n (the carriers of A) of C -objects and a family of morphisms in C (structure maps) such that a 0,m · η Am = id Am for all m ≤ n and, whenever m + k + r ≤ n, the diagram below commutes: M ω -algebras and their morphisms are defined similarly by allowing indices to range over all m, r, k ∈ ω.
We will be particularly interested in depth-1 graded monads, recalled in Section 4.4, in which M n -algebras may be constructed from M 1 -algebras (cf. Theorem 4.15). As such, we now examine the M 0 -and M 1 -algebras in closer detail. (1) We note that every C -object X gives rise to an M 0 -algebra with carrier M 0 X and algebra structure µ 0,0 X : M 0 M 0 X → M 0 X. Indeed, the only instance of Diagram (1) commutes by the associative law of the monad M 0 .
(2) More generally, using the corresponding identity and associativity laws of the graded monad M, the pair (M n X, µ 0,n X : M 0 M n X → M n X) defines an M 0algebra for all n ∈ ω. Instantiating this example to X = M k Y, it follows that of the graded monad M states precisely that µ n,k X : M n M k X → M n+k X is a morphism from (M n M k X, µ 0,n M k X ) to (M n+k X, µ 0,n+k X ).
Example 3.5 (M 1 -algebras). An M 1 -algebra consists of M 0 -algebras (A 0 , a 00 ) and (A 1 , a 01 ) and a main structure map a 10 : M 1 A 0 → A 1 satisfying two instances of Diagram (1); one stating that a 10 is a morphism of M 0 -algebras from (M 1 A 1 , µ 01 A1 ) to (M 0 A 1 , a 01 ) and the other stating that the diagram M1a 00 commutes in the category of M 0 -algebras.
We recall the following result concerning the category of M n -algebras which plays a role in the interpretation of propositional operators in graded logics. Explicitly, the product of an I-indexed family A i = ((A i k ) k≤n , (a mk i ) m+k≤n ) of M n -algebras has carriers i∈I A i k for k ≤ n and structure maps given by the following composition:

Canonical M 1 -algebras
Those M 1 -algebras for which Diagram (2) is a coequalizer are of particular interest for later use in the semantics of graded logics. Such algebras can be characterized as precisely the free M 1 -algebras with respect to the forgetful functor taking an M 1 -algebra to its underlying 0-part [5]. We recall the details presently.
Definition 3.7. The 0-part of an M 1 -algebra A is its underlying M 0 -algebra (A 0 , a 00 ). Taking 0-parts defines a functor Z from the category of M 1 -algebras to the category of M 0 -algebras which maps a morphism (h 0 , h 1 ) of M 1 -algebras to h 0 . An M 1 -algebra A is canonical if it is free over its 0-part with respect to the functor Z and inclusion map id A0 .

Presentations of Graded Monads on Pos
We now introduce a notion of ordered algebraic theories in context which capture finitary enriched graded monads on Pos. This correspondence is the key to isolating a suitable analogue of the notion of depth-1 graded monad [23] which, in turn, is the main ingredient for compositional graded logics. Moreover, this correspondence allows us to transfer to an algebraic perspective on graded behavioural preorders on coalgebras (Section 5).

Graded Signatures over Contexts
For the remainder of this paper, we fix a set Pos f of finite posets representing all finite posets up to isomorphism, the elements of which we shall call contexts.
(1) By a graded signature over contexts we understand a mapping Σ assigning to each context Γ in Pos f and n ∈ ω a set Σ(Γ, n) of depth-n Σ-operations of arity Γ . We denote by d(f ) the depth of the operation f .
(2) By a (Σ, n)-algebra A we understand a family of posets (A k ) k≤n together with a family of monotone maps One might have expected that we would work with a classical notion of signature given by an assignment of each natural number n to a set Σn of operations of arity n which are meant to be interpreted as n-ary monotone maps on algebras carried by a poset. Such algebras were studied by Bloom [2,3]. More recently, Kurz and Velebil [20] showed that varieties of such algebras (specified by inequalities s ≤ t between terms s, t) correspond to strongly finitary monads on Pos [20] in the sense of Kelly and Lack [16]. Finally, we note that the idea to work with operations with partially ordered (finite) aritites traces back to the work of Kelly and Power [17].

Terms and Inequations in Context
We now introduce a logic of inequations in context which provides an explicit description of the (absolutely) free Σ-algebra on a given context Γ, whose elements will be called the terms with variables in context Γ . Definition 4.3. For every k ∈ ω, we generate the poset (T Σ (Γ, k), ≤) of Σterms with variables in context Γ of uniform depth k recursively via the following calculus of rules for term formation (top row) and rules for ordering terms (second and third row); that is, we have t ∈ T (Γ, k) iff Γ ⊢ k t: The poset T Σ (Γ ) of uniform Σ-terms in context Γ is given by the coproduct (in Pos) over the T Σ (Γ, k).
We note that every term t ∈ T Σ (Γ, k) has one of two shapes: t is either a variable in context Γ (and k = 0) or there exists ∆ ∈ Pos f and f ∈ Σ(∆, m) such that t = f (σ) for some monotone map σ : ∆ → T Σ (Γ, n) with m + n = k. In other words, every variable in context Γ is a term of uniform depth 0 and f (t 1 , . . . , t n ) is a term (in context Γ ) of uniform depth k whenever all t i are terms (in context Γ ) of uniform depth m such that d(f ) + m = k and the t i 'satisfy' the arity of f. Unwinding the rules for ordering relations, it is easy to verify that for all Observe, too, that every constant c (i.e. operations whose arity is the empty poset) has uniform depth k for every k ≥ d(c).
Example 4.4. Let Σ be a signature consisting of a depth-0 binary operation + with arity {0 < 1} and a unary depth-0 operation a(−) of arity 1. Then every Σ-term in context Γ of uniform depth 0 is either a variable from Γ or a finite sum of variables. Moreover, at depth-1, every term is given by a non-empty finite sum of terms of the shape a(t) where t has uniform depth 0. Observe that the expression x + a(y) is not a term: (i) x and a(y) do not have the same uniform depth and (ii) the terms x and a(y) are incomparable whence Γ ⊢ x ≤ a(y) is not derivable.
Apart from the appropriate notion of substitution of terms, the poset of uniform Σ-terms in context comes with the usual syntactic notions (e.g. subterms), defined as expected.
In words, a uniform substitution σ interprets each variable in context Γ as some uniform term in context ∆, all of the same uniform depth k. Such an interpretation inductively extends to all uniform terms in context Γ by putting as expected. It is easy to verify that uniformity of σ ensures that its extension maps terms in context Γ of uniform depth m to terms in context ∆ of uniform depth m + k. Moreover, σ preserves derivable inequality (i.e. its extension is monotone). (1) A Σ-inequation in context Γ is a pair (s, t) of Σ-terms in context Γ of the same uniform depth. If s and t have uniform depth k, we say that (s, t) is a Σ-inequation in context Γ of uniform depth k.
(2) A graded theory T is a pair (Σ, E) consisting of a graded signature Σ and a set E of Σ-inequations in context (the axioms of T).
Example 4.7. (1) As a base example for later use in Section 5, we introduce the graded theory J whose signature consists of n-ary depth-1 choice operations for all non-empty words w = a 1 · · · a n ∈ A * , which is just a compact representation of the formal sum a 1 (x 1 ) + · · · + a n (x n ). Thus, given a decomposition of a word w = w 1 w 2 into non-empty words w 1 , w 2 , we will write The axioms of J state that the formal summation over actions is a commutative and monotone operation, which we encode in terms of choice operators as follows: Take note that monotonicity implies that Σ aa (x, x) = Σ a (x) for all a ∈ A, which states that + is idempotent: a(x) + a(x) = a(x). Moreover, associativity of formal summation is immediate. Thus J is the extension of the theory of join semi-lattices in Pos by monotonicity.
(2) The graded theory J + 0 is obtained from J by adding a depth-0 constant 0 which we will understand as the additive identity of formal summation. In particular, we further impose the following axiom for all actions a ∈ A: We now introduce an logic of inequations in context for a theory T. We do so by adding two additional rules to the rule system of Definition 4.3 which axiomatize the role of uniform substitutions. The first rule states that the axioms of T are closed under uniform substitutions. The latter is slightly more technical: its purpose is to ensure that Γ ⊢ k f (t 1 , . . . , t n ) if and only if f (t 1 , . . . , t n ) has uniform depth k and Γ ⊢ k−d(f ) t i ≤ t j is derivable for all i ≤ j in the arity of f.
where the latter is subject to the following condition: there exists an axiom Γ ⊢ m s ≤ t ∈ E and a subterm f (t 1 , . . . , t j ) of s or t with such that each t i has uniform depth n and for some i ≤ j in arity(f ) we have u = t i and u = t j .
Note that the premise of these additional rules states that σ is a uniform substitution, and this is derivable. The first rule simply states that the axioms of T are closed under such substitutions, whereas the latter rule -which might well be called the arity rule -is slightly more obtuse. We note that, in its absence, the arity of an operation f is not characterized by derivability in general. In particular, the main role of arity rule is is to ensure that whenever a graded inequation Γ ⊢ n s ≤ t is derivable, then both Γ ⊢ n s and Γ ⊢ n t are derivable as well.
Notation 4.9. By an abuse of notation we denote by Γ ⊢ k s ≤ t the Σ-If s, t ∈ T Σ (Γ, k), we denote their associated Σ-inequation in context Γ , (s, t), by Γ ⊢ k s ≤ t and say that Γ ⊢ k s ≤ t has uniform depth k. We denote by Γ ⊢ k s = t the conjunction of the inequations Γ ⊢ k s ≤ t and Γ ⊢ k t ≤ s.

Graded Monads and Graded Theories
We will now describe a correspondence between graded theories and finitary enriched graded monads on Pos.
A graded theory (Σ, E) induces a finitary enriched graded monad on Pos by taking M n X to be the poset of T-terms of uniform depth n with variables from X modulo derivable equality. Then, as usual, the unit and multiplication are defined as the inclusion of variables as terms and the collapsing of layered terms, respectively.
Conversely, a finitary enriched graded monad (M n ) n<ω on Pos induces a graded theory (Σ, E) whose signature is given by putting Σ(Γ, n) := M n Γ for every context Γ and every n ∈ ω. Then, for a poset X, each Σ-term t of uniform depth has a canonical interpretation t ∈ M n X defined recursively in the usual way. We let E consist of an inequation in context Γ ⊢ n s ≤ t just in case s ≤ t in M n Γ. Proposition 4.10. For every n ∈ ω, ((M m X) m≤n , (µ mk ) m+k≤n ) is the free M n -algebra on X with respect to the forgetful functor which maps an M n -algebra ((A m ), (a mk )) to A 0 and an M n -morphism (f k ) to f 0 .
Proof. Given an M n -algebra ((A k ), (a mk )) and a monotone map f :

Depth-1 Graded Monads
We shall now recall the notion of a depth-1 graded monad [23] leading to compositional graded logics.  Recall that a natural transformation α : F → G between endofunctors on Pos is an epi-transformation if all of its components are surjective. We have the following characterization of finitary depth-1 graded monads on Pos, the proof of which is completely analogous to the corresponding Set-based result [23,Prop. 7.3]. The key difference in our setting rests in the additional assumption that M 1 µ 1,n is an epi-transformation; this is automatic in the Set-based case since functor on Set preserves epimorphisms.
is object-wise a coequalizer diagram in the category of M 0 -algebras.

Behavioural Preorders via Graded Monads
Definition 5.1. Let G : Pos → Pos be a functor. A graded behavioural preorder on G-coalgebras is induced from a graded monad M on Pos and a natural transformation α : G → M 1 . The sequence (γ (n) : X → M n X) n<ω of n-step (M, α)-behaviours for a G-coalgebra γ : X → GX is defined by For states x ∈ X and y ∈ Y in G-coalgebras γ : X → GX and δ : Y → GY, we say that x is a (M, α)-refinement of y if M n ! · γ n (x) ≤ M n ! · δ n (y) for all n ∈ ω.
Coalgebraic Simulation Recall from Example 3.2 that taking M n = G n defines a graded monad. By taking α = id, it is easy to verify that ((G n ) n<ω , id)refinement is precisely ω-simulation in the sense of Section 2.2. In particular, ((G n ) n<ω , id)-refinement corresponds to coalgebraic simulation if G is finitary.
For example, taking G = C ω yields bisimilarity on A-LTS in Pos. (It may seem surprising that we obtain bisimilarity as a behavioural preorder in this case; however, recall from Remark 2.7 that the ordering on an A-LTS in Pos is a bisimulation, and also that on discrete orders, C ω is the standard powerset equipped with the discrete ordering.) Similarity Let J be the graded theory from Example 4.7. The graded monad induced by J has M n = P ↓ ω and thus fits the profile of the previous example, again with α = id. In particular, the corresponding graded behavioural preorder corresponds to simulation on P ↓ ω -coalgebras which is similarity in the classic sense [21]. Further simulation-type behavioural preorders such as ready simulation and complete simulation are covered in a straightforward manner by adding factors to the action set. E.g. ready similarity, which additionally requires states to have the same ready sets, i.e. sets of enabled actions, is covered by taking G = P ↓ ω (P ω (A) × A × (−) + 1), with P ω (A) discretely ordered and 1 denoting deadlock. The original functor P ↓ ω (A × (−)) is then transformed into G by mapping S to {(π 1 [S], a, x) | (a, x) ∈ S} for S = ∅, where π 1 denotes the first projection, and to the unique element of 1 otherwise. This is similar to decoration-oriented coalgebraic approaches to trace semantics [4].
Synchronisation Recall the theory J + 0 from Example 4.7. The induced notion of behavioural preorder is in fact, like in the case of bisimilarity, a notion of process equivalence that one might term synchronous bisimilarity: Recall that two states are (finite-depth) bisimilar iff have the same tree unfoldings at every finite depth, where the relevant trees have set-based branching in the sense that every node is identified by its set of children. In these terms, two states are synchronously bisimilar if they have the same pruned tree unfolding at every finite depth, where the pruning removes all branches of the tree that end in deadlocks before the current depth is reached.
Probabilistic Trace Inclusion We capture probability subdistributions (which are defined like distributions except the global mass is only required to be at most 1 rather than exactly 1) by the algebraic theory of subconvex algebras (also known as positive convex modules [25]), whose operations are formal subconvex combinations n i=1 p i · (−) for p i ≤ 1, and whose equations reflect the laws of (plain) monad algebras: The equation δ ik ·x k = x i , with δ ik being Kronecker delta (δ ik = 1 if i = k, and δ ik = 0 otherwise), reflects compatibility with the unit, and the equation scheme reflects compatibility with the monad multiplication. We further impose inequations of the form {x 1 , . . . , Interpreting this algebraic theory over Pos yields a subdistribution monad S on Pos.
Coalgebras for the functor S(A × (−)) on Pos then are ordered probabilistic transition systems with possible deadlock. We define a graded monad on Pos by taking subconvex combinations as operations of depth 0, and the actions as unary operations of depth 1; besides the mentioned equations of subconvex algebras, we include equations stating that the actions distribute over subconvex combinations, i.e. for k i=1 p i ≤ 1 and a ∈ A, we postulate depth-1 equations The induced graded behavioural preorder is probabilistic trace inclusion.

Graded Characteristic Logics for Behavioural Preorders
We will now recall the general setup of graded logics [5,23]. The syntax of graded logics is parameterized over a set Θ of truth constants, a set O of propositional operators with assigned finite arities, and a set Λ of modalities with assigned finite arities, which we fix for the remainder of the paper. For readability, we restrict our technical discourse to unary modalities; the treatment of higher arity modalities is handled with additional indexing. where ψ is a formula of uniform depth n.
The semantics of graded formulae is further parameterized in an endofunctor G on Pos, a graded behavioural preorder (M = ((M n ), η, (µ nk )), α) with M depth-1, and an M 0 -algebra (Ω, o : M 0 Ω → Ω) of truth values, which we fix for the remainder of the paper. In light of Proposition 3.6, powers Ω k of Ω are again M 0 -algebras.
Example 6.2. Recall that finite-depth G-similarity is given by the graded monad (G, id). As M 0 = G 0 is the identity monad, an M 0 -algebra is simply a poset Ω with structure map o : Ω → Ω given by the identity on Ω. As a further very simple example, in the graded monad induced by the graded theory J + 0 (Example 4.7(2)), M 0 -algebras are just partially ordered sets with a distinguished element 0. Further examples will be seen later. For every canonical M 1 -algebra A and every M 0 -morphism f : A 0 → Ω, we write L (f ) to denote the unique M 0 -morphism extending f to an M 1 -morphism A → A L . That is, L (f ) is the unique M 0 -morphism such that the square below commutes: The meaning of a graded formula ϕ of uniform depth n in a G-coalgebra γ : X → GX is given by the map We note that, for each n ∈ ω, the evaluation L(ϕ) of formulae of the shape L(ϕ) of uniform depth n is defined since (M n 1, µ 0,n 1 ) is the 0-part of the M 1algebra with carriers (M n 1, M n+1 1) and multiplication as structure, which is canonical by Corollary 4.14. That is, L ( ϕ ) exists and is an M 0 -morphism of the type M n+1 1 → Ω. Example 6.5. We describe characteristic logics for the graded behavioural preorders of Section 5. In the first two examples, we take the truth object Ω to be ¾, the linear order {⊥ < ⊤} and, in the final example on probabilistic trace inclusion, we fix Ω = [0, 1].
Positive Coalgebraic Modal Logic: Recall from Section 5 that the graded monad with M n = G n captures coalgebraic similarity on G-coalgebras. Then, as noted in Example 6.2, an M 0 -algebra is just a poset with structure map given by the identity id ¾ . It follows that every monotone map ¾ k → ¾ is an M 0 -morphism.
Thus, we can take all lattice operations as propositional operators. Furthermore, M 1 -algebras are given by maps a 10 : GA 0 → A 1 , and modalities are interpreted as maps G¾ → ¾.
Observe that the evaluation of such maps according to Definition 6.4 corresponds precisely to the meaning of modalities in coalgebraic modal logic; the absence of negation means that we are in the setting of positive coalgebraic modal logic. Thus, for A-LTS, we obtain positive basic modal logic by taking modalities ♦ a for all a ∈ A with ♦ a : C ω (A × ¾) → ¾ defined by ♦ a (S) = ⊤ if and only if (a, ⊤) ∈ S.
Simulation: One particular instantiation of the example above is similarity on A-LTS, which arises via the graded monad with M n = G n where G = P ↓ ω (A×(−)). As indicated above, we can use conjunction as a propositional operator, which is explicitly defined by the M 0 -morphism given by ∧ (x, y) = ⊤ if and only if x = ⊤ = y. We take the arising logic to include conjunction and modalities ♦ a for each a ∈ A. Of course, this logic is well known to characterise similarity [7]; we will show that this fact arises by straightforward application of the general criterion we establish in the next section. The adaptation of the logic to further simulation-type preorders such as ready simulation is achieved by indexing the modalities with ready sets I like in earlier work on graded process equivalence [5]: ♦ a,I φ requires, besides satisfaction of ♦ a φ, that the ready set is exactly I.
Probabilistic Trace Inclusion: Recall that probabilistic transition systems (with actions in A) in Pos are S(A × (−))-coalgebras, and probabilistic trace inclusion is given by the graded monad with M n = S(A n × (−)). In particular, we have M 0 ∼ = S unlike the previous examples where M 0 is the identity. We take the ensuing logic L Prob to consist of modalities from Λ := { a | a ∈ A} and a single truth constant ⊤. As mentioned above, we take Ω = [0, 1] as the object of truth values which is made into a subconvex algebra by taking expected values (i.e. by mapping formal subconvex combinations to their respective arithmetic sums). We define ⊤ = 1 ∈ [0, 1], and we take the interpretation of the modality a to be the M 1 -algebra This logic is invariant for probabilistic trace inclusion by design; we will see that it is also expressive.

Expressiveness
We generalize the expressiveness criterion for Set-based graded logics as follows.
Recall that an I-indexed family f i : X → Y of morphisms in Pos is said to be jointly order-reflecting if for all x, y ∈ X we have that x ≤ y whenever f i (x) ≤ f i (y) for all i ∈ I. Definition 6.6. We say that L is (1) depth-0 separating if the family ( c : M 0 1 → Ω) c∈Θ is jointly orderreflecting; (2) depth-1 separating if for every canonical M 1 -algebra A and every jointly order-reflecting family A of M 0 -homomorphisms A 0 → Ω that is closed under the propositional operators in O (i. e. p f 1 , . .
is jointly order-reflecting.
Theorem 6.7. Let L be a depth-0 separating and depth-1 separating graded logic. Then, for every n ∈ ω, the family ϕ : M n 1 → Ω of evaluations of uniform depth n formulas is order-reflecting. In particular, L is expressive.
We will apply our expressiveness criterion to the graded logics introduced in Example 6.5. In most cases, this amounts to showing depth-1 separation only.
Coalgebraic ω-simulation: Let G be a finitary enriched functor on Pos preserving embeddings and surjections. Then the graded monad with M n = G n captures (coalgebraic) similarity. As noted, M 0 -algebras are just posets and modalities in the described graded logic are maps L : G¾ → ¾. Using that the functor G is enriched, it follows from the enriched Yoneda Lemma that such maps are equivalent to monotone predicate liftings, which in the present context we understand as operations λ that lift monotone predicates X → ¾ to monotone predicates GX → ¾, subject to a naturality condition. In generalization of the discrete notion of separation [24,28], we say that Λ, understood as a set of monotone predicate liftings in this sense, is separating if whenever t, s ∈ GX are such that λ(f )(t) ≤ λ(f )(s) for all λ ∈ Λ and all monotone f : X → ¾, then t ≤ s; this is precisely the notion of separation used by Kapulkin et al. [14]. E.g. the standard diamond modality on P ↓ ω , i.e. the predicate lifting given by (S) = ⊤ iff ⊤ ∈ S, is separating. In this terminology, we have Theorem 6.8. If the set Λ of monotone predicate liftings for G is separating and G is finitary and enriched, and preserves embeddings and surjections, then the logic L arising by taking ⊤ as the only truth constant and disjunction and conjunction as propositional operators is depth-0 separating and depth-1 separating, hence expressive for coalgebraic simulation.
That is, we obtain the existing expressiveness result for positive coalgebraic modal logic [14] by instantiation of Theorem 6.7.
Simulation: Recall that the graded logic L Sim for simulation includes conjunction and modalities ♦ a for each action a ∈ A. In this case, depth-0 separation is trivial; we will illustrate that this logic is furthermore depth-1 separating, so that we recover the well-known result that this logic is also expressive for simulation by instantiation of Theorem 6.7, this improving on the result obtained as a special case of Theorem 6.8, where the logic needed to include also disjunction. Proposition 6.9. The graded logic L Sim is depth-1 separating.
The same holds for the characteristic logics for finer simulation-type equivalences such as ready similarity introduced above, the key being that ♦ I,a requires the ready set to be exactly I.
Probabilistic Trace Inclusion: The application of our expressiveness condition the graded logic L Prob for probabilistic trace inclusion is completely analogous to the proof given for probabilistic trace equivalence in the full version of [5]; indeed, the proof of depth-1 separation becomes slightly easier since the underlying predicates preserve subconvex instead of only convex combinations. Like in the set-based case, having subconvex combinations as propositional operators in the logic is not necessary to obtain expressiveness.

Conclusion
We have introduced a generic framework for behavioural preorders that combines coalgebraic parametrization over the system type (nondeterministic, probabilistic etc.) with a parametrization over the granularity of system semantics. The latter is afforded by mapping the type functor into a graded monad on the category Pos of partially ordered sets. The framework includes support for designing characteristic logics; specifically, it allows for identifying, in a straightforward manner, propositional operations and modalities that automatically guarantee preservation of formula satisfaction under the behavioural preorder, and it offers a readily checked criterion for the converse implication, standardly referred to as expressiveness. Important topics for future research include the development of generic minimization and learning algorithms modulo a given graded semantics, as well as a generic axiomatic treatment of characteristic logics.

Details on the Subdistribution Monad
We will characterize the ordering of the finitely supported subdistribution monad S on Pos. A similar characterization has been provided by Jones and Plotkin [12,Lemma 9.2] in a more restricted domain-theoretic setting (directedcomplete posets). Their argument is based on the max-flow-min-cut theorem; we give an independent, more syntactic argument. Given a poset X, we first note that the terms representing elements of SX can be normalized (in the standard manner known from the set-based case [25]) to a single layer of formal subconvex combinations, i.e. formal sums n i=1 p i · x i where n ∈ ω, x i ∈ X, p i ∈ (0, 1], and i∈I p i ≤ 1. We generally write [n] = {1, . . . , n} for n ∈ ω.
We then also say that (2) We say that a formal subconvex combination Recall that in addition to the standard equational axioms, the theory includes the inequational axiom scheme and moreover that we generally enforce that operations, in this case subconvex combinations, are monotone. If d 1 is a subdivision of d 2 , then the equational part of the theory clearly implies d 1 = d 2 . Moreover, the inequational axiom scheme (5) and monotonicity imply that d 1 ≤ d 2 whenever d 1 ⊑ d 2 . It follows that is included in the ordering ≤ on SX. We will show that the reverse inclusion also holds.
Since the ordering on SX is the smallest partial order (more precisely, the partial order quotient of the smallest pre-order, which however we will show to be already antisymmetric) that contains all instances of the inequational axiom scheme (5) and moreover is preserved by subconvex combinations, it suffices to show that already has these properties. It is clear that subsumes all instances of (5): if p i ≤ q i for all i ≤ n, then n i=1 p i · x i n i=1 q i · x i is witnessed by the trivial subdivisions of these subconvex combinations via the identity on [n]. The monotonicity condition is also easy to see: Lemma A.2. Subconvex combinations preserve both the subdivision relation and the obviously-below relation ⊑, and are hence monotone w.r.t. .
Proof. The second claim clearly follows from the first two. Preservation of the subdivision relation is straightforward by the equational laws of subconvex combinations and distributivity of multiplication. Preservation of ⊑ is seen similarly by the equational laws of subconvex combinations and monotonicity of multiplication by non-negative reals.
⊓ ⊔ It remains to show that is a partial ordering. To this end, it will be convenient to work with two alternative presentation of partitions of real numbers, introduced presently.
For p ∈ [0, 1], we denote by smd(p) the set of summand representations of partitions of p, i.e., the set of sequences p 1 , . . . , p n ∈ (0, 1] (with n referred to as the length of the sequence) such that n i=1 p i = p. We define a partial order → (refines) on smd(p) by (p 1 , . . . , p n ) → (q 1 , . . . , q k ) if and only if (q 1 , . . . , q k ) arises from (p 1 , . . . , p n ) by summing consecutive summands, formally if there exist indices 1 ≤ j 1 < · · · < j n < j k+1 = n + 1 such that q i = ji+1−1 l=ji p l for i = 1, . . . , k. Observe that a subdivision of n i=1 p i · x i may be specified by the choice of an s i ∈ smd(p i ) for each i ≤ n.
Alternatively, we may represent partitions in terms of sequences of partial sums: The set psums(p) of partial-sum representations of partitions of p consists of all finite subsets P ⊆ [0, p) such that 0 ∈ s. When we write P = {q 0 , . . . , q n−1 }, we mean to imply that 0 = q 0 < q 1 < · · · < q n−1 , and implicitly understand q n = p; we refer to n as the length of s. We note the equivalence of the two representations explicitly: which in the left-to-right direction assigns to a summand representation (p 1 , . . . , p n ) ∈ smd(p) the partial-sum representation { k i=1 p i | k = 0, . . . , n − 1}, and in the right-to-left direction assigns to a partial-sum representation {q 0 , . . . , q n−1 } the summand representation (p 1 , . . . , p n ) given by p i = q i − q i−1 .
It follows that the set of subdivisions of a subconvex combination n i=1 p i · x i is in bijection with the set of families (P i ) i≤n such that P i ∈ psums(p i ). We next establish the key properties that will be needed in order to prove that is a partial order. We first note that given subdivisions always have a joint refinement: Proof. One immediately reduces to the case n = 1; we then omit the indices. By Lemma A.3, it suffices to consider partial-sum representations of partitions. But for subdivisions represented by P, Q ∈ psums(p), we obtain a common subdivision from P ∪ Q ∈ psums(p).
⊓ ⊔ Next, we show that subdivisions can be pulled back and pushed forward along the obviously-below relation: Proof. One immediately reduces to the case that n = m = 1; we then omit the indices. Both claims are now seen straightforwardly via partial-sums representations; in detail: Given p · x ⊑ q · y, we have p ≤ q and x ≤ y.
(i) We are given a subdivision of p · x, say in terms of P ∈ psums(p). But then P is also in psums(q), and as such induces the desired subdivision d * of q · y, with the relation d ⊑ d * witnessed by the identity map.
(ii) We are given a subdivision of q · y, say in terms of Q ∈ psums(q). We then obtain s * as desired from Q∩[0, p) ∈ psums(p), with the relation d * ⊑ d witnessed by the inclusion of the respective index sets.
Proposition A.6. The relation is a preorder. Proof.
(1) We first note that is reflexive since every subconvex combination is a subdivision of itself.
(2) We now show that is transitive. To this end, suppose that (a) ℓ i=1 p i · x i m j=1 q j · y j and (b) m j=1 q j · y j n k=1 r k · z k hold; we will show that ℓ i=1 p i · x i n k=1 r j · z j . By (a), we have subdivisions s p ⊑ s pq of ℓ i=1 p i · x i and m j=1 q j · y j , respectively, and, by (b), we are given subdivisions s qr ⊑ s r of m j=1 q j · y j and n k=1 r k · z j , respectively. This is all summarized in the diagram below where an arrow from x to y denotes that x is a subdivision of y. Let s q denote the joint subdivision of s pq and s qr given by Lemma A.4. Then, by Lemma A.5(i), we obtain a subdivision (s p ) * of s p such that s * p ⊑ s q and, by Lemma A.5(ii) we obtain a subdivision (s r ) * of s r such that s q ⊑ (s r ) * . Let f pq and f qr be injections witnessing these relations. Then the composition f qr · f pq is a injection witnessing that (s p ) * ⊑ (s r ) * . Since (s p ) * and (s r ) * are moreover subdivisions of ℓ i=1 p i · x i and n k=1 r k · z k , respectively, it immediately follows that ℓ i=1 p i · x i n k=1 r k · z k , as desired. We note additionally (although this is not strictly needed in the remainder) that the ordering does not cause unexpected identifications on SX; that is, the underlying set of SX is the set of subdistributions on the underlying set of X in the standard sense. For simplicity, we assume the set SX to be given in this way; then this claim may be formulated as follows: Proposition A.7. The relation on SX is antisymmetric.
Proof. Suppose that m i=1 p i · x i n j=1 q j · y j and n j=1 q j · y j m i=1 p i · x i ; we proceed to show that m i=1 p i · x i = n j=1 q j · y j in SX, i.e. that the two terms define the same subdistribution on the underlying set of X in the standard sense. Unwinding our assumptions, we have subdivisions s p0 , s p1 and s q0 , s q1 of m i=1 p i · x i and n j=1 q j · y j , respectively, such that s p0 ⊑ s q0 and s q1 ⊑ s p1 , all as in indicated in the diagram below: Applying Lemma A.4 to s p0 and s p1 , we obtain a common subdivision s p . Then, by Lemma A.5, there exist subdivisions (s p ) * and (s q ) * of s q1 and s q0 , respectively, such that (s p ) * ⊑ s p ⊑ (s p ) * .
By tracing the sum of all coefficients attached to a given x ∈ X through the witnessing injections of these relations, we see that m i=1 p i · x i and n j=1 q j · y j define the same subdistribution, as claimed.
⊓ ⊔ Proof of Proposition 6.9 Let A be a canonical M 1 -algebra with carriers A 0 , A 1 and suppose that A is a jointly order-reflecting family of M 0 -morphisms A 0 → ¾ closed under conjunction. Now, suppose that x ≤ y in A 1 . Since A is canonical, the map a 10 : P ↓ ω (A × A 0 ) → A 1 is surjective, so x, y have the form x = a 10 (↓{(a 1 , x 1 ), . . . , (a n , x n )}) and y = a 10 (↓{(b 1 , y 1 ), . . . , (b n , y n )}) for some (a i , x i ), (b j , y j ) ∈ A × A 0 . By monotonicity of a, there exists i ≤ n such that x i ≤ y j for all j such that a i = b j . As A is jointly order-reflecting, it follows that for each j there is f j ∈ A such that f j (x i ) = ⊤ and f j (y j ) = ⊥. Indeed, as x i ≤ y j it follows that there exists Recall that the modal operator ♦ ai : P ↓ iff (a i , ⊤) ∈ S, and ♦ ai (f ) is defined by commutation of the diagram (an instance of Diagram (4)). Thus, ♦ ai (f )(x) = ♦ ai ↓({(a 1 , f (x 1 )), . . . , (a n , f (x n ))}) = ⊤, and similarly ♦ ai (f )(y) = ⊥, i.e. ♦ ai (f )(x) ≤ ♦ ai (f )(y), as required.

⊓ ⊔
Proof of Theorem 6.7 We proceed by induction on n to show that, for every n ∈ ω, the family ϕ : M n 1 → Ω of evaluations of graded formulas ϕ ∈ L n is jointly orderreflecting. The base case n = 0 follows immediately from depth-0 separation. Let A denote the family of evaluation maps ϕ : M n 1 → Ω of formulas ϕ ∈ L n . By the inductive hypothesis, A is jointly order-reflecting. Moreover, for every k-ary propositional operator p and every ϕ 1 , . . . , ϕ k ∈ L n , we have that p(ϕ 1 , . . . , ϕ k ) ∈ L n whence A is closed under propositional operators in O. By depth-1 separation, it follows that the family Λ(A) = { L ( ϕ ) | L ∈ Λ, ϕ ∈ L n } is jointly order-reflecting. In other words, the family of evaluations of depth-(n + 1) formulas is jointly order-reflecting, as desired.
Finally, we will prove that L is expressive. Let x, y be states in G-coalgebras γ : X → GX and δ : Y → GY such that ϕ γ (x) ≤ ϕ δ (y) for all ϕ ∈ L. We must prove that M n ! · γ n (x) ≤ M n ! · δ n (y) for all n ∈ ω. By assumption, we know that ϕ (M n ! · γ (n) (x)) = ϕ γ (x) ≤ ϕ δ (y) = ϕ (M n ! · δ (n) (y)) for all ϕ ∈ L of uniform depth n and for all n ∈ ω, and we have just shown that the family ϕ : M n 1 → Ω of evaluations of such formulas is jointly orderreflecting. Hence x is a (M, α)-refinement of y, as desired.
Proof of Theorem 6.8 Depth-0 separation is trivial, since M 0 1 = 1. For depth-1 separation, we note first that for finitary G, it suffices to check the condition for finite A 0 . But for finite A 0 and a given jointly order-reflecting set A of monotone maps A 0 → ¾, every monotone h : A 0 → ¾ can be written as a finite join of finite meets of elements of A, so depth-1 separation is immediate from the separation condition assumed in the theorem.

Details on Probabilistic Trace Inclusion
We will show that the logic L Prob is expressive for probabilistic trace inclusion on probabilistic transition systems, which we construe as S(A × −)-coalgebras.
Recall SX is the poset of subdistributions µ : X → [0, 1] X, which we normalize to formal sums n i=1 p i · x i where n ∈ ω, p i ∈ (0, 1], and n i=1 p i ≤ 1; its partial ordering ≤ puts µ ≤ ν if and only if there exists subdivisions s µ and s ν such that s µ is obviously below s ν (see Definition A.1). By Theorem 6.7, it suffices to show that L Prob is depth-0 and depth-1 separating. Depth-separation is immediate: L Prob has the truth object Ω = [0, 1] and a unique truth truth constant ⊤ which we interpret as ⊤ = 1 ∈ [0, 1]. We will now see that L Prob is also depth-1 separating hence also expressive, as expected. The following fact about estimating subdistributions is immediate from the description of the ordering of subdistributions given in Section A: Lemma A.8. Let µ and ν be subdistributions of the form µ = i j p ij · x ij and ν = i j q ij · x ij (with ranges of indices left implicit) such that j p ij · x ij ≤ j q ij · x ij for all i. Then µ ≤ ν.
Proof. By the results of Section A, the subdistributions j p ij ·x ij and j q ij ·x ij have subdivisions d i and d ′ i , respectively, such that d i ⊑ d ′ i for each i. We can combine these into subdistributions d ′ and d of µ and ν, respectively, such that d ⊑ d ′ , showing µ ≤ ν.
Given a canonical M 1 -algebra A : S(A × A 0 ) → A 1 and a jointly orderreflecting family A of positive convex module morphisms A 0 → [0, 1] closed under subconvex algebra morphisms, we will show that the family Λ(A) = { a (f ) : A 1 → [0, 1] | a ∈ A, f ∈ A} is jointly order-reflecting.
First, note that the map S(A × A 0 ) → A 1 is a surjection since A is canonical (hence also a coequalizer). Hence every element of A 1 is represented by a subdistribution A × A 0 which we cast as a subconvex combination of elements of the shape a(x) where (a, x) ∈ A × A 0 . Now, given subdistributions µ, ν ∈ S(A × A 0 ) such that a (f )(µ) ≤ a (f )(ν) for all a ∈ A and all f ∈ A, we will show that µ ≤ ν. Unwinding our assumption, we have that the inequality x∈A0 µ(a, x) · f (x) ≤ x∈A0 ν(a, x) · f (x) ( * ) holds for all f ∈ A and all a ∈ A. In particular, we have Since A is jointly order-reflecting, it follows that x∈A0 µ(a, x) · x ≤ x∈A0 ν(a, x) · x for all a ∈ A. By applying the monotone operation a.(−) to both sides of this inequality and using that actions distribute over subconvex combinations we obtain that x∈A0 µ(a, x) · a(x) ≤ x∈A0 ν(a, x) · a(x) for all a ∈ A, an inequality that holds in S(A × A 0 ) = M 1 A 0 , having been derived in the theory. Hence, by Lemma A.8, we have that µ = a∈A x∈A0 µ(a, x) · a(x) ≤ a∈A x∈A0 ν(a, x) · a(x) = ν, as desired.