On the trade-off between labels and weights in quantitative bisimulation

TL;DR

This paper explores the expressiveness of various quantitative transition system models, revealing a trade-off between label information and weights, and establishing their fundamental differences and relationships.

Contribution

It introduces a formal analysis of the trade-off between labels and weights in quantitative models, showing their fundamental distinctions and the limits of reduction.

Findings

Weighted transition systems use only weights to encode information.

Labelled transition systems rely solely on labels for information.

The models form a spectrum with no further significant reductions possible.

Abstract

Reductions for transition systems have been recently introduced as a uniform and principled method for comparing the expressiveness of system models with respect to a range of properties, especially bisimulations. In this paper we study the expressiveness (w.r.t. bisimulations) of models for quantitative computations such as weighted labelled transition systems (WLTSs), uniform labelled transition systems (ULTraSs), and state-to-function transition systems (FuTSs). We prove that there is a trade-off between labels and weights: at one extreme lays the class of (unlabelled) weighted transition systems where information is presented using weights only; at the other lays the class of labelled transition systems (LTSs) where information is shifted on labels. These categories of systems cannot be further reduced in any significant way and subsume all the aforementioned models.

Equations

$$T::=(S-{)}^A\mid T\times (S-{)}^{A}S::={\mathcal{F}}_{\text{mspace}-1.0muM}\mid {\mathcal{F}}_{\text{mspace}-1.0muM}\circ S$$

$$({\mathcal{F}}_{\text{mspace}-1.0mu\text{vv}M}f{)}^{\text{vv}A}\triangleq {\prod }_{i=0}^n({\mathcal{F}}_{\text{mspace}-1.0mu\text{vv}{M}_i}f{)}^{A_i}({\mathcal{F}}_{\text{mspace}-1.0mu\text{vv}{M}_i}f{)}^{A_i}\triangleq ({\mathcal{F}}_{\text{mspace}-1.0mu{M}_{i,0}}\dots {\mathcal{F}}_{\text{mspace}-1.0mu{M}_{i,m_i}}f{)}^{A_i}$$

$$R{\sigma }^b{R}^{\prime }⟹(xR{x}^{\prime }⟺{\sigma }^c(x)R^{\prime }{\sigma }^c(x^{\prime }))\text{.}$$

$$\{{\sigma }_{\alpha }:\alpha \to \sigma (\alpha ){\}}_{\alpha \in \text{C}}$$

$${\sigma }_{\beta }^c\circ f=\sigma (f)\circ {\sigma }_{\alpha }^c\text{.}$$

$$\text{Sys}(S)\preccurlyeq \text{Sys}(T)⟹\left|\mathrm{car}\left(\nu S\right)\right|\le \left|\mathrm{car}\left(\nu T\right)\right|\text{.}$$

$$R\in \mathrm{bis}(\sigma (\nu S))⟹({\sigma }_{\nu S}^c(x)R{\sigma }_{\nu S}^c(y)⟺x=y)\text{.}$$

$$R{\sigma }^b{R}^{\prime }⟺(xRy⟺{\sigma }^c(x)R^{\prime }{\sigma }^c(y))\text{.}$$

$$\text{Sys}(S)\preccurlyeq \text{Sys}(T)⟸\left|\mathrm{car}\left(\nu S\right)\right|\le \left|\mathrm{car}\left(\nu T\right)\right|\text{.}$$

$$X+\mathrm{car}\left(\nu T\right)$$

$$\text{Sys}(S)\preccurlyeq \text{Sys}(T)⟺\left|\mathrm{car}\left(\nu S\right)\right|\le \left|\mathrm{car}\left(\nu T\right)\right|\text{.}$$

$$\max ({\aleph }_0,\left|M\right|,\left|A\right|)\le \left|\mathrm{car}\left(\nu ({\mathcal{F}}_{\text{mspace}-1.0muM}-{)}^A\right)\right|\text{.}$$

$$\left|\mathrm{car}\left(\nu ({\mathcal{F}}_{\text{mspace}-1.0muM}-{)}^A\right)\right|\le {\left|M\right|}^{\max ({\aleph }_0,|A|)}\text{.}$$

$$X\cong ({\mathcal{F}}_{\text{mspace}-1.0muM}X{)}^A⟹\left|X\right|\ge \max ({\aleph }_0,\left|M\right|,\left|A\right|)\text{.}$$

$$\left|X\right|=\left|({\mathcal{F}}_{\text{mspace}-1.0muM}X{)}^A\right|={\left|M\right|}^{|X||A|}\ge 2^{|X|}>\left|X\right|$$

$$\left|M\right|=\left|\{x\cdot m\mid m\in M\}\right|\le \left|({\mathcal{F}}_{\text{mspace}-1.0muM}X{)}^A\right|=\left|X\right|$$

$$\left|A\right|=\left|\{{\delta }_a\mid a\in A\}\right|\le \left|({\mathcal{F}}_{\text{mspace}-1.0muM}X{)}^A\right|=\left|X\right|\text{.}$$

$$F_{\alpha +1}=({\mathcal{F}}_{\text{mspace}-1.0muM}{F}_{\alpha }{)}^A{F}_{\alpha +1}^{\beta +1}=({\mathcal{F}}_{\text{mspace}-1.0muM}{F}_{\alpha }^{\beta }{)}^A$$

$$\left|F_{\alpha }\right|\le {\left|M\right|}^{\max ({\aleph }_0,|A|)}\text{.}$$

$$\left|F_{n+1}\right|$$

$$={\left(\sum _{k\in \mathbb{N}}{\left({\left|M\right|}^{\max ({\aleph }_0,|A|)}\right)}^k\right)}^{|A|}\le {\left({\left|M\right|}^{\max ({\aleph }_0,|A|)}\right)}^{{\aleph }_0\cdot |A|}={\left|M\right|}^{\max ({\aleph }_0,|A|)}\text{.}$$

$$\left|F_{\omega }\right|$$

$$2^{\kappa }$$

$$\stackrel{(\text{hypertarget}thm:wlts-reduction-1-5\text{v})}{\le }{\left|\underline{M}\right|}^{\max \left({\aleph }_0,|\underline{A}|\right)}$$

$${\left|\underline{M}\right|}^{\max \left({\aleph }_0,|\underline{A}|\right)}=2^{\max \left({\aleph }_0,|\underline{A}|\right)}=\max \left(2^{{\aleph }_0},2^{|\underline{A}|}\right)\text{.}$$

$${\left|\underline{M}\right|}^{\max \left({\aleph }_0,|\underline{A}|\right)}={\left|\underline{M}\right|}^{|\underline{A}|}\ge 2^{|\underline{A}|}\text{.}$$

$$2^{\kappa }<{\left|\underline{M}\right|}^{\max ({\aleph }_0,|\underline{A}|)}={\left|\underline{M}\right|}^{{\aleph }_0}\le \max \left(2^{|\underline{M}|},2^{{\aleph }_0}\right)=2^{|\underline{M}|}$$

