{'fraction_non_alphanumeric': 0.0534625287979401, 'fraction_numerical': 0.006928445588833175, 'mean_word_length': 4.160678380977358, 'pattern_counts': {'":': 0, '<': 3, '<?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': 32, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Structural operational semantics for non-deterministic processes with quantitative aspects

General frameworks have been recently proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions), aiming to provide general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function GSOS (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and GSOS formats (e.g. GSOS, Weighted GSOS, Segala-GSOS, among others). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric on the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.


Introduction
Process calculi and labelled transition systems have proved very successful for modelling and analysing concurrent, non-deterministic systems. This success has led to many extensions dealing with quantitative aspects, by adding further informations to the transition relation like probability rates or stochastic rates; see [5,6,15,16,22,30] among others. These calculi are very effective in modeling and analysing quantitative aspects, like performance analysis of computer networks, model checking of time-critical systems, simulation of biological systems, probabilistic analysis of security and safety properties, etc.
Each of these calculi is tailored to a specific quantitative aspect and for each of them we have to develop a quite complex theory almost from scratch. This is a daunting and error-prone task, as it embraces the definition of syntax, semantics, transition rules, various behavioural equivalences, logics, proof systems; the proof of important properties like congruence of behavioural equivalences; the development of algorithms and tools for simulations, model checking, etc. This situation would naturally benefit from general frameworks for LTS with quantitative aspects, i.e., mathematical meta-models offering general methodologies, results, and tools, which can be uniformly instantiated to a wide range of specific calculi and models. In recent years, some of these theories have been proposed; we mention Segala systems [31], Functional Transition Systems (FuTS) [24], weighted labelled transition systems (WLTSs) [13,22,32], and Uniform Labelled Transition Systems (ULTraS), introduced by Bernardo, De Nicola and Loreti specifically as "a uniform setting for modelling non-deterministic, probabilistic, stochastic or mixed processes and their behavioural equivalences" [5].
A common feature of most of these meta-models is that their labelled transition relations do not yield simple states (e.g., processes), but some mathematical object representing quantitative informations about "how" each state can be reached. 1 In particular, transitions in ULTraS systems have the form P a ρ where ρ is a state reachability weight function, i.e., a function assigning a weight to each possible state. By suitably choosing the set of weights, and how these functions can be combined, we can recover ordinary non-deterministic LTSs, probabilistic transition systems, stochastic transition systems, etc. As convincingly argued in [5], the use of weight functions in place of plain processes simplifies the combination of non-determinism with quantitative aspects, like in the case of EMPA or PEPA. Moreover, it paves the way for general definitions and results, an important example being the notion of M-bisimulation [5].
Albeit quite effective, these meta-models are at their dawn, with many results and techniques still to be developed. An important example of these missing notions is a specification format, like the well-known GSOS format for non-deterministic labelled transition systems. These formats are very useful in practice, because they can be used for ensuring important properties of the system; in particular, the bisimulations induced by systems in these formats is guaranteed to be a congruence (which is crucial for compositional reasoning). From a more foundational point of view, these frameworks would benefit from a categorical characterization in the theory of coalgebras and bialgebras: this would allow a cross-fertilizing exchange of definitions, notions and techniques with similar contexts and theories.
In this paper, we provide two main contributions in this respect. First, we present a GSOS-style format, called Weight Function GSOS (WF-GSOS), for the specifications of non-deterministic systems with quantitative aspects. The judgement derived by rules in this style is of the form P a ψ, where P is a process and ψ is a weight function term. These terms describe weight functions, by means of an interpretation. A specification given in this format defines a ULTraS (although we could work also in other frameworks, such as FuTS). By choosing the set of weights, the language of weight function terms and their interpretation, we can readily capture many quantitative notions (probabilistic, stochastic, etc.), and different kinds of non-deterministic interactions, covering models like PEPA, TIPP, PCSP, EMPA, among others. Moreover, the WF-GSOS format supports a general definition of (strong) bisimulation, which can be readily instantiated to the various specific systems.
The second contribution is more fundamental. We provide a general categorical presentation of these non-deterministic systems with quantitative aspects. Namely, we prove that ULTraS systems are in one-to-one correspondence with coalgebras of a precise class of functors, parametric on the underlying weight structure. Using this characterization we define the abstract notion of WF-GSOS distributive law (i.e. a natural transformation of a specific shape) for these functors. We show that each WF-GSOS specification yields such a distributive law (i.e., the format is sound); taking advantage of Turi-Plotkin's bialgebraic framework, this implies that the bisimulation induced by a WF-GSOS is always a congruence, thus allowing for compositional reasoning in quantitative settings. Additionally, we extend the results we presented in [26] proving that the WF-GSOS format is also complete: every abstract WF-GSOS distributive law for ULTraSs can be described by means of some WF-GSOS specification.
Previous works on this line are Klin's Weighted GSOS, a rule format for WLTS [22], and Bartel's Segala-GSOS, a rule format for Segala systems [4, §5.3]. Both WLTSs and Segala systems are subsumed by ULTraSs (in fact, WLTSs correspond to "deterministic" ULTraSs, where a process is associated to exactly one weight function for each label), and as we will show, WF-GSOS subsumes both WGSOS and Segala-GSOS formats. On a different direction, in [12] De Nicola et al. provide a "meta-calculus" for describing stochastic systems and their semantics as FuTS, showing that in several cases behavioural equivalences are congruences. This interesting approach is complementary to ours, since it provides some "syntactic-semantic basic blocks" to be assembled, instead of a general rule format.
The rest of the paper is structured as follows. In Section 2 we recall Uniform Labelled Transition Systems, and their bisimulation. In Section 3 we introduce the Weight Function GSOS specification format for the syntactic presentation of ULTraSs. In Section 4 we provide some application examples, such as a WF-GSOS specification for PEPA and the translations of Segala-GSOS and WGSOS specifications in the WF-GSOS format. The categorical presentation of UL-TraS and WF-GSOS, with the results that the format is sound and complete and bisimilarity is a congruence, are in Section 5. Final remarks and directions for future work are in Section 6.

Uniform Labelled Transition Systems and their bisimulation
In this Section we recall and elaborate the definition of ULTraSs, and define the corresponding notion of (coalgebraically derived) bisimulation; finally we compare it with the notion of Mbisimulation presented in [5]. Additional examples are provided in the Appendix. Although we focus on the ULTraS framework, the results and methodologies described in this paper can be ported to similar formats (like FuTS [24]), and more generally to a wide range of systems combining computational aspects in different ways.

Uniform Labelled Transition Systems
ULTraS are (non-deterministic) labelled transition systems whose transitions lead to state reachability weight functions, i.e. functions representing quantitative informations about "how" each state can be reached. Examples of weight functions include probability distributions, resource consumption levels, or stochastic rates. Under this light, ULTraS can be thought as a generalization of Segala systems [31], which stratify non-determinism over probabilism. Following the parallel with Segala systems, ULTraS transitions can be pictured as being composed by two steps: x a ρ w y where the first is a labelled non-deterministic (sub)transition and the second is a weighted one; from this perspective the weight function plays the rôle of the "hidden intermediate state". Akin to Weighted Labelled Transition Systems (WLTS) [13,22,32], weights are drawn from a fixed set endowed with a commutative monoid structure, where the unit is meant to be assigned to disabled transitions (i.e. those yielding unreachable states) and the monoidal addition is used to compositionally weight sets of transitions given by non-determinism.
Definition 1 (W-ULTraS). Given a commutative monoid W = (W, +, 0), a (W-weighted) Uniform Labelled Transition System is a triple (X, A, ) where: • X is a set of states (processes); • A is a set of labels (actions); denotes the set of weight functions from X to W.
Monoidal addition does not play any rôle in the above definition 2 but it is crucial to define the notion of bisimulation by uniformly providing a compositional way to weight sets of outgoing transitions (e.g. stochastic or probabilistic bisimulations). Since total weights are defined by summation, some guarantees on the cardinality of these sets are needed: Definition 2 (Image boundedness). Let W = (W, +, 0) be a monoid. For a function ρ : X → W the set {x | ρ(x) = 0} is called support of ρ (written ⌊ρ⌋). Let κ, κ ′ be two ordinals; a function ρ : X → W is κ-supported iff ⌊ρ⌋ < κ. A W-ULTraS (X, A, ) is image (κ, κ ′ )-bounded iff for any state x ∈ X and label a ∈ A the set {ρ | x a ρ} has cardinality less than κ and contains only κ ′ -supported functions. (We shall drop κ ′ when it is equal to κ.) The notion of image boundedness guarantees that the branching transitions do not exceed the expressive power of summation of the underlying monoid in the sense that, if sum is defined for any family of cardinality lesser than κ, then for any state in a κ-bounded system the total weights for sets of outgoing transitions are always defined. Henceforth, for the sake of simplicity, we will restrict ourselves to image-finite systems (i.e. ω-bounded), but the development can be generalized throughout.
Definition 3. Let W = (W, +, 0) be a commutative monoid. For any set X let F W X be the set of finitely supported weight functions over X, i.e., F W X {ρ : X → W | |⌊ρ⌋| < ω}. For ρ ∈ F W X and Y ⊆ X let us define ρ(Y ) x∈Y ∪⌊ρ⌋ ρ(x). Finally the total weight of ρ is ρ ρ(X).

Bisimulation
We present now the definition of bisimulation for ULTraS. As we will see in Section 5, this arises directly from their coalgebraic characterization of ULTraS. Let R ⊆ X × Y be a relation between two sets X, Y . The subset closure of R is the smallest A relation R between X and Y is a bisimulation if, and only if, for each pair of states x ∈ X and y ∈ Y , (x, y) ∈ R implies that for each label a ∈ A the following hold: .
Processes x and y are said to be bisimilar if there exists a bisimulation relation R s.t. (x, y) ∈ R.
As ULTraSs can be seen as stacking non-determinism over other computational behaviour, Definition 4 stratifies bisimulation for non-deterministic labelled transition system over bisimulation for systems expressible as labelled transition systems weighted over commutative monoids. In fact, two processes x and y are related by some bisimulation if, and only if, whether one reaches a weight function via a non-deterministic labelled transition, the other can reach another function via a transition with the same label, where the two functions are equivalent in the sense that they assign the same total weight to the classes of states in the relation. For instance, in the case of weights being probabilities, functions are considered equivalent only when they agree on the probabilities assigned to each class of states which is precisely the intuition behind probabilistic bisimulation [23]. More examples will be discussed below or in the Appendix.
Constrained ULTraS Sometimes, the ULTraSs induced by a given monoid are too many, and we have to restrict to a subclass. For instance, fully-stochastic systems such as (labelled) CTMCs are a strict subclass of ULTraSs weighted over the monoid of non-negative real numbers (R + 0 , +, 0), where weights express rates of exponentially distributed continuous time transitions. In the case of fully-stochastic systems, for each label, each state is associated with precisely one weight function. This kind of "deterministic" ULTraSs are called functional in [5], because the transition relation is functional, and correspond precisely to WLTSs [13,22,32]. These are a well-known family of systems (especially their automata counterpart) and have an established coalgebraic understanding as long as a (coalgebraically derived) notion of weighted bisimulation which are shown to subsume several known kinds of systems such as non-deterministic, (fully) stochastic, generative and reactive probabilistic [22]. Moreover, Definition 4 coincides with weighted bisimulation on functional ULTraSs/WLTSs over the same monoid [22,Def. 4]; hence Definition 4 covers every system expressible in the framework of WLTS. (cf. Appendix A). Another constraint arises in the case of probabilistic systems, i.e., weight functions are probability distribution. Since addition is not a closed operation in the unit interval [0, 1], there is no monoid W such that every weight function on it is also a probability distributions. We could relax Definition 1 to allow commutative partial monoids 3 such as the weight structure of probabilities ([0, 1], +, 0). Unfortunately, not every weight function on [0, 1] is a probability distribution. In fact, probabilistic systems (among others) can be recovered as ULTraSs over the (R + 0 , +, 0) (i.e. the free completion of ([0, 1], +, 0)) and subject to suitable constraints. For instance, Segala systems [31] are precisely the strict subclass of R + 0 -ULTraS such that every weight function ρ in their transition relation is a probability distribution i.e. ρ = 1. Moreover, bisimulation is preserved by constraints. For instance, bisimulations on the above class of (constrained) ULTraS are Segala's (strong) bisimulations (cf. [31,Def. 13]), and vice versa. A similar result holds for reactive and generative (or fully) probabilistic systems and their bisimulations. In fact, these are functional ULTraS with weight functions in F R 0 + and subject to constraints ∀x ∈ X : a∈A,y∈X ρ(x, a, y)∈{0, 1} and ∀x ∈ X, a ∈ A : y∈X ρ(x, a, y)∈{0, 1} respectively. • for all x ∈ X, a ∈ A and C ∈ PX, M(x, a, C) = ⊥ whenever ρ(C) = 0 for every x a ρ or there is no ρ at all;
Definition 6 (M-bisimulation [5]). Let M be an M -function for (X, A, ). A relation R ⊆ X × X is a M-bisimulation for iff for each pair (x, y) ∈ R, label a ∈ A, and class C ∈ (X/R), the following holds: M(x, a, C) = M(y, a, C).
In some sense, the notion of M-bisimulation is more general than Definition 4 since (sets of) transitions are not necessarily weighted in the same structures. For instance, stochastic rates can be considered up-to a suitable tolerance in order to account for experimental measurement errors in the model.
A further distinction between bisimulation and M-bisimulation arises from the fact that UL-TraSs come with two distinct way of terminating. A state can be seen as "terminated" either when its outgoing transitions are always the constantly zero function, or when it has no transitions at all. In the first case, the state has still associated an outcome, saying that no further state is reachable; we call these states terminal. In the second case, the LTS does not even tell us that the state cannot reach any further state; in fact, there is no "meaning" associated to the state.
In this case, we say that the state is stuck. 5 The bisimulation given in Definition 4 keeps these two terminations as different (i.e., they are not bisimilar), whereas M-bisimulation does not make this distinction (cf. [5,Def. 3.2] or, for a concrete example based on Segala systems, [5,Def. 7.2]).
Finally, the two notions differ on the quantification over equivalence classes: in the case of Definition 4 quantification depends on the non-deterministic step whereas in the case of Mbisimulation it does not.
Under some mild assumptions, the two notions agree. In particular, let us restrict to systems with just one of the two terminations for each action a-i.e. if for some x, {ρ | x a ρ} = ∅ then for all y, λz.0 / ∈ {ρ | y a ρ}, and, symmetrically, if for some x, λz.0 ∈ {ρ | x a ρ} then for all y, {ρ | y a ρ} = ∅. Then, the bisimulation given in Definition 4 corresponds to a M-bisimulation for a suitable choice of M.
Proposition 3. Let (X, A, ) be a W-ULTraS with at most one kind of termination, for each label. Every bisimulation R is also an M-bisimulation for Proof. See Appendix C, page 21.

WF-GSOS: A complete GSOS format for ULTraSs
In this section we introduce the Weight Function GSOS specification format for the syntactic presentation of ULTraSs. As it will be proven in Section 5.2, bisimilarity for systems given in this format is guaranteed to be a congruence with respect to the signature used for representing processes.
The format is parametric in the weight monoid W and, as usual, in the process signature Σ defining the syntax of system processes. In contrast with "classic" GSOS formats [20], targets of rules are not processes but terms whose syntax is given by a different signature, called the weight signature. This syntax can be thought of as an "intermediate language" for representing weight functions along the line of viewing ULTraSs as stratified (or staged) systems. An early example of this approach can be found in [2], where targets are terms representing measures over the continuous state space. Earlier steps in this direction can be found e.g. in Bartels [5,9] where targets are described by meta-expressions.
Definition 7 (WF-GSOS Rule). Let W be a commutative monoid and A a set of labels. Let Σ and Θ be the process signature and the weight signature respectively. A WF-GSOS rule over them is an expression of the form: where: • f is an n-ary symbol from Σ; is a set of clubs of W, i.e. subsets of W being monoid ideals whose complements are sub-monoids of W; • a, b, c ∈ A are labels and A i ∩ B i = ∅ for 1 ≤ i ≤ n; • ψ is a weight term for the signature Θ such that var(ψ) ⊆ X ∪ Y ∪ Φ.
A rule like above is triggered by a tuple C 1 , . . . , C n of enabled labels and by a tuple v 1 , . . . , v p of weights if, and only if, Intuitively, the four families of premises can be grouped in two kinds: the first two families correspond to the non-deterministic (and labelled) behaviour, whereas the other two correspond to the weighting behaviour of quantitative aspects. The former are precisely the premises of GSOS rules for LTSs (up-to targets being functions), and describe the possibility to perform some labelled transitions. The latter are inspired by Bartels' Segala-GSOS [4, §5.3] and Klin's WGSOS [22] formats; a premise like ϕ = w constrains the variable ϕ to those functions whose total weight is exactly the constant w; a premise like φ C ∋ y binds the process variable y to those elements being assigned a weight in C. Clubs are substructures of commutative monoids that are "isolated" w.r.t. the monoidal operation in the sense that: • are commutative monoid ideals, i.e. subsets C with a module structure: img(+ W×C ) ⊆ C; This isolation property means that clubs are not affected by variables substitutions (in fact, clubs form the finest topology on a commutative monoid enforcing this property). Likewise Segala-GSOS (but not WGSOS), there are no variables denoting the weight of each y k since this information can be readily extracted from ϕ a k i k j k , e.g. by some operator from Θ that "evaluates" ϕ a k i k j k on y k . Targets of transitions defined by these rules are terms generated from the signature Θ. In order to characterize transition relations for ULTraSs, we need to evaluate these terms to weight functions. This is obtained by adding an interpretation for weight terms, besides a set of rules in the above format.
Before defining interpretations and specifications, we need to introduce some notation. For a signature S and a set X of variable symbols, let T S X denote the set of terms freely generated by S over the variables X (in the following, S will be either Σ or Θ). A substitution for symbols in X is any function σ : X → Y ; its action extends to terms defining the function T S (σ) : T S X → T S Y (i.e. simultaneous substitution). When confusion seems unlikely we use the more evocative t[σ] instead of T S (σ)(t).
A variable substitution σ : X → Y induces also a function F W (σ) : F W X → F W Y , mapping (finitely supported) weight functions over X to (finitely supported) weight functions over Y , as follows: Consistently, we denote the action of σ on ρ by ρ[σ].
Definition 8 (Interpretation). Let W be a commutative monoid, Σ and Θ be the process and the weight signature respectively. A weight term interpretation for them is a family of functions indexed over sets of variable symbols, and respecting substitutions, i.e.: Differently from [26] interpretations allow one term to represent finitely many weight functions. This generalization offers more freedom in the use of the format by reducing the constrains on what can be encoded in weight function terms and simplifies the proof for completeness.
We are ready to introduce the WF-GSOS specification format. Basically, this is a set of WF-GSOS rules, subject to some finiteness conditions to ensure image-finiteness, together with an interpretation.
Definition 9 (WF-GSOS specification). Let W be a commutative monoid, A the set of labels, Σ and Θ the process and the weight signature respectively. An image-finite WF-GSOS specification over W, A, Σ and Θ is a pair R, {|-| } where {|-| } is a weight term interpretation and R is a set of rules compliant with Definition 7 and such that only finitely many rules share the same operator in the source (f), the same label in the conclusion (c), and the same trigger A 1 , . . . , A n , w 1 , . . . , w p .
Every WF-GSOS specification induces an ULTraS over ground process terms.
is defined as the smallest subset of T Σ ∅ × A × F W T Σ ∅ being closed under the following condition.
Let p = f(p 1 , . . . , p n ) ∈ T Σ ∅. Since the ground Σ-terms p i are structurally smaller than p assume (by structural recursion) that the set {ρ | p i a ρ} -and hence the trigger A = A 1 , . . . , A n , w = w 1 , . . . , w q -is determined for every i ∈ {1, . . . , n} and a ∈ A. For any rule R ∈ R whose conclusion is in the form f(x 1 , . . . , x n ) c ψ and triggered by A and w let X, Y , Φ be the set of process and weight function variables involved in R as per Definition 7. Then, for any substitution σ : X ∪ Y → T Σ ∅ and map θ : Φ → F W T Σ ∅ such that: The above definition is well-given since it is based on structural recursion over ground Σterms (i.e. the process p in each triple (p, a, ρ)); in particular, terms have finite depth and only structurally smaller terms are used by the recursion (i.e. the assumption of p i a ρ being defined for each p i in p = f(p 1 , . . . , p n )). Moreover, for any trigger, operator, and conclusion label only finitely many rules have to be considered.
Finally we can state the main adequacy result for the proposed format.
Theorem 4 (Congruence). The bisimulation on the ULTraS induced by a WF-GSOS specification is a congruence with respect to the process signature.
The proof is postponed to Section 5.2, where we will take advantage of the bialgebraic framework.
Remark 1 (Expressing interpretations). Weight term interpretation can defined in many ways, such as structural recursion or λ-iteration [2]. For instance, every substitutions-respecting family of maps: uniquely extends to an interpretation by structural recursion on Θ-terms where h X and b X define the inductive and base cases respectively. These maps can be easily given by means of a set of equations, as in [26, §4.1].

Examples and applications of WF-GSOS specifications
In this Section we provide some examples of applications of the WF-GSOS format. First, we show how a process calculus can be given a WF-GSOS specification; in particular, we consider PEPA, a well known process algebra with quantitative features. Then we show that Klin's Weighted GSOS format for weighted systems [22] and Bartels' Segala-GSOS format for Segala systems [4] are subsumed by our WF-GSOS format; this corresponds to the fact that ULTraSs subsume both weighted and Segala systems.

WF-GSOS for PEPA
In PEPA [16,17], processes are terms over the grammar: where a ranges over a fixed set of labels A, L over subsets of A and r over R + . The semantics of process terms is usually defined by the inference rules in Figure 1 where a ∈ A, r, r 1 , r 2 , R ∈ R + (passive rates are omitted for simplicity) and R depends only on r 1 , r 2 and the intended meaning of synchronisation. For instance, in applications to performance evaluation [16], rates model times and R is defined by the minimal rate law : where r a denotes the apparent rate of a. In systems biology [8], rates model molecules concentrations and R is defined by the multiplicative law : R = r 1 · r 2 . PEPA can be characterized by a specification in the WF-GSOS format where the process signature Σ is the same as (2) and weights are drawn from the monoid of positive real numbers under addition extended with the +∞ element (only for technical reasons connected with the {|-| } and process variables-differently from other stochastic process algebras like EMPA [6], PEPA does not allow instantaneous actions, i.e. with rate +∞). The intermediate language of weight terms is expressed by the grammar: where r ∈ R + 0 , L ⊆ A, ξ range over weight functions, and P over processes. Note that the grammar is untyped since it describes the terms freely generated by the signature Θ = {⊥: 0, ♦ r : 1, ⊕ : 2, L : 2}, over weight function variables and processes. Intuitively ⊥ is the constantly 0 function, ♦ r reshapes its argument to have total weight r, ⊕ is the point-wise sum and L parallel composition e.g. by (3). The formal meaning of these operators is given below by the definition (by structural recursion on Θ-terms) of the interpretationwhich is introduced alongside WF-GSOS rules for presentation convenience. Each operator is interpreted as a singleton (PEPA describes functional ULTraSs) and hence we will describeas if a weight function is returned.
For each action a ∈ A and rate r ∈ R + , a process (a, r).P presents exactly one a-labelled transition ending in the weight function assigning r to the (sub)process denoted by the variable P and 0 to everything else. Hence, the action axiom is expressed as follows: where ♦ r reshapes 6 P X to equally distribute the weight r over its support; in particular, since process variables will be interpreted as "Dirac-like" functions ♦ r (P ) corresponds to the weight function assigning r to Σ-term denoted by P . 6 Since the interpretationis being defined by structural recursion and has to cover all the language freely generated from Θ, we can not use the (slightly more intuitive) "Dirac" operator δr(P ) where P is restricted to be a process variable instead of a Θ-term. Likewise, indexing δ r,P also over processes would break substitution independence i.e. naturality.
Conversely to the action axiom, (a, r).P can not perform any action but a: This rule is required to obtain a functional ULTraS and is implicit in Figure 1 where disabled transitions are assumed with rate 0 as in any specification in the Stochastic GSOS or Weighted GSOS formats. Without this rule, transitions would have been disabled in the non-deterministic layer i.e. (a, r).P b . Stochastic choice is resolved by the stochastic race, hence the rate of each competing transition is added point-wise as in Figure 1 (and in the SGSOS and WGSOS formats). This passage belongs to the stochastic layer of the behaviour (hence to the interpretation, in our setting) whereas the selection of which weight functions to combine is in the non-deterministic behaviour represented by the rules and, in particular, to the labelling. Therefore, the choice rules become: Likewise, process cooperation depends on the labels to select the weight function to be combined. This is done in the next two rules: one when the two processes cooperate, and the other when one process does not interact on the channel: The combination step depends on the specific e.g. in the case of (3): Each process is interpreted as a weight function over process terms. This is achieved by a Dirac-like function assigning +∞ to the Σ-term composed by the aforementioned variable: P X (t) = +∞ if P = t, 0 otherwise. The infinite rate characterizes instantaneous actions as if all the mass is concentrated in the variable; e.g., in interactions based on the minimal rate law, processes are not consumed. For the same reason, if we were dealing with concentration rates and the multiplicative law, we would assign 1 to P .
The remaining rules for hiding are straightforward: This completes the definition ofby structural recursion and hence the WF-GSOS specification of PEPA. It is easy to check that the induced ULTraS is functional and correspond to the stochastic system of PEPA processes; that bisimulations on it are stochastic bisimulations (and vice versa) and that bisimilarity is a congruence with respect to the process signature.
Definition 11 ([4, §5.3]). A GSOS rule for Segala systems is a rule of the form where: • f is an n-ary symbol from Σ; i } are pairwise distinct process and probability distribution variables respectively; • a, b, c ∈ A are labels and A i ∩ B i = ∅ for any i ∈ {1, . . . , n}; • t 1 , . . . , t m are target terms on variables X, Y and V ; the latter are associated with colours from a finite palette to indicate different instances; • {w i ∈ (0, 1] | 1 ≤ i ≤ m} are weights associated to the target terms and s.t. 1≤i≤m w i = 1.
A rule like above is triggered by a tuple C 1 , . . . , C n of enabled labels if, and only if, A i ⊆ C i and B i ∩ C i = ∅ for each i ∈ {1, . . . , n}. A GSOS specification for Segala systems is a set of rules in the above format containing finitely many rules for any source symbol f, conclusion label c and trigger C.
Segala-GSOS specifications can be easily turned into WF-GSOS ones. The first two families of premises are translated straightforwardly to the corresponding ones in our format; the third can be turned into those of the form ⌊ϕ⌋ ∋ y. Targets of transitions describe finite probability distributions and are evaluated to actual probability distributions by a fixed interpretation of a form similar to Definition 8. Some care is needed to handle copies of probability variables. In practice, duplicated variables are expressed by adding "colouring" operators to Θ; their number is finite and depends only on the set of rules since multiplicities are fixed and finite for rules in the above format. LetṼ be the set of "coloured" variables from V where the colouring is used to distinguish duplicated variables (cf. [4, §5.3]). Given a substitution ν fromṼ to (finite) probability distributions over T Σ (X + Y ), each t i is interpreted as the probability distribution: and each target term w 1 · t 1 + · · · + w m · t m is interpreted as the convex combination oft 1 , . . . ,t m .

Weighted GSOS
In t where: • f is an n-ary symbol from Σ; process and weight variables; • {w ai ∈ W | 1 ≤ i ≤ n, a ∈ A i } are weight constants such that w i k = 0 for 1 ≤ k ≤ m; • β : W m → W is a multiadditive function on W; • a, b, c ∈ A are labels and A i ⊆ A for 1 ≤ i ≤ n; • t is a Σ-term such that Y ⊆ var(t) ⊆ X ∪ Y ; A rule is triggered by a n-tuple C of enabled labels s.t. A i ⊆ C i and by a family of weights {v ai | 1 ≤ i ≤ n, a ∈ A i } s.t. w ai = v ai . A W-GSOS specification is a set of rules in the above format such that there are only finitely many rules for the same source symbol, conclusion label and trigger.
Each rule describes the weight of t in terms of weights assigned to each y k (i.e. u k ) occurring in it; if two rules share the same symbol, label, trigger and target then their contribute for t is added.
To turn a W-GSOS specification into WF-GSOS ones, the first step is to make weight function explicit, by means of premises like x i a ϕ a i (since WLTS are functional ULTraS, i.e. m a i = 1). Then, each premise x i a w ai is translated into ϕ a i = w ai . If W is zerosumfree (i.e., whenever a + b = 0 then a = b = 0) then W \ {0} is a club and the translation of a W-GSOS into a WF-GSOS is straightforward. More generally, it suffices to combine rules sharing the same source, label and trigger into a single WF-GSOS rule with the same source, label and trigger. Its target is a suitable weight term containing the functions β and targets t of the original rules; every occurrence of variables y k and u k is replaced with the corresponding function variable (i.e. ϕ b k i k ). In order to deal with multiple copies of the same weight variable, we wrap each occurrence in a different "colouring" operator, like in the case of Segala-GSOS.

A coalgebraic presentation of ULTraS and WF-GSOS
The main aim of this Section is to prove some important results about WF-GSOS specifications. We first provide a characterization of ULTraSs as coalgebras for a specific behavioural functor (Section 5.1), and their bisimulations as cocongruences. Then, leveraging this characterization in Section 5.2 we apply Turi and Plotkin bialgebraic theory [33], which allows us to define the categorical notion of WF-GSOS distributive law ; these laws describe the interplay between syntax and behaviour in any GSOS presentation of ULTraS. We will prove that every WF-GSOS specification yields a WF-GSOS distributive law, i.e., the format is sound. As a consequence, we obtain that the bisimilarities induced by these specifications are always congruence relations. Finally, in Section 5.3 we prove that WF-GSOS specification are also complete: every abstract WF-GSOS distributive law can be described by means of a WF-GSOS specification.

ULTraSs as coalgebras
Since ULTraSs alternate non-deterministic steps with quantitative steps, the corresponding behavioural functor can be obtained by composing the usual functor (P f ) A : Set → Set of nondeterministic labelled transition systems with the functors capturing the quantitative computational aspects.
Let us recall that for every set X we denoted by F W X = {ϕ : X → W | |⌊ϕ⌋| < ω} the set of finitely supported weight functions over X. This extends to an endofunctor F W : Set → Set whose action on morphisms is given by, for f : λy. x∈f −1 (y) ϕ(x). It is easy to check that identities and compositions are preserved.
Proposition 5. For any W and any A, coalgebras for (P f F W ) A are in one-to-one correspondence with A-labelled image-finite W-ULTraSs.
Proof. Any image-finite W-ULTraS (X, A, ) determines a coalgebra (X, h) where, for any x ∈ X and a ∈ A: h(x)(a) {ρ | x a ρ}. Image-finiteness guarantees that these sets are finite and that their elements are finitely supported weight functions from X to the carrier of W. Then, it is easy to check that the correspondence is bijective.
A similar result holds also for the bisimulation given in Definition 4. Categorically, a relation between X and Y is a (jointly monic) span X ← R → Y . In our case, this span has to be subject to some conditions, as shown next.
Proof. See Appendix C, page 21.
Intuitively, the system (Y, g) "subsumes" both (X 1 , h 1 ) and (X 2 , h 2 ) via f 1 , f 2 ; then, R relates the states which are mapped to the same behaviour in Y (( ). This kind of behavioural equivalence is also called kernel bisimulation (or cocongruence).
Coalgebraic bisimulation In Concurrency theory also Aczel-Medler's coalgebraic bisimulation [1] is widely used -arguably because its formulation corresponds precisely to the (strong) bisimulations of most calculi (CCS, π-calculus, etc.). In fact, it is known that kernel bisimulations and coalgebraic bisimulations coincide if the behavioural functor is weak pullback preserving (wpp). This is the case for many behavioural functors, but not for F W in general [22]. Actually, the fact that F W (and (P f F W ) A ) preserves weak pullbacks depends on the underlying monoid only:
Proof. (P f ) A is weak wpp, and under the proposition hypothesis also F W is wpp, by a straightforward extension of [28,Th. 3.6] as noted in [19,Prop. 4]. Therefore, (P f F W ) A is wpp, hence every behavioural equivalence is a coalgebraic bisimulation on (P f F W ) A -coalgebras. We conclude by Proposition 5.
This condition, called row-column property, can be easily verified and in fact holds for most monoids of interest. A simple counter example is ({0, a, b, 1}, +, 0) where x + y 1 whenever = a, a and v = b, b ).

WF-GSOS specifications are WF-GSOS distributive laws
In this subsection we put the WF-GSOS format within the bialgebraic framework [33]. As a consequence, we obtain that the bisimilarity induced by the ULTraS defined by this specification is a congruence. We refer the interested reader to [20] for an introduction to the general theory of abstract GSOS.
In particular, we prove that every WF-GSOS specification represents a distributive law of the signature over the ULTRaS behavioural functor, i.e., a natural transformation of the form where A is the set of labels, W is the commutative monoid of weights, Σ = f∈Σ Id ar(f) is the syntactic endofunctor induced by the process signature Σ, and T Σ is the free monad for Σ. We will call natural transformations of this type WF-GSOS distributive laws. Before stating the soundness theorem, we note that every natural transformation λ as above induces a (P f F W ) A -coalgebra structure over ground Σ-terms. Namely, this is the only function h λ : T Σ ∅ → (P f F W (T Σ ∅)) A such that: We can now provide the soundness result for WF-GSOS specifications with respect to WF-GSOS distributive laws, and between systems and coalgebras they induce over ground Σ-terms. (4) such that h λ and the ULTraS induced by R, {|-| } coincide.

Theorem 8 (Soundness). A specification R, {|-| } yields a natural transformation λ as in
Proof. For any set X, define the function λ X as the composite: where R X is defined as follows: for all ) if, and only if, there exists in R a (possibly renamed) rule such that m a i = 0 iff a ∈ A i and there exists a substitution σ such that ψ ′ = σ[ψ], σx i = x ′ i , σy k = y ′ k , σϕ a ij = φ a ij , φ a k i k j k = w k and φ a k i k j k (σy k ) ∈ C k . Then, naturality can be proved separately for the two components: the former can be tackled as in [33, Th. 1.1] and the latter readily follows from Definition 8.
Correspondence of (T Σ ∅, h λ ) with the induced ULTraS follows by noting that the latter is given by structural recursion on Σ-terms by applying precisely the distributive law λ as given above (cf. (5) and Definition 10). Now, by general results from the bialgebraic framework, every behavioural equivalence on the coalgebra induced on ground process terms (T Σ ∅, h λ ) is also a congruence on its carrier T Σ ∅ with respect to the process signature Σ (i.e. w.r.t. their Σ-algebra structure). In order to obtain this result we need the following (simple yet important) property.
Proposition 9. The category of (P f F W ) A -coalgebras has a final object.
Proof. By [3] every finitary Set endofunctor admits a final coalgebra. By definition F W is finitary for every abelian monoid W. The thesis follows from P f ∼ = F 2 and from finitarity being preserved by functor composition.
Corollary 10 (Congruence). Behavioural equivalence on the coalgebra over T Σ ∅ induced by R, {|-| } is a congruence with respect to the process signature Σ.
Proof. The syntactic endofunctor Σ admits an initial algebra and, by Proposition 9, the behavioural endofunctor (P f F W ) A admits a final coalgebra. The same holds for their free monad and cofree copointed functor respectively. The specification R, {|-| } defines, by Theorem 8, a distributive law which uniquely extends to a distributive law distributing the free monad over the cofree copointed functor; then the thesis follows from [33,Cor. 7.3].