$$\left|\mathrm{car}\left(\nu ({\mathcal{F}}_{\text{mspace}-1.0muM}-{)}^A\right)\right|\le {\left|M\right|}^{\max ({\aleph }_0,|A|)}\le \max (\underline{A},\underline{M})\le \left|\mathrm{car}\left(\nu ({\mathcal{F}}_{\text{mspace}-1.0mu\underline{M}}-{)}^{\underline{A}}\right)\right|\text{.}$$

$$\text{vv}0=\sum _{a\in A}0\cdot a$$

$$\sum _{a\in A}{m}_a\cdot a+\sum _{a\in A}{n}_a\cdot a=\sum _{a\in A}(m_a+n_a)\cdot a\text{.}$$

Full text

1 Introduction

Weighted labelled transition systems (WLTSs) [10] are a meta-model for systems with quantitative aspects: transitions are of the form $P\xrightarrow{a,w}Q$ and labelled with weights $w$ that are taken from a given monoidal weight structure and express the quantity associated to the computational step. Many computational aspects can be captured just by changing the underlying weight structure: weights can model probabilities, resource costs, stochastic rates, \etc; as such, WLTSs are a generalisation of labelled transition systems (LTSs) [18], probabilistic systems (PLTSs) [23], stochastic systems [8], among others. Definitions and results developed in this setting instantiate to existing models, thus recovering known results and discovering new ones. In particular, the notion of weighted bisimulation in WLTSs coincides with that of (strong) bisimulation for all the aforementioned models [10].

In the wake of these encouraging results, other meta-models have been proposed aiming to cover an even wider range of computational models and concepts. Uniform labelled transition systems (ULTraSs) [2] are systems whose transitions have the form $P\xrightarrow{a}\phi$, where $\phi$ is a weight function assigning weights to states; hence, ULTraSs can be seen both as a non-deterministic extension of WLTSs and as a generalisation of Segala’s probabilistic systems [21] (NPLTSs). In [14, 16] a (coalgebraically derived) notion of bisimulation for ULTraSs is presented and shown to precisely capture bisimulations for weighted and Segala systems. Function-to-state transition systems (FuTSs) were introduced in [5] as a generalisation of the above, of IMCs [7], and of other models used to formalise the semantics of several process calculi with quantitative aspects. Later, [12] defined a (coalgebraically derived) notion of (strong) bisimulation for FuTSs which instantiates to known bisimulations for all the aforementioned models and hence can be taken as a general schema for defining quantitative bisimulations (\cf[11]).

Given all these meta-models, it is natural to wonder about their expressiveness. We should consider not only the class of systems these frameworks can represent, but also whether these representations are faithful with respect to the properties we are interested in. Intuitively, a meta-model M is subsumed by $\textnormal{{M}}^{\prime}$ according to a property $P$ if any system $S$ which is an instance of M with the property $P$, is also an instance of $\textnormal{{M}}^{\prime}$ preserving $P$.

In this work we study these meta-models according to their ability to correctly express strong bisimulation. In this context, a meta-model M is subsumed by $\textnormal{{M}}^{\prime}$ if any system $S$ which is an instance of M, is also an instance of $\textnormal{{M}}^{\prime}$ preserving and reflecting bisimulations.

Previous work [10, 2, 14, 16, 12] has shown that, according to this order, each of the models mentioned above subsumes the previous ones, thus forming the hierarchy shown in Figure 1. These results rely on direct inclusions between classes of models (\egLTSs are WLTSs on booleans) or some \adhocarguments (\egWLTSs are “functional” ULTraSs). Furthermore, in \loccitit is never shown if any of these models is strictly more expressive than the ones it subsumes.

To address this issue in a uniform and principled way, we introduced in [15] the notion of reduction between categories of systems and used it to formally define expressiveness of models with respect to (strong) bisimulation. We remark that this notion is far more general and can be used to study any category of state-based transition systems: all constructions and results are developed abstracting from the “type” of computation under scrutiny thanks to the theory of coalgebras [20]. This level of abstraction allowed us to formulate general results for the systematic derivation of reductions. As an application, we derived a reduction taking FuTSs to WLTSs hence proving that the former are subsumed by the latter. Because of this reduction, the hierarchy in Figure 1 collapses to that in Figure 1.

In [15] we left unanswered a fundamental question about this hierarchy of models:

Can the hierarchy of FuTSs/WLTSs be further collapsed in any meaningful way?

To provide this answer we extend the framework of reductions with new results concerning the existence of reductions and determine necessary and sufficient conditions for a wide class of systems of interest. Thanks to these methods, we are able to formally prove that there is a trade-off between labels and weights in the definition of WLTSs and similar models: information and complexity can be shifted from labels to weights and \viceversain ways that are coherent with model semantics as per the notion of quantitative bisimulation. At the two ends of this trade-off we find labelled transition systems and “unlabelled” weighted transition systems. As a consequence, LTSs subsume the whole hierarchy of models described above.

Synopsis

In Section 2 we recall from [20] basic notions of coalgebras and their use as a uniform model of (discrete) transition systems, their bisimulation, and final semantics. In Section 3 we recall from [15] relevant definitions about reductions and extend this framework with new results. In particular, in Section 3.2 we introduce necessary and sufficient conditions for reductions to exist under the assumption that all types involved have final coalgebras. In Section 4 we focus the lens of reductions on WLTSs and study under which conditions the category of WLTSs can be reduced. In Section 5 we apply the results we introduced in Section 3.2 to the category of FuTSs to prove that it reduces to that of WLTSs. The result is known since [15, Sec. 6] but here we provide an alternative proof. Final remarks are in Section 6.

2 Discrete transition systems

Coalgebras are a well established framework for modelling and studying the operational semantics of (abstract) computational devices such as automata, concurrent systems, and reactive ones; the methodology is termed universal coalgebra [20]. In this approach, the first step is to define a behavioural endofunctor $T$ over the category Set of small sets and functions modelling the computational aspects under scrutiny. Here, the term “modelling” has to be intended in the sense that, for $X$ a set of states, $TX$ is the set of possible behaviours over $X$. Then, a system is modelled by a $T$-coalgebra \iea pair $(X,\alpha\colon X\to TX)$ where the set $X$, called carrier, is the state-space of the system and the map $\alpha$, called structure, associates each state with its behaviour. Coalgebras are often identified with their structure; in this situation the carrier $X$ of a $T$-coalgebra $\alpha\colon X\to TX$ will be denoted by ${\mathrm{car}\left({\alpha}\right)}$. The definition of the endofunctor $T$ constitutes the crucial step of this method, as it corresponds to specify the behaviours that the systems under scrutiny are meant to exhibit \ietheir dynamics and observations. Hence, $T$-coalgebras and the systems they model are said to be of type $T$. Herein, the terms “coalgebra” and “system” (of type $T$) will be often treated as synonyms. Once a behavioural endofunctor is defined, this canonically determines a notion of coalgebra homomorphism \iestructure preserving maps between carriers: a $T$-homomorphism from $\alpha\colon X\to TX$ to $\beta\colon Y\to TY$ is a function $f\colon X\to Y$ such that $Tf\circ\alpha=f\circ\beta$. Categories formed by systems and their homomorphisms will be called categories of systems and the category of all $T$-systems will be denoted as ${\textnormal{{Sys}}(T)}$.