WF-GSOS distributive laws are WF-GSOS specifications
In this subsection we give the important result that the WF-GSOS format is also complete with respect to distributive laws of the form (4).
The proof of this Theorem follows the methodology introduced by Bartels for proving adequacy of Bloom's GSOS specification format [4, §3.3.1]. The (rather technical) proof will take the rest of this subsection, so for sake of conciseness we omit to recall some results which can be found in loc. cit..
The thesis follows by proving that, for every λ, there exists an image-finite set of WF-SOS rules R (and suitable interpretations θ and ξ) making the diagram in Figure 2 commute. The lower part of the diagram defines the interpretation {|-| } out of ξ and θ completing the WF-GSOS specification for λ. The middle and right parts of the diagram trivially commute.
The upper part of the diagram commutes because of the following lemma which states that every WF-GSOS distributive law arises from an interpretation and a natural transformation having the same type of those defined by image-finite sets of WF-GSOS rules.
Lemma 12. Let Σ, A and W be a signature, a set of labels and a commutative monoid respectively. Let λ be a WF-GSOS distributive law as in (4). There exist Θ and an interpretation θ factorizing λ i.e. there exists ρ : Proof (sketch). In Set it is easy to encode finitely supported functions as terms. For instance let Θ extend Σ with operators for describing collections and weight assignments (e.g. (-→ w) where w ∈ W \ {0}). Then, we can turn λ into ρ by simply encoding its codomain. Then θ simply evaluates these terms back to weight functions everything else to the ∅.
The left part of the diagram commutes by reducing ρ to simpler, but equivalent, families of natural transformations following Bartels' methodology and eventually deriving a syntactical specification which is then shown to be equivalent to a image-finite set of WF-GSOS rules and an intermediate interpretation ξ. The use of another weight signature Ξ besides Θ gives us an extra degree of freedom and simplifies the proof. In particular, it allows us to encode natural transformations of type F W ⇒ P f F W (yielded by the aforementioned reduction) in ξ and handle them downstream to the interpretation {|-| }. This expressiveness gain is one of the reasons for the introduction of non-determinism in Definition 8.
First, note that, by [4, Lem. A.1.1], ρ as above is equivalent to: which is equivalent to a family of natural transformations indexed by f ∈ Σ and c ∈ A and where N = {1, . . . , ar(f)}. In fact, Σ is a polynomial functor and Id × A ∼ = A · Id is an |A|-fold coproduct. By [4,Lem. A.1.7], each α f,c is equivalent to a natural transformation and, by the natural isomorphism where the added index corresponds to the vector of sets of labels E 1 , . . . , E ar(f) composing the trigger of a WF-GSOS rule. By the natural isomorphism where w : E → P + f W. Since total weight premises associate pairs from E to weights, maps like w can be seen as families of triggering weights. By where the added index ψ ranges over some subset of T Θ (1 + N ) (cf. target terms of WF-GSOS rules). Then, following [4, §3.3.1, Cor. A.2.8] it is easy to check that each δ f,c,E,w,ψ describes a nonempty, finite set of derivation rules of the form of where p, q ∈ N, e j ∈ E, 1 ≤ j ≤ p, 1 ≤ i ≤ q, v j ∈ w(e j ), each z k ∈ {y i | 1 ≤ i ≤ q} for 1 ≤ k ≤ |ψ| * and each ǫ j,vj is a natural transformation: . Natural transformations of this type can be easily encoded in the term ψ by suitable extensions of Θ and therefore each δ f,c,E,w,ψ can be shown to be equivalent to a δ-specification i.e. a non-empty finite set of derivation rules as above except for each z k being a term wrapping φ j,v with the symbol denoting ǫ j,v . These terms are then evaluated by the interpretation ξ δ as expected.
This proof points out the trade-off that has to be made in presence of specifications with interpretation such as WF-GSOS or MGSOS [2]. In fact, clubs were not mentioned in the above reduction of ρ since ǫ were handled by the interpretation ξ. However, the following result shows that clubs (hence, premises like ϕ C ∋ y), characterize natural transformations of type F v W ⇒ P f .