Because homomorphisms preserve structures (hence system dynamics), their codomain can be thought of as a refinement system for their domain in the sense that they can aggregate states with equivalent dynamics. This observation corresponds to the notion of (kernel) bisimulation: a relation $R$ on $X$ is bisimulation for a system $\alpha\colon X\to TX$ provided it is the kernel of a function underlying some $T$-homomorphism with domain $\alpha$ [22]. This notion of bisimulation generalises Milner’s strong bisimulation for LTSs as well as its generalisation to all the models considered in this work. The set of all bisimulations for a $T$-system $\alpha$ will be denoted as $\operatorname{bis}(\alpha)$.

Under mild conditions on the behavioural endofunctor $T$, there exists a final $T$-system $\operatorname{\nu}T$ which describes all abstract behaviours of type $T$. Final $T$-systems are final objects in the category ${\textnormal{{Sys}}(T)}$ [1, 24]. Finality means that every $T$-system $\alpha$ has a unique homomorphism $!_{h}$ into the final $T$-system. The function ${\mathrm{car}\left({\alpha}\right)}\to{\mathrm{car}\left({\operatorname{\nu}T}\right)}$ underlying $!_{\alpha}\colon\alpha\to\operatorname{\nu}T$ uniquely associates each state in ${\mathrm{car}\left({\alpha}\right)}$ with a semantics, called final semantics, in the form of an abstract behaviour. Final semantics uniquely associates bisimilar states to the same abstract behaviour. As a consequence, states of final coalgebras can only be bisimilar to themselves. This property is called strong extensionality and identifies final homomorphisms with the coinductive proof principle [9]. Because of its relation with coinduction, the unique homomorphism from a system $\alpha$ into the final one is also called coinductive extension of $\alpha$.

Example 1** (LTSs).**

It has been shown in [20] that:

• •

image finite LTSs over a set of labels $A$ are $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}-)^{A}$-systems where $\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}$ is the finite powerset functor;

• •

the notion of (kernel) bisimulation for $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}-)^{A}$-systems coincides with Milner’s (strong) bisimulation for LTSs;

• •

the endofunctor $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}-)^{A}$ has final systems.

For exposition sake, sets of labels are implicitly assumed to not be empty—thus avoiding degenerate systems of type $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}-)^{0}\cong 1$. Hereafter, let LTS denote the category of all image-finite labelled transition systems and let $\textnormal{{LTS}}(A)\triangleq\textnormal{{Sys}}((\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}-)^{A})$ be its subcategory of systems whose labels range over $A$. ∎

For $(M,+,0)$ an abelian monoid111An abelian monoid is a set $M$ equipped with an associative and commutative binary operation $+$ and a unit [math] for $+$; such structure is called trivial when $M$ is a singleton., the generalised (finite) multiset functor $\mathcal{F}_{\mspace{-1.0mu}M}$ is the endofunctor over Set which assigns:

• •

to each set $X$ the set $\{\phi\colon X\to M\mid\operatorname{supp}(\phi)\text{ is finite}\}$ of finitely supported weight functions (the support of $\phi$ is the set $\operatorname{supp}(\phi)=\{x\mid\phi(x)\neq 0\}$);

• •

to each function $f\colon X\to Y$ the map $(\mathcal{F}_{\mspace{-1.0mu}M}f)(\phi)=\lambda y\in Y.\sum_{x:f(x)=y}\phi(x)$. (summation is well defined because $\phi$ is finitely supported).

Note that if $M$ is trivial then $\mathcal{F}_{\mspace{-1.0mu}M}X$ is always a singleton whence, monoids of weights are implicitly assumed to not be trivial. Elements of $\mathcal{F}_{\mspace{-1.0mu}M}X$ will be often presented in formal sum notation: for $\phi\in\mathcal{F}_{\mspace{-1.0mu}M}X$ we write $\sum_{x}\phi(x)\cdot x$ or, given $\operatorname{supp}(\phi)=\{x_{1},\ldots,x_{n}\}$, simply $\sum_{i=1,\ldots,n}\phi(x_{i})\cdot x_{i}$. For instance, $\mathcal{F}_{\mspace{-1.0mu}M}(f)(\phi)$ is formulated as $\sum\phi(x)\cdot f(x)$.

Example 2** (WLTSs).**

Let $A$ be a non-empty set and $M$ a non-trivial abelian monoid. It has been shown in [10] that:

• •

WLTSs with labels drawn from $A$ and weights drawn from $M$ are $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-system;

• •

the notion of (kernel) bisimulation for $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-systems coincides with that of weighted bisimulation;

• •

the endofunctor $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ has final systems.

In the sequel, let WLTS be the category of all weighted labelled transition systems and write $\textnormal{{WLTS}}(A,M)$ for its subcategory ${\textnormal{{Sys}}((\mathcal{F}_{\mspace{-1.0mu}M}-)^{A})}$ formed by $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-systems. If weights are drawn from the monoid $\mathbb{B}=(\{\texttt{t\!t},\texttt{f\!f}\},\lor,\texttt{f\!f})$ of boolean values under disjunction then, $\textnormal{{WLTS}}(A,\mathbb{B})$ is (isomorphic to) $\textnormal{{LTS}}(A)$ and the associated notions of bisimulation coincide. ∎

Example 3** (ULTraSs).**

Let $A$ be a non-empty set and $M$ a non-trivial abelian monoid. It has been shown in [14, 16] that (image finite) ULTraSs on $A$ and $M$ are $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-systems. The notion of bisimulation for $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-systems coincides with that of strong bisimulation as per [14, 16]. The functor $(\mathcal{P}_{\mspace{-1.0mu}\mspace{-2.0mu}f}\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ admits final systems. Let ULTraS denote the category of all image-finite ULTraSs and $\textnormal{{ULTraS}}(A,M)$ its subcategory of systems with labels in $A$ and weights in $M$. WLTSs can be cast to ULTraSs by wrapping each target of their transitions into a singleton (\ieby post-composition with components of the powerset unit). In [2] ULTraSs obtained in this way are called functional and, as shown in [14], the casting operation is faithful to the semantics of WLTSs. ∎

Example 4** (FuTSs).**

FuTSs are systems for any endofunctor $T$ by the grammar

[TABLE]

where $A$ and $M$ range over (non-empty) sets of labels and (non-trivial) abelian monoids, respectively. Any such endofunctor is equivalently described by

[TABLE]

where $\vv{A}=\langle A_{0},\dots,A_{n}\rangle$ is a sequence of (non-empty) sets of labels, each $\vv{M}_{i}=\langle M_{i,0},\dots,M_{i,m_{i}}\rangle$ is a sequence of non-trivial abelian monoids, and $\vv{M}=\langle\vv{M}_{0},\dots,\vv{M}_{n}\rangle$. (Up to minor notational variations, this characterisation can be found in [12, 16].) The notion of bisimulation for $(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}f)^{\vv{A}}$-systems coincides with that of strong bisimulation for FuTSs described in [12]. In \loccitit is shown that every $(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}f)^{\vv{A}}$ has final systems. For any $\vv{A}$ and $\vv{M}$ as above define $\textnormal{{FuTS}}(\vv{A},\vv{M})$ as category ${\textnormal{{Sys}}(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}})}$. Clearly, $\textnormal{{FuTS}}(\langle A),\langle M\rangle)$ and $\textnormal{{FuTS}}(\langle A\rangle,\langle\mathbb{B},M\rangle)$ coincide with $\textnormal{{WLTS}}(A,M)$ and $\textnormal{{ULTraS}}(A,M)$, respectively. As a consequence, the categories LTS, WLTS, and ULTraS are all subcategories of FuTS, the category of all FuTSs. ∎