Lemma 13.
For any natural transformation υ : F w W ⇒ P f there exists a club C υ characterizing it: x ∈ υ X (ϕ) ⇐⇒ φ(x) ∈ C υ . Proof (sketch). Intuitively, natural transformations of this type are "selecting a finite subset from each weight function domain" and it is easy to check that elements can be only singled out by their weight. Likewise, finiteness and naturality prevent the selection of anything outside function supports. Then, the problem readily translates into finding the finest topology on the weight monoid that "plays well" with F W i.e. such that monoidal addition, seen as a continuous map from the product topology, preserves opens (i.e. any admissible selection). Clubs form this topology since, by definition, these are the only substructures isolated w.r.t. F W -action. Hence selections made by υ are completely characterized by a single club C υ .
Finally, we have to translate the set of rules we got so far into the WF-GSOS format; we do it by reversing the chain that led us from ρ to δ and δ-specification. By Lemma 13 every δ-specification is equivalent to a γ-specification vj ∈w(ej ), where φ j [ζ j ] is a term build with the Ξ-operator denoting the natural transformation ζ j : F vj W ⇒ P f F W and ξ γ acts as ξ δ on these terms, as the identity on those generated from Θ (distributing the powerset as expected) and maps everything else to ∅. A γ-specification defines a natural transformation as in (9) and every family of γ-specifications characterizing a natural transformation as in (8) is equivalent to a β-specification i.e. a set of derivation rules finite up to vectors of total weights v = v 0 , . . . , v p . Since E ⊆ A × N , every family of βspecifications describing a natural transformation as in (7) is equivalent to a set containing finitely many rules for every E and v. This set corresponds to an α-specification i.e. an image-finite set like the following: Finally, every family of α-specifications equivalent to a natural transformation as ρ corresponds to an image-finite set of WF-GSOS rules and an interpretation. Therefore we conclude that for any ρ there exist R and ξ as in Figure 2.