3 Reductions for discrete transition systems

In [15] the notion of reduction was introduced in order to formalise the intuition that a behaviour type is (at least) as expressive as another whenever systems and homomorphisms of the latter can be “encoded” as systems and homomorphisms of the former and provided that their semantically relevant structures are both preserved and reflected. In this work we extend the framework of reductions with new results concerning existence of reductions under the assumption that the involved types have final systems.

3.1 Reductions

Intuitively, to reduce a transition system (source) to another (target) of a possibly different type means to “encode” the state space of the former into the state space of the latter while preserving and reflecting their semantically relevant structure and properties. Because the source and target system of a reduction may be of different types, structure preservation cannot be formalised as a system homomorphism. Instead, reductions rely on an indirect expression of homomorphisms: bisimulations. Reductions require that every bisimulation for the source system is assigned to bisimulations for the target system that are coherent with the encoding of the state space.

Definition 1**.**

For systems $\alpha$ and $\beta$, a (system) reduction $\sigma\colon\alpha\to\beta$ is given by

a function $\sigma^{c}\colon{\mathrm{car}\left({\alpha}\right)}\to{\mathrm{car}\left({\beta}\right)}$ and 2. 2.

a left-total222A relation $R\subseteq X\times Y$ is called left-total or multivalued function if for every $x\in X$ there is $y\in Y$ s.t. $x\mathrel{R}y$. relation $\sigma^{b}\subseteq\operatorname{bis}(\alpha)\times\operatorname{bis}(\beta)$

such that $\sigma^{c}$ carries a relation homomorphism for any pair of bisimulations in $\sigma^{b}$, \ie:

[TABLE]

A system reduction $\sigma\colon\alpha\to\beta$ is called full whenever $\sigma^{c}\colon{\mathrm{car}\left({\alpha}\right)}\to{\mathrm{car}\left({\beta}\right)}$ is surjective.

As a consequence of Condition ($\diamondsuit$ ‣ 1), the function $\sigma^{c}$ is always injective and the correspondence $\sigma^{b}$ is always left-unique333A relation $R\subseteq X\times Y$ is called left-unique or injective if for every $y\in Y$ there is at most one $x\in X$ s.t. $x\mathrel{R}y$..

Proposition 1**.**

For $\sigma\colon\alpha\to\beta$ a system reduction, $\sigma^{c}$ is injective and $\sigma^{b}$ is left-unique.

Proof.

Observe that the diagonal (or identity) relation on a system state space is always a bisimulation. For a set $X$, write $\Delta_{X}$ for the diagonal on $X$. By left-totality of $\sigma^{b}$, there is a bisimulation $R$ for $\beta$ such that $\Delta_{{\mathrm{car}\left({\alpha}\right)}}\mathrel{\sigma^{b}}R$. Then, it follows from Condition ($\diamondsuit$ ‣ 1), that $\sigma^{c}(x)\mathrel{R}\sigma^{c}(x^{\prime})$ if and only if $x\mathrel{\Delta_{{\mathrm{car}\left({\alpha}\right)}}}x^{\prime}$ \ieif and only if $x=x^{\prime}$. Left-uniqueness follows immediately from injectivity of $\sigma^{c}$. ∎

The first property guarantees that reductions preserve the identity of states and this is of relevance \egwhen these are presented as terms of some process calculus or programming language, since reductions provide alternative but faithful semantics. The second property ensures that given $\sigma\colon\alpha\to\beta$ any bisimulation for $\alpha$ can be recovered by restricting some bisimulation for $\beta$ to the image of ${\mathrm{car}\left({\alpha}\right)}$ in ${\mathrm{car}\left({\beta}\right)}$ through the injection $\sigma^{c}$.

Fullness identifies reductions that use the state space of the target system in its entirety which means that full reductions do not introduce auxiliary states.

Proposition 2**.**

For $\sigma\colon\alpha\to\beta$ a full system reduction, the map $\sigma^{c}$ is an isomorphism and the relation $\sigma^{b}$ is right-unique444A relation $R\subseteq X\times Y$ is called right-unique if for every $x\in X$ there is $y\in Y$ s.t. $x\mathrel{R}y$..

Proof.

Assume that $\sigma$ is full. The function $\sigma^{c}$ is injective and surjective hence an isomorphism. Then it follows from condition ($\diamondsuit$ ‣ 1) that $\sigma^{b}$ is also right-unique since states related by a bisimulation of the target system are always image of states of the source system ∎

System reductions can be extended to categories of systems by equipping functors with them and ensuring they respect the structure of homomorphisms. Formally:

Definition 2**.**

For C and D categories of system, a reduction $\sigma$ from C to D, written $\sigma\colon\textnormal{{C}}\to\textnormal{{D}}$, is a functor going from C to D equipped with a collection of system reductions

[TABLE]

such that for any $f\colon\alpha\to\beta$ in C:

[TABLE]

A reduction $\sigma\colon\textnormal{{C}}\to\textnormal{{D}}$ is called full if, and only if, every system reduction $\sigma_{\alpha}$ is full. A category C is said to reduce (resp. fully reduce) to D, if there is a reduction (resp. a full reduction) going from C to D.

Notation**.**

For categories C and D we write $\textnormal{{C}}\preccurlyeq\textnormal{{D}}$ if C reduces to D, $\textnormal{{C}}\approxeq\textnormal{{D}}$ if $\textnormal{{C}}\preccurlyeq\textnormal{{D}}$ and $\textnormal{{C}}\succcurlyeq\textnormal{{D}}$, $\textnormal{{C}}\mathrel{\dot{\preccurlyeq}}\textnormal{{D}}$ and $\textnormal{{C}}\mathrel{\dot{\approxeq}}\textnormal{{D}}$ if the reductions involved are full.

Reductions form a category. To compose reductions $\sigma\colon\textnormal{{C}}\to\textnormal{{D}}$ and $\tau\colon\textnormal{{D}}\to\textnormal{{E}}$ it suffices to compose their underlying functors and each system reduction accordingly: the composite reduction $\tau\circ\sigma\colon\textnormal{{C}}\to\textnormal{{E}}$ is the composite functor $\tau\circ\sigma$ equipped with the family of system reductions given on each $\alpha\in\textnormal{{C}}$ by $(\tau\circ\sigma)_{\alpha}^{c}\triangleq\tau_{\sigma(\alpha)}^{c}\circ\sigma_{\alpha}^{c}$ and $(\tau\circ\sigma)_{\alpha}^{b}\triangleq\tau_{\sigma(\alpha)}^{b}\circ\sigma_{\alpha}^{b}$. Reduction composition is associative and admits identities which are given on every C as the identity assignments for systems and homomorphisms. Any reduction restricts to a reduction from a subcategory of its domain and extends to a reduction to a super-category of its codomain. Fullness is preserved by the above operations and full reductions form a category that lies in the category of reductions.

3.2 Reductions and final systems

Final systems describe all abstract behaviours for their type \ieall behaviours bisimulations cannot distinguish. Reductions preserve and reflect bisimulations and are injective on state spaces. As a consequence, for a reduction going from ${\textnormal{{Sys}}(S)}$ to ${\textnormal{{Sys}}(T)}$ to exist, it is necessary that there are at least as many abstract behaviours of type $T$ as are those of type $S$.

Lemma 3**.**

For any $S$ and $T$, if both admit final systems then:

[TABLE]

Proof.

Let $\sigma$ be a reduction going from ${\textnormal{{Sys}}(S)}$ to ${\textnormal{{Sys}}(T)}$. It follows from Proposition 1 that ${\left|{\mathrm{car}\left({\operatorname{\nu}S}\right)}\right|}\leq{\left|{\mathrm{car}\left({\sigma(\operatorname{\nu}S)}\right)}\right|}$ and from Condition ($\diamondsuit$ ‣ 1) that $\sigma(\operatorname{\nu}S)$ is strongly extensional on the image of ${\mathrm{car}\left({\operatorname{\nu}S}\right)}$ \ie:

[TABLE]

As a consequence, the $T$-system $\sigma(\operatorname{\nu}S)$ exhibits at least as many distinct abstract behaviours as the final $S$-systems $\operatorname{\nu}S$. Therefore, ${\left|{\mathrm{car}\left({\operatorname{\nu}S}\right)}\right|}\leq{\left|{\mathrm{car}\left({\operatorname{\nu}T}\right)}\right|}$ or otherwise there would be $x,y\in{\mathrm{car}\left({\operatorname{\nu}S}\right)}$ such that $x\nsim_{S}y$ but $\sigma^{c}_{\operatorname{\nu}S}(x)\sim_{T}\sigma^{c}_{\operatorname{\nu}S}(y)$. ∎

The condition on the size of final systems is not only necessary but also sufficient for having a reduction. Intuitively, the size condition guarantees that it is possible to represent abstract behaviours of the source type $S$ as abstract behaviour of type $T$ by means of a system reduction for the final system. In fact, provided that ${\left|{\mathrm{car}\left({\operatorname{\nu}S}\right)}\right|}\leq{\left|{\mathrm{car}\left({\operatorname{\nu}T}\right)}\right|}$, it is possible to fix an injection $\sigma^{c}\colon{\mathrm{car}\left({\operatorname{\nu}S}\right)}\to{\mathrm{car}\left({\operatorname{\nu}T}\right)}$ to be used as an “encoding”. Since final systems are strongly extensional, this map uniquely identifies a left-total relation $\sigma^{b}\subseteq\operatorname{bis}(\operatorname{\nu}S)\times\operatorname{bis}(\operatorname{\nu}T)$ such that

[TABLE]

By construction, $\sigma^{c}$ and $\sigma^{b}$ define a system reduction $\sigma\colon\operatorname{\nu}S\to\operatorname{\nu}T$. Once all abstract behaviours are covered, the reduction can be extended to every other $S$-system along their final semantics.

Lemma 4**.**

For any $S$ and $T$, if both admit final systems then:

[TABLE]

Proof.

Assume that ${\left|{\mathrm{car}\left({\operatorname{\nu}S}\right)}\right|}\leq{\left|{\mathrm{car}\left({\operatorname{\nu}T}\right)}\right|}$ and let $e\colon{\mathrm{car}\left({\operatorname{\nu}S}\right)}\to{\mathrm{car}\left({\operatorname{\nu}T}\right)}$ be any injective map. For $\alpha\colon X\to SX$ define $\sigma(\alpha)$ as the $T$-system depicted in the diagram below:

[TABLE]

where ${inr}_{X,{\mathrm{car}\left({\operatorname{\nu}T}\right)}}$ is the right injection into the coproduct $X+{\mathrm{car}\left({\operatorname{\nu}T}\right)}$. Let $R\in\operatorname{bis}(\alpha)$ and consider the relation $R^{\prime}=R\cup\Delta_{{\mathrm{car}\left({\operatorname{\nu}T}\right)}}$ on ${\mathrm{car}\left({\sigma(\alpha)}\right)}$. Observe that $x\mathrel{R^{\prime}}y$ whenever $x=y$ or $x\mathrel{R}y$ and that $R\subseteq{\sim_{S}}$. Therefore, the relation $R^{\prime}$ is a bisimulation for $\sigma(\alpha)$ by construction. Define $\sigma_{\alpha}^{c}\colon X\to X+{\mathrm{car}\left({\operatorname{\nu}T}\right)}$ as the left injection into the coproduct and $\sigma_{\alpha}^{b}$ as the (left-total) relation $\{(R,R\cup\Delta_{{\mathrm{car}\left({\operatorname{\nu}T}\right)}})\mid R\in\operatorname{bis}(\alpha)\}$. If follows from the observation above that $\sigma_{\alpha}^{c}$ and $\sigma_{\alpha}^{b}$ form a reduction going from $\alpha$ to $\sigma(\alpha)$. For $f\colon\alpha\to\beta$ a $S$-homomorphism, the function $f\times{id}_{{\mathrm{car}\left({\operatorname{\nu}T}\right)}}$ carries a $T$-homomorphism going from $\sigma(\alpha)$ to $\sigma(\beta)$ as shown by the commuting diagram below:

[TABLE]

Note that the left triangle commutes by definition of final system. As a consequence, the mappings $\alpha\mapsto\sigma(\alpha)$ and $f\mapsto f\times{id}_{{\mathrm{car}\left({\operatorname{\nu}T}\right)}}$ define a functor $\sigma\colon{\textnormal{{Sys}}(S)}\to{\textnormal{{Sys}}(T)}$. This functor is coherent with the family of system reductions $\{\sigma_{\alpha}\}_{\alpha\in{\textnormal{{Sys}}(S)}}$ defined above and hence extends to a reduction from ${\textnormal{{Sys}}(S)}$ to ${\textnormal{{Sys}}(T)}$. ∎

It follows from Lemmas 3 and 4 that the condition on the size of final systems is both necessary and sufficient for the existence of a reduction. Formally:

Theorem 5**.**

For any $S$ and $T$, if both admit final systems then:

[TABLE]

As a consequence, to prove or disprove that there is a reduction taking $S$-systems to $T$-systems it suffices to provide an upper and a lower bound to the size of their final systems, respectively.

4 Reducing weighted transition systems

In this section we address the main question left open in [15] \iewhether it is possible to collapse the hierarchy of FuTSs beyond the category of WLTSs. To answer this question, we determine conditions on subcategories of WLTS that are necessary and sufficient for a reduction to exist. Remarkably, these conditions involve solely the total number of labels and weights used by systems of a certain type. This suggests the possibility for reductions to shift information between labels and weights while preserving the semantics of WLTSs.

In [10], Klin proved that every category $\textnormal{{WLTS}}(A,M)$ has final objects but to the best of our knowledge the cardinality of their carriers has not been studied yet. We determine lower and upper bounds to said cardinality. Albeit conservative, these bounds have the advantage of offering a clear dependency on the cardinality of labels and weights. For any non-empty set $A$ and non-trivial abelian monoid $M$, it holds that:

[TABLE]

Intuitively, the type $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ has at least

• •

$\aleph_{0}$-many abstract behaviours since $M$ is not trivial and natural numbers can be encoded using computation length;

• •

${\left|M\right|}$-many abstract behaviours since there is at least a computation whose first step assigns a given weight to a state;

• •

${\left|A\right|}$-many abstract behaviours since there is at least a computation that is able to proceed under a given label.

For any non-empty set $A$ and non-trivial abelian monoid $M$, it holds that:

[TABLE]

Intuitively, abstract behaviours for $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ can be pictured as certain possibly infinite trees that alternate $A$-indexed branches and $M$-labelled finite branches. These trees have at most $({\left|M\right|}^{\aleph_{0}})^{{\left|A\right|}}={\left|M\right|}^{\aleph_{0}\cdot{\left|A\right|}}={\left|M\right|}^{\max(\aleph_{0},{\left|A\right|})}$ possible ways of branching and their depth is countable. Thus, there are not more than $\left({\left|M\right|}^{\max(\aleph_{0},{\left|A\right|})}\right)^{\aleph_{0}}={\left|M\right|}^{\max(\aleph_{0},{\left|A\right|})}$ of such trees.

Lemma 6**.**

For $(M,+,0)$ a non-trivial abelian monoid and $A$ a non-empty set, $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ has final systems and the cardinality of their carrier satisfies ($\spadesuit$ ‣ 4) and ($\clubsuit$ ‣ 4).

Proof.

Recall from [10, Prop. 3] that $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ has final coalgebras.

In order to prove that ($\spadesuit$ ‣ 4) holds, we claim that the following implication holds:

[TABLE]

Then, ($\spadesuit$ ‣ 4) follows from Lambeck’s Lemma—which states that final coalgebras are always isomorphisms \ieinvariants of their endofunctor. To prove our claim we proceed considering three main cases: one for each factor in $\max(\aleph_{0},{\left|M\right|},{\left|A\right|})$. For the first case assume that $\aleph_{0}=\max(\aleph_{0},{\left|M\right|},{\left|A\right|})$. Assume by contradiction that $X$ is finite. As a consequence, $(\mathcal{F}_{\mspace{-1.0mu}M}X)^{A}$ is the function space $\left(M^{X}\right)^{A}$ leading to the contradiction:

[TABLE]

since ${\left|X\right|}<\aleph_{0}$, ${\left|M\right|}\geq 2$, and ${\left|A\right|}\geq 1$. Therefore, ${\left|X\right|}\geq\aleph_{0}$ must follow from the premise that $X\cong(\mathcal{F}_{\mspace{-1.0mu}M}X)^{A}$ and the assumption that $\aleph_{0}=\max(\aleph_{0},{\left|M\right|},{\left|A\right|})$. For the second case assume that ${\left|M\right|}=\max(\aleph_{0},{\left|M\right|},{\left|A\right|})$. Fix a state $x\in X$. It follows that:

[TABLE]

since $\lambda a.x\cdot m\in(\mathcal{F}_{\mspace{-1.0mu}M}X)^{A}$. For the second case assume that ${\left|A\right|}=\max(\aleph_{0},{\left|M\right|},{\left|A\right|})$. Fix any $x\in X$ and any $m\in M\setminus\{0\}$. For $a\in A$ define $\delta_{a}\colon A\to\mathcal{F}_{\mspace{-1.0mu}M}X$ as the Dirac’s delta function taking $a$ to $x\cdot m$ and everything else to the constantly zero function. It holds that:

[TABLE]

Recall that the final sequence for $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ is a limit preserving functor $F\colon\textnormal{{Ord}}\to\textnormal{{Set}}$ from the category of ordinal numbers to that of sets and such that:

[TABLE]

where $\alpha\leq\beta$ are ordinal numbers and $F^{\beta}_{\alpha}\colon F_{\beta}\to F_{\alpha}$ is the action induced by $\alpha\leq\beta$. We claim that for any ordinal $\alpha$,

[TABLE]

Then, ($\clubsuit$ ‣ 4) holds since the the final sequence for $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ stabilises at the final $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$-coalgebra. Let $\alpha$ be [math]. $F_{0}=\varprojlim_{\alpha<0}F^{0}_{\alpha}=1$. Let $\alpha$ be $n+1$ for $n<\omega$. It holds that:

[TABLE]

where (LABEL:thm:wlts-final-coalgebras-bounds-1) follows from the observation that $\mathcal{F}_{\mspace{-1.0mu}M}X=\bigcup_{k\in\mathbb{N}}\{\rho\in\mathcal{F}_{\mspace{-1.0mu}M}X\mid{\left|\operatorname{supp}(\rho)\right|}=k\}$, (LABEL:thm:wlts-final-coalgebras-bounds-2) from the inductive hypothesis, and the remaining inequalities from basic cardinal arithmetic. Let $\alpha$ be $\omega$. Observe that the limit step $F_{\omega}$ is a subset of $\prod_{n<\omega}F_{n}$. Therefore, it holds that:

[TABLE]

We claim that for any transfinite ordinal $\alpha$ it holds that ${\left|F_{\alpha}\right|}\leq{\left|F_{\omega}\right|}$ and, as a consequence of the above, ($\clubsuit$ ‣ 4). Observe that $\mathcal{F}_{\mspace{-1.0mu}M}$ is finitary and that $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$ preserves injections. Recall from [25] that final sequences for finitary endofunctors stabilise after $\omega+\omega$ steps (\cf[25, Thm. 11]), that all actions for $\omega<\alpha$ are injections, and that this holds also for arbitrary products of finitary endofunctors (\cf[25, Thm. 13]). We conclude that our claims holds true. ∎

Recall from Proposition 1 that reductions never take systems to systems with smaller state spaces and from Theorem 5 that this situation applies also to abstract behaviours described by final systems. Therefore, a consequence of the dependency shown above between the size of final WLTSs and the number of labels and weights they use is that the target of a reduction from the category WLTS to any of its subcategories must have systems with enough labels and weights for every small555A cardinal number is called small if it is the cardinality of a (small) set as opposed to proper classes. cardinal. Formally:

Theorem 7**.**

For C a subcategory of WLTS, if $\textnormal{{WLTS}}\preccurlyeq\textnormal{{C}}$ then for any small cardinal $\kappa$ there is $\alpha\colon X\to(\mathcal{F}_{\mspace{-1.0mu}M}X)^{A}$ in C such that $\kappa\leq\max({\left|M\right|},{\left|A\right|})$.

Proof.

Let $\sigma$ be a reduction going from WLTS to C. Fix a small cardinal $\kappa$ and assume without loss of generality that it is transfinite. Let $A$ and $(M,+,0)$ be a non-empty set and a non-trivial abelian monoid with the property that $2^{\kappa}<{\left|A\right|}+{\left|M\right|}$. Write $\underline{A}$ and $\underline{M}$ for the set of labels and monoid of weights defining the type of the system $\sigma(\operatorname{\nu}(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A})$. Observe that $\sigma$ restricts to a reduction going from ${\textnormal{{Sys}}((\mathcal{F}_{\mspace{-1.0mu}M}-)^{A})}$ to ${\textnormal{{Sys}}((\mathcal{F}_{\mspace{-1.0mu}\underline{M}}-)^{\underline{A}})}$ since homomorphisms respect types and reductions are functors. Then, it holds that:

[TABLE]

where (LABEL:thm:wlts-reduction-1-1) follows from the assumption that $\kappa\geq\aleph_{0}$ and definition of cardinal sum, (LABEL:thm:wlts-reduction-1-2) and (LABEL:thm:wlts-reduction-1-4) follow from Lemma 6, (LABEL:thm:wlts-reduction-1-3) follows from Proposition 1, and (LABEL:thm:wlts-reduction-1-5) follows from the same reasoning used in the proof of Theorem 5. We claim that $\kappa\leq\max({\left|\underline{M}\right|},{\left|\underline{A}\right|})$. The proof is divided in three cases. For the first case, assume that ${\left|\underline{M}\right|}<\aleph_{0}$. As a consequence, it holds that:

[TABLE]

Observe that $2^{\aleph_{0}}\leq 2^{\kappa}$ since cardinal exponentiation is monotonic and $\aleph_{0}\leq\kappa$ by assumption. As a consequence of the last of observation, since the above inequality holds we conclude that $2^{\kappa}<2^{{\left|\underline{A}\right|}}$ and hence that $\kappa\leq{\left|\underline{A}\right|}$. Therefore, $\kappa\leq{\left|\underline{A}\right|}+{\left|\underline{M}\right|}$. For the second case, assume that ${\left|\underline{M}\right|}\geq\aleph_{0}$ and that ${\left|\underline{A}\right|}\geq\aleph_{0}$. As a consequence, it holds that:

[TABLE]

Then, the claim follows from the same argument discussed in the previous case. For the last case, assume that ${\left|\underline{M}\right|}\geq\aleph_{0}$ and ${\left|\underline{A}\right|}\leq\aleph_{0}$. As a consequence, it holds that:

[TABLE]

where the last inequality is an instance of a general result of powers involving at least a transfinite cardinal. It follows by monotonicity of cardinal exponentiation that $\kappa\leq{\left|\underline{M}\right|}$ hence the claim. Since the only assumption put on $\kappa$ is that it is transfinite, the thesis holds true. ∎

A consequence of Theorem 7 is that it cannot exist an instance of the WLTS meta-model that is “universal”: it is not possible to faithfully express all behaviours modelled as WLTSs using a single set of labels and a single monoid of weights.

Corollary 8**.**

There are no $A$ and $M$ such that $\textnormal{{WLTS}}\preccurlyeq\textnormal{{WLTS}}(A,M)$.

Proof.

Assume by contradiction that there are $A$ and $M$ such that $\textnormal{{WLTS}}\preccurlyeq\textnormal{{WLTS}}(A,M)$. It follows from Theorem 7 that ${\left|A\right|}+{\left|M\right|}$ is greater than any small cardinal. As a consequence, at least one between $A$ and $M$ is a proper class whereas they are sets by definition of WLTS. ∎

Theorem 7 describes a condition on a subcategory C of WLTS that is necessary to reduce WLTS to C. However, said condition fails to be sufficient. For a counter example, consider as C the category of all final weighted transition systems. This category satisfies the hypothesis of Theorem 7: for any small cardinal $\kappa$ the category has a system whose type has at least $\kappa$-many labels and weights, combined. However, it is not possible to reduce WLTS to C for the same reason that it is not possible to reduce $\textnormal{{WLTS}}(A,M)$ to its subcategory of final systems: reductions are injective on state spaces and respect system homomorphisms. Because of the injectivity property the target category must at least have, for any small cardinal $\kappa$ a system with a carrier exceeding $\kappa$. Because homomorphisms preserve types, systems from $\textnormal{{WLTS}}(A,M)$ must be reduced to systems of the same type. These observations suggest the following sufficient condition which, roughly speaking, extends that of Theorem 7 by assuming that C has also enough systems for each type in the reduction targeted.

Theorem 9**.**

For C a category of systems, if for any small cardinal $\kappa$ there are $A$ and $M$ such that $\kappa\leq\max({\left|M\right|},{\left|A\right|})$ and $\textnormal{{WLTS}}(A,M)\preccurlyeq\textnormal{{C}}$ then, $\textnormal{{WLTS}}\preccurlyeq\textnormal{{C}}$.

Proof.

Observe that system homomorphisms preserve types and reductions respect homomorphisms. As a consequence, any subcategory $\textnormal{{WLTS}}(A,M)$ of WLTS can be considered and reduced in isolation: to reduce WLTS to C it is sufficient to provide a reduction for each $\textnormal{{WLTS}}(A,M)$. Given any $A$ and $M$, let $\underline{A}$ and $\underline{M}$ be a non-empty set and a non-trivial abelian monoid with the property that ${\left|{\mathrm{car}\left({\operatorname{\nu}(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}}\right)}\right|}\leq{\left|{\mathrm{car}\left({\operatorname{\nu}(\mathcal{F}_{\mspace{-1.0mu}\underline{M}}-)^{\underline{A}}}\right)}\right|}$ and $\textnormal{{WLTS}}(\underline{A},\underline{M})\preccurlyeq\textnormal{{C}}$. Existence of $\underline{A}$ and $\underline{M}$ follows from hypothesis on C and Lemma 6: if ${\left|M\right|}^{\max(\aleph_{0},{\left|A\right|})}$ is taken as $\kappa$ then it holds that:

[TABLE]

It follows from Theorem 5 and hypothesis on $\underline{A}$ and $\underline{M}$ that $\textnormal{{WLTS}}(A,M)\preccurlyeq\textnormal{{WLTS}}(\underline{A},\underline{M})\preccurlyeq\textnormal{{C}}$ proving that any subcategory $\textnormal{{WLTS}}(A,M)$ of WLTS reduces to C and hence that $\textnormal{{WLTS}}\preccurlyeq\textnormal{{C}}$. ∎

Neither Theorem 7 nor Theorem 9 distinguish between the contribution of labels and weights. Instead, both require that any small cardinal is covered by the combined size of labels and weights. This situation points to a trade-off between labels and weights: it is possible to shift information and complexity between the two parameters defining WLTSs behaviours while preserving their semantics in terms of quantitative bisimulation. At one end of this trade-off all information is shifted into labels and weights are drawn from the smallest non-trivial abelian monoid which is (up-to isomorphism) the monoid $\mathbb{B}$ of boolean values under disjunction. Systems weighted over $\mathbb{B}$ are LTSs.

Corollary 10**.**

$\textnormal{{WLTS}}\approxeq\textnormal{{LTS}}$.

At the other end of the trade-off all information is expressed using weights only. These systems have exactly one label which means that they are essentially “unlabelled”. We write WTS for the subcategory of WLTS formed by “unlabelled” weighted transition systems.

Corollary 11**.**

$\textnormal{{WLTS}}\approxeq\textnormal{{WTS}}$.

Actually, a result stronger than that stated in Corollary 11 holds: there is a full reduction.

Theorem 12**.**