Conclusions and future work
In this paper we have presented WF-GSOS, a GSOS-style format for specifying non-deterministic systems with quantitative aspects. A WF-GSOS specification is composed by a set of rules for the derivation of judgements of the form P a ψ, where ψ is a term of a specific signature, and an interpretation for these terms as weight functions. We have shown that a specification in this format defines an ULTraS, and it is expressive enough to subsume other more specific formats such as WGSOS and Segala-GSOS. WF-GSOS induces naturally a notion of (strong) bisimulation, which we have compared with M-bisimulation used in ULTraS. We have also provided a general categorical presentation of ULTraSs as coalgebras of a precise class of functors, parametric on the underlying weight structure. This presentation allows us to define categorically the notion of abstract GSOS for ULTraS, i.e., natural transformations of a precise type. We have proved that WF-GSOS specification format is adequate (i.e., sound and complete) with respect to this notion. Taking advantage of Turi-Plotkin's bialgebraic framework, we have proved that the bisimulation induced by a WF-GSOS is always a congruence; hence our specifications can be used for compositional and modular reasoning in quantitative settings (e.g., for ensuring performance properties). Moreover, the format is at least as expressive as every GSOS specification format for systems subsumed by ULTraS.
In [10] Gebler et al. proposed a ntµf ν/ntµxν rule format for describing Segala Systems and such that the induced bisimulation is always a congruence. It would be interesting to investigate the possibility to extend their work to the wider range of behaviours covered by ULTraSs since, in general, GSOS and tree-rule formats have different expressive powers.
Although in this paper we have taken ULTraS systems as a reference, WF-GSOS can be interpreted in other meta-models, such as FuTS [24]. Like ULTraS, FuTS have state-to-function transitions, but admit several distinct domains for weight functions and hence can be read as "composing in parallel" distinct behaviours. The results in this paper readily extend to FuTS since these systems can be seen as coalgebras for functors with a specific shape: (P f W∈W F W ) A for W being the set of admitted weight domains. In this context it is easy to formulate compositionality results also for the framework for stochastic calculi proposed in [12]. A coalgebraic understanding of FuTS is presented in [24] but covers only the deterministic case (i.e. ( W∈W F W ) A ), while ours is non-deterministic.
For sake of simplicity, we have characterized ULTraS systems using the functor F W . However, the results and definition presented here can be further generalized by taking generic behavioural functors in place of F W , thus considering systems that are coalgebras for functors of the form of (P f B) A . This would affect mostly the evaluation {|-| }, while only minor changes to the rule format may be required in order to capture interactions between P f and B (like e.g. the total weight premises). This fact suggests to investigate systems with stratified (or "staged") behaviours via "stratified" specifications. We can develop general results at the abstract level of bialgebraic structural operational semantics, aiming to provide some modularity to the format. This line of research can be seen as complementary to Mosses' Modular SOS [29] and recent developments towards a GSOS equivalent [27] (which still are more "syntax bound" since the behavioural functor is not very changed by these compositions).
The categorical characterization of ULTraS systems paves the way for further interesting lines of research. One is to develop Hennessy-Milner style modal logics for quantitative systems at the generality level of the ULTraS framework. In fact, Klin has shown in [18] that HML and CCS are connected by a (contravariant) adjunction. A promising direction is to follow this connection taking advantage of the bialgebraic presentation of ULTraSs provided in this paper. Another is to explore the implications of the recent developments in the coalgebraic understanding of silent actions [7,14,25] in the context of this work.

A Weighted transition Systems
Weighted labelled transition systems (e.g. [13,22,32]) are LTS whose transition are assigned a weight drawn from a commutative monoid W = (W, 0, +). Henceforth we will write W-LTS for W-Weighted LTS or in general WLTS if no specific monoid is intended.
. Given a commutative monoid W = (W, +, 0), a W-weighted LTS is a triple (X, A, ρ) where: • X is a set of states (processes); • A is a set of labels (actions); • ρ : X × A × X → W is a weight function, mapping each triple of X × A × X to a weight.
(X, A, ρ) is said to be image-finite iff for each x ∈ X and a ∈ A, the set {y ∈ X | ρ(x, a, y) = 0} is finite.
Moreover, Klin defined in [22] a notion for WLTS (based on cocongruences) which uniformly instantiates to known bisimulations for systems expressible in the WLTS framework. . Given a W-LTS (X, A, ρ), a W-bisimulation is an equivalence relation R on X such that for each pair (x, x ′ ) of elements of X, (x, x ′ ) ∈ R implies that for each label a ∈ A and each equivalence class C of R: y∈C ρ(x, a, y) = y∈C ρ(x ′ , a, y).
WLTS are precisely functional ULTraS and, as stated in Proposition 1, every weighted bisimulation for a WLTS is a bisimulation for the corresponding functional ULTraS and vice versa.
Proof of Proposition 1. Trivially, there is a 1-1 correspondence between W-LTS and functional W-ULTraS. Then, Proposition 1 readily follows by observing that, for any given W-LTS/ULTraS (X, A, ), Definition 4 degenerates in Definition 14 because for any x a − → ϕ there is exactly one y a − → ψ.