$\textnormal{{WLTS}}\mathrel{\dot{\approxeq}}\textnormal{{WTS}}$.

Proof.

For $(M,+,0)$ an abelian monoid and $A$ a set, the function space $M^{A}$ carries an abelian monoid structure given by an $A$-indexed product of monoids. In particular, the monoidal zero is the $A$-indexed tuple:

[TABLE]

and monoidal sum is defined on each $\vv{m}$ and $\vv{n}$ as:

[TABLE]

There is a natural isomorphism $\mu\colon(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}\cong\mathcal{F}_{\mspace{-1.0mu}M^{A}}$ given on each set $X$ as:

[TABLE]

and

[TABLE]

Since this natural transformation is component-wise injective, it follows from [15, Thm. 3] that there is a full reduction $\hat{\mu}\colon\textnormal{{WLTS}}(A,M)\to\textnormal{{WLTS}}(1,M^{A})$ given on each system $\alpha$ as:

[TABLE]

and each homomorphism $f\colon\alpha\to\beta$ as follows:

[TABLE]

5 Reducing state-to-function transition systems, again

In [15, 17, Sec. 6] we proved that the category of FuTSs reduces to that of WLTSs by defining a suitable reduction. An explicit reduction offered us a bridge for deriving logical characterisations of bisimulations for these systems [17, Sec. 8] but this may not be necessary in general. In this section we present an alternative (and shorter) proof based on the results we introduced in Section 3.2. In this way, we are also able to validate the technique rediscovering known reductions.

Recall from Section 3.2 that to prove existence of reductions using Theorem 5 it suffices to provide an upper bound for the size of final systems for the source type (here FuTSs) and a lower bound for the size of final systems for the target type (here WLTSs).

Lemma 13**.**

There are final $\operatorname{\nu}(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}}$-systems and it holds that:

[TABLE]

Proof.

For any non-trivial abelian monoid $M$, set $X$ and small cardinal $\kappa>\aleph_{0}$ it holds that:

[TABLE]

In fact, if $\max\left({\left|M\right|},{\left|X\right|}\right)\leq\kappa$ then,

[TABLE]

Write $F\colon\textnormal{{Ord}}\to\textnormal{{Set}}$ for the final sequence of the endofunctor $(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}}$ and $\mu$ for the cardinal number $\max_{M\in\vv{M}}({\left|M\right|})^{\max_{A\in\vv{A}}(\aleph_{0},{\left|A\right|})}$. The proof proceeds by showing that ${\left|F_{\alpha}\right|}\leq\mu$ for any ordinal $\alpha$. Observe that like $(\mathcal{F}_{\mspace{-1.0mu}M}-)^{A}$, also the final sequence for $(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}}$ stabilises in $\omega+\omega$ and that all actions after $\omega$ are injections. It suffices to prove that ${\left|F_{\alpha}\right|}\leq\mu$ for any $\alpha\leq\omega$. Let $\alpha$ be [math]. By definition of $F$ it holds that ${\left|F_{0}\right|}=1<\mu$. Let $\alpha$ be a finite successor ordinal $\beta+1$. It follows from the inductive hypothesis, the implication above, and definition of $F_{\beta+1}$ that:

[TABLE]

Let $\alpha$ be $\omega$. From definition of $F$ on limit ordinals and the inductive hypothesis it holds that:

[TABLE]

Therefore, every set in the final sequence for the endofunctor $(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}}$ is of cardinality less or equal to $\mu=\max_{M\in\vv{M}}({\left|M\right|})^{\max_{A\in\vv{A}}(\aleph_{0},{\left|A\right|})}$, especially the carrier of $\operatorname{\nu}(\mathcal{F}_{\mspace{-1.0mu}\vv{M}}-)^{\vv{A}}$. ∎

The category of FuTSs reduces to that of WLTSs.

Theorem 14**.**

$\textnormal{{FuTS}}\approxeq\textnormal{{WLTS}}$.

Proof.

Let $\vv{A}$ and $\vv{M}$ be sequences of labels and monoids from a type modelling FuTSs. It follows from Lemma 13 that there is a non-empty set $\underline{A}$ and a non-trivial abelian monoid $\underline{M}$ such that:

[TABLE]

Recall from Lemma 6 that $\max(\underline{M},\underline{A})$ is a lower bound to the size of final $(\mathcal{F}_{\mspace{-1.0mu}\underline{M}}-)^{\underline{A}}\mspace{1.0mu}$-systems, then $\textnormal{{FuTS}}(\vv{A},\vv{M})\preccurlyeq\textnormal{{WLTS}}(\underline{A},\underline{M})$ by Theorem 5. From the fact that every subcategory $\textnormal{{FuTS}}(\vv{A},\vv{M})$ of FuTS reduces to some subcategory $\textnormal{{WLTS}}(\underline{A},\underline{M})$ of WLTS it follows that $\textnormal{{FuTS}}\preccurlyeq\textnormal{{WLTS}}$. ∎

6 Conclusions and final remarks

In this paper we studied the category of weighted labelled transitions systems under the lens of reductions in order to understand their expressiveness in terms of quantitative bisimulation. We proved that there is no instance of the WLTS model that is “universal”: it is not possible to faithfully express all behaviours modelled as WLTSs using a single set of labels and a single monoid of weights (Corollary 8). In fact, we proved that the expressiveness of these models depends on combined size of their sets of labels and weights (the parameters of WLTSs models) which can be arbitrarily large sets but not proper classes (Theorem 7). Given that the dependency is on the combined size, we then proved that it is indeed possible to freely distribute the contribution between labels and weights while preserving the model expressiveness in terms of quantitative bisimulation (Theorem 9). At the two ends of this trade-off between labels and weights there are the categories of LTSs and of WTSs (or unlabelled WLTSs) where the information is completely shifted to labels or to weights, respectively (Corollaries 10 and 11).

To obtain these results, we extended the framework of reductions with new results relating the existence of reductions to properties of final coalgebras. In particular, we proved that reductions exist if and only if the target type has at least as many abstract behaviours as the source type. As a consequence, even a rough estimate of the final coalgebra size suffices to prove or disprove the existence of a reduction. As an application, in Section 5 we provided a shorter proof of a known result: that the category of FuTSs reduces to that of WLTSs.

Besides the classification interest, results presented in this work are of relevance to the extension of these theories of models. In fact, reductions pave the way for porting existing and new results between categories of transition systems. For instance, in [17] reductions are used to derive new Hennessy-Milner-style modal logics for transition systems and guarantee an important property of such logics called full-abstraction (or expressiveness) \ietheir ability to characterise bisimilarity.

In this (and previous works [15, 17]) we focused on strong bisimulation; a natural direction to pursue is to consider different behavioural equivalences, like trace equivalence or weak bisimulation. We remark that, as shown in [6, 3, 4, 19], in order to deal with these and similar equivalences, endofunctors need to be endowed with a monad (sub)structure; although WLTSs are covered in [13, 3], an analogous account of ULTraSs and FuTSs is still an open problem.

Acknowledgements

This work was supported by the CRC project, grant no. DFF–4005-00304 from the Danish Council for Independent Research, and by the Open Data Framework project at the University of Southern Denmark.