B Segala Systems
In their general format, Segala systems [31] are state machines (originally introduced as automata) whose transitions can be pictured as being made of two steps belonging to two different behavioural aspects: the first sub-step is non-deterministic and the second one is probabilistic. The following definitions are taken from [31] with minor notational differences and by restricting to finite probability distributions (whereas the original definition is given to discrete at most countable probability spaces) for conciseness and uniformity with the restriction to image-finite systems made in the paper.
Definition 15. A Segala system is a triple (X, A, ) where: • X is a set of states (processes); • A is a set of labels (actions); • ⊆ X × D(A × X) a transition relation between states and discrete probability spaces over pairs of labels and states.
Before stating what is a strong bisimulation for these systems, we need to recal the notion of of R-equivalence between probability distributions ( [31, Def. 13]) which, intuitively, says that two distributions are R-equivalent if they assign the same probability to each class in the equivalence relation R.
Strong bisimulation [31,Def. 14] is defined in terms of simple-labelled steps i.e. transitions of the form of x a P which intuitively means to see labels as inputs ((DX) A ) instead of outputs (D(A × X)).
Definition 17 ([31, Def. 14]). Given a Segala system (X, A, ), a bisimulation is an equivalence relation R on X such that for each pair (x, x ′ ) of elements of X, (x, x ′ ) ∈ R implies that for each label a ∈ A if x a P then x ′ a P ′ such that P ≡ R P ′ and symmetrically for x ′ .
Proof of Proposition 2. Clearly DX ⊆ F R + 0 X and hence Segala systems are constrained UL-TraS. Then, Proposition 2 readily follows by observing that the two notions coincide on the non-deterministic part and that R-equivalence means that the two distributions assign the same probability to each equivalence class of R i.e. the same total weight: P(C) = c∈C P(c) = c∈C P ′ (c) = P ′ (C).

C Omitted proofs
Proof of Proposition 3. The function M is well-given because M(x, a, C) =⊥ whenever x a or, for each x a ρ, ρ(C) = 0, and M(x, a, C 1 ) = M(y, a, C 1 ) and M(x, a, C 2 ) = M(y, a, C 2 ) implies M(x, a, C 1 ∪ C 2 ) = M(y, a, C 1 ∪ C 2 ) by definition of ≡ R .
By Definition 4, whenever x a ϕ then y a ψ s.t. ϕ(C) = ψ(C) for each C ∈ X/R i.e. ϕ ≡ R ψ and the symmetric case for y. Therefore (x, y) ∈ R implies that Φ x,a {[ϕ] ≡R | x a ϕ} and Φ y,a {[ψ] ≡R | y a ψ} are equal for each a ∈ A. We can safely add ⊥ to both Φ x,a and Φ y,a since, whenever both x and y terminate, they are either both stuck or both terminal. In fact, equality and inequality are preserved while adding ⊥ since Φ x,a = ∅ =⇒ ⊥ / ∈ Φ y,a (and vice versa) by hypothesis. For each C ∈ X/R (x, y ∈ X and a ∈ A) let Ψ x,a,C (Φ x,a \ {[ρ] ≡R | ρ(C) = 0}) ∪ {⊥}. Clearly Φ x,a ∪ = C∈X/R Ψ x,a,C and if (x, y) ∈ R then Ψ x,a,C = Ψ y,a,C . Complementarily, if (x, y) / ∈ R then there exists some ϕ ∈ Φ x,a s.t. for no ψ ∈ Φ y,a ϕ ≡ R ψ or vice versa; w.l.o.g. assume the former. Hence there exists C ∈ X/R such that ϕ(C) = ψ(C) whence Ψ x,a,C = Ψ y,a,C . Finally, we conclude by M(x, a, C) = Ψ x,a,C for each x ∈ X, a ∈ A and C ∈ X/R.
Proof of Proposition 6. Let (X, A, X ), (Y, A, Y ), (X, α) and (Y, β) be two ULTraS over a given commutative monoid W and their corresponding coalgebras (cf. Proposition 5). Recall that a function f : X → Y is a also coalgebra morphism f : α → β iff, for each x ∈ X, and a ∈ A: where ϕ[f ] denotes the action of f on ϕ (i.e. the function λy : Y. x∈f −1 (y) ϕ(x)) and function equality is defined point-wise as usual.
Firstly, we prove that if R is a kernel relation of some jointly epic cospan of coalgebra mophism from α and β then it is a bisimulation in the sense of Definition 4. Let the aforementioned cospan be (X, α) f ← − (Z, γ) g − → (Y, β), (Z, A, Z ) the ULTraS for γ and assume x and y such that f (x) = g(y). Since f is coalgebra homomorphism, f (x) = z implies: x a X ϕ ⇐⇒ z a Z ρ = ϕ[f ] = λc : Z. x∈f −1 (c) ϕ(x).
Therefore f (x) = g(y) implies: x a X ϕ =⇒ y a Y ψ ∧ ∀C ∈ Z. x∈f −1 (C) ϕ(x) = y∈g −1 (C) ψ(y) y a Y ψ =⇒ x a X ϕ ∧ ∀C ∈ Z. x∈f −1 (C) ϕ(x) = y∈g −1 (C) ψ(y) We conclude by noting that if R is the kernel of f, g there is a bijective correspondence between its equivalence classes and elements in Z since every class is in the image of f or g by the epic sink assumption. For the converse, given a bisimulation R for (X, A, X ) (Y, A, Y ) let Z be the set of the equivalence classes in R and consider the ULTraS (Z, A, Z ) defined as follows: The two statements are redundant since x, y ∈ C ⇐⇒ xRy and hence iff for every x a − → X ϕ there is y a − → Y ψ s.t. ϕ ≡ R ψ and vice versa. Finally, class membership defines a jointly epic coalgebra cospan from the coalgebras associated to (X, A, X ) and (Y, A, Y ) to the one associated to (Z, A, Z ) by simply mapping each x ∈ X and each y ∈ Y to its class.