\EventEditors

Serge Haddad and Daniele Varacca \EventNoEds2 \EventLongTitle32nd International Conference on Concurrency Theory (CONCUR 2021) \EventShortTitleCONCUR 2021 \EventAcronymCONCUR \EventYear2021 \EventDateAugust 23–27, 2021 \EventLocationVirtual Conference \EventLogo \SeriesVolume203 \ArticleNo32 stix@largesymbols"0E stix@largesymbols"0F Radboud University, Nijmegen, The Netherlands [email protected]://orcid.org/0000-0001-8993-6486Work forms part of the NWO TOP project 612.001.852 and the DFG-funded project COAX (MI 717/5-2) Friedrich-Alexander-Universität Erlangen-Nürnberg, [email protected]://orcid.org/0000-0002-2021-1644 Work forms part of the DFG-funded project CoMoC (MI 717/7-1) Friedrich-Alexander-Universität Erlangen-Nürnberg, [email protected]://orcid.org/0000-0002-3146-5906Work forms part of the DFG-funded project CoMoC (SCHR 1118/15-1) \CopyrightT. Wißmann, S. Milius, and L. Schröder \relatedversion \relatedversiondetailsFull Version with Appendixhttps://arxiv.org/abs/2105.00669 {CCSXML} <ccs2012> <concept> <concept_id>10003752.10003790</concept_id> <concept_desc>Theory of computation Logic</concept_desc> <concept_significance>500</concept_significance> </concept> </ccs2012> \ccsdesc[500]Theory of computation Logic {CCSXML} <ccs2012> <concept> <concept_id>10003752.10010124.10010138.10010143</concept_id> <concept_desc>Theory of computation Program analysis</concept_desc> <concept_significance>500</concept_significance> </concept> </ccs2012> \ccsdesc[500]Theory of computation Program analysis

Explaining Behavioural Inequivalence Generically
in Quasilinear Time

Thorsten Wißmann Stefan Milius Lutz Schröder

Abstract

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time $\mathcal{O}((m+n)\log n)$ on systems with $n$ states and $m$ transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was $\mathcal{O}(mn)$ .

keywords:

bisimulation, partition refinement, modal logic, distinguishing formulae, coalgebra

1 Introduction

For finite transition systems, the Hennessy-Milner theorem guarantees that two states are bisimilar if and only if they satisfy the same modal formulae. This implies that whenever two states are not bisimilar, then one can find a modal formula that holds at one of the states but not at the other. Such a formula explains the difference of the two states’ behaviour and is thus usually called a distinguishing formula [13]. For example, in the transition system in Figure 2, the formula $\Box\Diamond\top$ distinguishes the states $x$ and $y$ because $x$ satisfies $\Box\Diamond\top$ whereas $y$ does not. Given two states in a finite transition system with $n$ states and $m$ transitions, the algorithm by Cleaveland [13] computes a distinguishing formula in time $\mathcal{O}(mn)$ . The algorithm builds on the Kanellakis-Smolka partition refinement algorithm [28, 29], which computes the bisimilarity relation on a transition system within the same time bound.

Figure 1: Example of a transition system

Figure 2: Example of a Markov chain

Similar logical characterizations of bisimulation exist for other system types. For instance, Desharnais et al. [16, 17] characterize probabilistic bisimulation on (labelled) Markov chains, in the sense of Larsen and Skou [33] (for each label, every state has either no successors or a probability distribution on successors). In their logic, a formula $\Diamond_{\geq p}\phi$ holds at states that have a transition probability of at least $p$ to states satisfying $\phi$ . For example, the state $x$ in Figure 2 satisfies $\Diamond_{\geq 0.5}\Diamond_{\geq 1}\top$ but $y$ does not. Desharnais et al. provide an algorithm that computes distinguishing formulae for labelled Markov chains in run time (roughly) $\mathcal{O}(n^{4})$ .

In the present work, we construct such counterexamples generically for a variety of system types. We achieve genericity over the system type by modelling state-based systems as coalgebras for a set functor in the framework of universal coalgebra [40]. Examples of coalgebras for a set functor include transition systems, deterministic automata, or weighted systems (e.g. Markov chains). Universal coalgebra provides a generic notion of behavioural equivalence that instantiates to standard notions for concrete system types, e.g. bisimilarity (transtion systems), language equivalence (deterministic automata), or probabilistic bisimilarity (Markov chains). Moreover, coalgebras come equipped with a generic notion of modal logic that is parametric in a choice of modalities whose semantics is constructed so as to guarantee invariance w.r.t. behavioural equivalence; under easily checked conditions, such a coalgebraic modal logic in fact characterizes behavioural equivalence in the same sense as Hennessy-Milner logic characterizes bisimilarity [39, 42]. Hence, as soon as suitable modal operators are found, coalgebraic modal formulae serve as distinguishing formulae.

In a nutshell, the contribution of the present paper is an algorithm that computes distinguishing formulae for behaviourally inequivalent states in quasilinear time, and in fact certificates that uniquely describe behavioural equivalence classes in a system, in coalgebraic generality. We build on an existing efficient coalgebraic partition refinement algorithm [46], thus achieving run time $\mathcal{O}(m\log n)$ on coalgebras with $n$ states and $m$ transitions (in a suitable encoding). The dag size of formulae is also $\mathcal{O}(m\log n)$ (for tree size, exponential lower bounds are known [22]); even for labelled transition systems, we thus improve the previous best bound $\mathcal{O}(mn)$ [13] for both run time and formula size. We systematically extract the requisite modalities from the functor at hand, requiring binary and nullary modalities in the general case, and then give a systematic method to translate these generic modal operators into more customary ones (such as the standard operators of Hennessy-Milner logic).

We subsequently identify a notion of cancellative functor that allows for additional optimization. E.g. functors modelling weighted systems are cancellative if and only if the weights come from a cancellative monoid, such as $(\mathbb{Z},+)$ , or $(\mathbb{R},+)$ as used in probabilistic systems. For cancellative functors, much simpler distinguishing formulae can be constructed: the binary modalities can be replaced by unary ones, and only conjunction is needed in the propositional base. On labelled Markov chains, this complements the result that a logic with only conjunction and different unary modalities (mentioned above) suffices for the construction of distinguishing formulae (but not certificates) [17] (see also [19]).

Related Work

Cleaveland’s algorithm [13] for labelled transition systems is is based on Kanellakis and Smolka’s partition refinement algorithm [29]. The coalgebraic partition refinement algorithm we employ [46] is instead related to the more efficient Paige-Tarjan algorithm [36]. König et al. [32] extract formulae from winning strategies in a bisimulation game in coalgebraic generality; their algorithm runs in $\mathcal{O}(n^{4})$ and does not support negative transition weights. Characteristic formulae for behavioural equivalence classes taken across all models require the use of fixpoint logics [21]. The mentioned algorithm by Desharnais et al. for distinguishing formulae on labelled Markov processes [17, Fig. 4] is based on Cleaveland’s. No complexity analysis is made but the algorithm has four nested loops, so its run time is roughly $\mathcal{O}(n^{4})$ . Bernardo and Miculan [10] provide a similar algorithm for a logic with only disjunction. There are further generalizations along other axes, e.g. to behavioural preorders [12]. The TwoTowers tool set for the analysis of stochastic process algebras [9, 8] computes distinguishing formulae for inequivalent processes, using variants of Cleaveland’s algorithm. Some approaches construct alternative forms of certificates for inequivalence, such as Cranen et al.’s notion of evidence [14] or methods employed on business process models, based on model differences and event structures [18, 6, 5].

2 Preliminaries

We first recall some basic notation. We denote by $0=\emptyset$ , $1=\{0\}$ , $2=\{0,1\}$ and $3=\{0,1,2\}$ the sets representing the natural numbers $0$ , $1$ , $2$ and $3$ . For every set $X$ , there is a unique map $!\colon X\to 1$ . We write $Y^{X}$ for the set of functions $X\to Y$ , so e.g. $X^{2}\cong X\times X$ . In particular, $2^{X}$ is the set of $2$ -valued predicates on $X$ , which is in bijection with the powerset $\mathcal{P}X$ of $X$ , i.e. the set of all subsets of $X$ ; in this bijection, a subset $A\in\mathcal{P}X$ corresponds to its characteristic function $\chi_{A}\in 2^{X}$ , given by $\chi_{A}(x)=1$ if $x\in A$ , and $\chi(x)=0$ otherwise. We generally indicate injective maps by $\rightarrowtail$ . Given maps $f\colon Z\to X$ , $g\colon Z\to Y$ , we write $\langle f,g\rangle$ for the map $Z\to X\times Y$ given by $\langle f,g\rangle(z)=(f(z),g(z))$ . We denote the disjoint union of sets $X$ , $Y$ by $X+Y$ , with canonical inclusion maps $\mathsf{in}_{1}\colon X\rightarrowtail X+Y$ and $\mathsf{in}_{2}\colon Y\rightarrowtail X+Y$ . More generally, we write $\coprod_{i\in I}X_{i}$ for the disjoint union of an $I$ -indexed family of sets $(X_{i})_{i\in I}$ , and $\mathsf{in}_{i}\colon X_{i}\rightarrowtail\coprod_{i\in I}X_{i}$ for the $i$ -th inclusion map. For a map $f\colon X\to Y$ (not necessarily surjective), we denote by $\ker(f)\subseteq X\times X$ the kernel of $f$ , i.e. the equivalence relation

\ker(f):=\{(x,x^{\prime})\in X\times X\mid f(x)=f(x^{\prime})\}.

(1)

Notation \thetheorem (Partitions).

Given an equivalence relation $R$ on $X$ , we write $[x]_{R}$ for the equivalence class $\{x^{\prime}\in X\mid(x,x^{\prime})\in R\}$ of $x\in X$ . If $R$ is the kernel of a map $f$ , we simply write $[x]_{f}$ in lieu of $[x]_{\ker(f)}$ . The intersection $R\cap S$ of equivalence relations is again an equivalence relation. The partition corresponding to $R$ is denoted by $X/R=\{[x]_{R}\mid x\in X\}$ . Note that $[-]_{R}\colon X\to X/R$ is a surjective map and that $R=\ker([-]_{R})$ .

A signature is a set $\Sigma$ , whose elements are called operation symbols, equipped with a function $a\colon\Sigma\to\mathbb{N}$ assigning to each operation symbol its arity. We write $\mathord{\raisebox{1.0pt}{$\sigma$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Sigma$ for $\sigma\in\Sigma$ with $a(\sigma)=n$ . We will apply the same terminology and notation to collections of modal operators.

2.1 Coalgebra

Universal coalgebra [40] provides a generic framework for the modelling and analysis of state-based systems. Its key abstraction is to parametrize notions and results over the transition type of systems, encapsulated as an endofunctor on a given base category. Instances cover, for example, deterministic automata, labelled (weighted) transition systems, and Markov chains.

Definition \thetheorem.

A set functor $F\colon\mathsf{Set}\to\mathsf{Set}$ assigns to every set $X$ a set $FX$ and to every map $f\colon X\to Y$ a map $Ff\colon FX\to FY$ such that identity maps and composition are preserved: $F\mathsf{id}_{X}=\mathsf{id}_{FX}$ and $F(g\cdot f)=Fg\cdot Ff$ . An $F$ -coalgebra is a pair $(C,c)$ consisting of a set $C$ (the carrier) and a map $c\colon C\to FC$ (the structure). When $F$ is clear from the context, we simply speak of a coalgebra.

In a coalgebra $c\colon C\to FC$ , we understand the carrier set $C$ as consisting of states, and the structure $c$ as assigning to each state $x\in C$ a structured collection of successor states, with the structure of collections determined by $F$ . In this way, the notion of coalgebra subsumes numerous types of state-based systems, as illustrated next.

Example \thetheorem.

1.

The powerset functor $\mathcal{P}$ sends a set $X$ to its powerset $\mathcal{P}X$ and a map $f\colon X\to Y$ to the map $\mathcal{P}f=f[-]\colon\mathcal{P}X\to\mathcal{P}Y$ taking direct images. A $\mathcal{P}$ -coalgebra $c\colon C\to\mathcal{P}C$ is precisely a transition system: It assigns to every state $x\in C$ a set $c(x)\in\mathcal{P}C$ of successor states, inducing a transition relation $\to$ given by $x\to y$ iff $y\in c(x)$ . Similarly, coalgebras for the finite powerset functor ${\mathcal{P}_{\textsf{f}}}$ (with ${\mathcal{P}_{\textsf{f}}}X$ being the set of finite subsets of $X$ ) are finitely branching transition systems.
2.

Coalgebras for the functor $FX=2\times X^{A}$ , where $A$ is a fixed input alphabet, are deterministic automata (without an explicit initial state). Indeed, a coalgebra structure $c=\langle f,t\rangle\colon C\to 2\times C^{A}$ consists of a finality predicate $f\colon C\to 2$ and a transition map $C\times A\to C$ in curried form $t\colon C\to C^{A}$ .
3.

Every signature $\Sigma$ defines a signature functor that maps a set $X$ to the set

$\textstyle T_{\Sigma}X=\coprod_{\mathord{\raisebox{1.0pt}{$\scriptstyle\sigma$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$\scriptstyle n$}}}\in\Sigma}X^{n},$

whose elements we may understand as flat $\Sigma$ -terms $\sigma(x_{1},\ldots,x_{n})$ with variables from $X$ . The action of $T_{\Sigma}$ on maps $f\colon X\to Y$ is then given by $(T_{\Sigma}f)(\sigma(x_{1},\ldots,x_{n}))=\sigma(f(x_{1}),\ldots,$ $f(x_{n}))$ . For simplicity, we write $\sigma$ (instead of $\mathsf{in}_{\sigma}$ ) for the coproduct injections, and $\Sigma$ in lieu of $T_{\Sigma}$ for the signature functor. States in $\Sigma$ -coalgebras describe possibly infinite $\Sigma$ -trees.
4.

For a commutative monoid $(M,+,0)$ , the monoid-valued functor $M^{(-)}$ [25] is given by

$M^{(X)}:=\{\mu\colon X\to M\mid\text{$\mu(x)=0$ for all but finitely many $x\in X$}\}$ (2)

on sets $X$ ; for a map $f\colon X\to Y$ , the map $M^{(f)}\colon M^{(X)}\to M^{(Y)}$ is defined by

$(M^{(f)})(\mu)(y)=\textstyle\sum_{x\in X,f(x)=y}\mu(x).$

A coalgebra $c\colon C\to M^{(C)}$ is a finitely branching weighted transition system, where $c(x)(x^{\prime})\in M$ is the transition weight from $x$ to $x^{\prime}$ . For the Boolean monoid ${\mathbb{B}}=(2,\vee,0)$ , we recover ${\mathcal{P}_{\textsf{f}}}={\mathbb{B}}^{(-)}$ . Coalgebras for $\mathbb{R}^{(-)}$ , with $\mathbb{R}$ understood as the additive monoid of the reals, are $\mathbb{R}$ -weighted transition systems. The functor

$\textstyle{\mathcal{D}}X=\{\mu\in\mathbb{R}_{\geq 0}^{(X)}\mid\sum_{x\in X}\mu(x)=1\},$

which assigns to a set $X$ the set of all finite probability distributions on $X$ (represented as finitely supported probability mass functions), is a subfunctor of $\mathbb{R}^{(-)}$ .
5.

Functors can be composed; for instance, given a set $A$ of labels, the composite of $\mathcal{P}$ and the functor $A\times(-)$ (whose action on sets maps a set $X$ to the set $A\times X$ ) is the functor $FX=\mathcal{P}(A\times X)$ , whose coalgebras are $A$ -labelled transition systems. Coalgebras for $({\mathcal{D}}(-)+1)^{A}$ have been termed probabilistic transition systems [33] or labelled Markov chains [17], and coalgebras for $({\mathcal{D}}((-)+1)+1)^{A}$ are partial labelled Markov chains [17]. Coalgebras for $SX={\mathcal{P}_{\textsf{f}}}(A\times{\mathcal{D}}X)$ are variously known as simple Segala systems or Markov decision processes.

We have a canonical notion of behaviour on $F$ -coalgebras:

Definition \thetheorem.

An $F$ -coalgebra morphism $h\colon(C,c)\to(D,d)$ is a map $h\colon C\to D$ such that $d\cdot h=Fh\cdot c$ . States $x,y$ in an $F$ -coalgebra $(C,c)$ are behaviourally equivalent ( $x\sim y$ ) if there exists a coalgebra morphism $h$ such that $h(x)=h(y)$ .

Thus, we effectively define the behaviour of a state as those of its properties that are preserved by coalgebra morphisms. The notion of behavioural equivalence subsumes standard branching-time equivalences:

Example \thetheorem.

1.

For $F\in\{\mathcal{P},{\mathcal{P}_{\textsf{f}}}\}$ , behavioural equivalence on $F$ -coalgebras, i.e. on transition systems, is bisimilarity in the usual sense.
2.

For deterministic automata as coalgebras for $FX=2\times X^{A}$ , two states are behaviourally equivalent iff they accept the same formal language.
3.

For a signature functor $\Sigma$ , two states of a $\Sigma$ -coalgebra are behaviourally equivalent iff they describe the same $\Sigma$ -tree.
4.

For labelled transition systems as coalgebras for $FX=\mathcal{P}(A\times X)$ , coalgebraic behavioural equivalence precisely captures Milner’s strong bisimilarity [1].
5.

For weighted and probabilistic systems, coalgebraic behavioural equivalence instantiates to weighted and probabilistic bisimilarity, respectively [41, Cor. 4.7], [7, Thm. 4.2].

Remark \thetheorem.

1.

The notion of behavioural equivalence extends straightforwardly to states in different coalgebras, as one can canonically define the disjoint union of coalgebras.
2.

We may assume without loss of generality that a set functor $F$ preserves injective maps [43] (see also [2, 8.1.12–17]), that is, $Ff$ is injective whenever $f$ is.

2.2 Coalgebraic Logics

We briefly review basic concepts of coalgebraic modal logic [38, 42]. Coalgebraic modal logics are parametric in a functor $F$ determining the type of systems underlying the semantics, and additionally in a choice of modalities interpreted in terms of predicate liftings. For now, we use $F=\mathcal{P}$ as a basic example, deferring further examples to section 5.

Syntax

The syntax of coalgebraic modal logic is parametrized over the choice of signature $\Lambda$ of modal operators (with assigned arities). Then, formulae $\phi$ are generated by the grammar
${\hskip 14.22636pt}\phi_{1},\ldots,\phi_{n}::=\top\leavevmode\nobreak\ |\leavevmode\nobreak\ \neg\phi_{1}\leavevmode\nobreak\ |\leavevmode\nobreak\ \phi_{1}\wedge\phi_{2}\leavevmode\nobreak\ |\leavevmode\nobreak\ \heartsuit(\phi_{1},\ldots,\phi_{n})\qquad(\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Lambda).$

Example \thetheorem.

For $F=\mathcal{P}$ , one often takes $\Lambda=\{\mathord{\raisebox{1.0pt}{$\Diamond$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$1$}}}\}$ ; the induced syntax is that of (single-action) Hennessy-Milner logic. As usual, we write $\Box\phi:\equiv\neg\Diamond\neg\phi$ .

Semantics

We interpret formulae as sets of states in $F$ -coalgebras. This interpretation arises by assigning to each modal operator $\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Lambda$ an $n$ -ary predicate lifting $\llbracket\heartsuit\rrbracket$ [38, 42], i.e. a family of maps $\llbracket\heartsuit\rrbracket_{X}\colon(2^{X})^{n}\to 2^{FX}$ , one for every set $X$ , such that the naturality condition

Ff^{-1}\big{[}\llbracket\heartsuit\rrbracket_{Y}(P_{1},\ldots,P_{n})\big{]}=\llbracket\heartsuit\rrbracket_{X}(f^{-1}[P_{1}],\ldots,f^{-1}[P_{n}])

(3)

for all $f\colon X\to Y$ and all $P_{1},\ldots,P_{n}\in 2^{X}$ (for categorically-minded readers, $\llbracket\heartsuit\rrbracket$ is a natural transformation $(2^{(-)})^{n}\to 2^{F^{\mathsf{op}}}$ ); the idea being to lift given predicates on states to predicates on structured collections of states. Given these data, the extension of a formula $\phi$ in an $F$ -coalgebra $(C,c)$ is a predicate $\llbracket\phi\rrbracket_{(C,c)}$ , or just $\llbracket\phi\rrbracket$ , on $C$ , recursively defined by

	$\displaystyle\llbracket\top\rrbracket_{(C,c)}=C\qquad\llbracket\phi\wedge\psi\rrbracket_{(C,c)}=\llbracket\phi\rrbracket_{(C,c)}\cap\llbracket\psi\rrbracket_{(C,c)}\qquad\llbracket\neg\phi\rrbracket_{(C,c)}=C\setminus\llbracket\phi\rrbracket_{(C,c)}$
	$\displaystyle\llbracket\heartsuit(\phi_{1},\ldots,\phi_{n})\rrbracket_{(C,c)}=c^{-1}\big{[}\llbracket\heartsuit\rrbracket_{C}\big{(}\llbracket\phi_{1}\rrbracket_{(C,c)},\ldots,\llbracket\phi_{n}\rrbracket_{(C,c)}\big{)}\big{]}\qquad\text{($\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Lambda$)}$

(where we apply set operations to predicates with the evident meaning). We say that a state $x\in C$ satisfies $\phi$ if $\llbracket\phi\rrbracket(x)=1$ . Notice how the clause for modalities says that $x$ satisfies $\heartsuit(\phi_{1},\ldots,\phi_{n})$ iff $c(x)$ satisfies the predicate obtained by lifting the predicates $\llbracket\phi_{1}\rrbracket,\ldots,\llbracket\phi_{n}\rrbracket$ on $C$ to a predicate on $FC$ according to $\llbracket\heartsuit\rrbracket$ .

Example \thetheorem.

Over $F=\mathcal{P}$ , we interpret $\Diamond$ by the predicate lifting

\llbracket\Diamond\rrbracket_{X}\colon 2^{X}\to 2^{\mathcal{P}X},\quad P\mapsto\leavevmode\nobreak\ \{K\subseteq X\mid\exists x\in K\colon x\in P\}=\{K\subseteq X\mid K\cap P\neq\emptyset\},

The arising notion of satisfaction over $\mathcal{P}$ -coalgebras $(C,c)$ is precisely the standard one: $x\in\llbracket\Diamond\phi\rrbracket_{(C,c)}$ iff $y\in\llbracket\phi\rrbracket_{(C,c)}$ for some transition $x\to y$ .

The naturality condition (3) of predicate liftings guarantees invariance of the logic under coalgebra morphisms, and hence under behavioural equivalence:

Proposition 2.1 (Adequacy [38, 42]).

Behaviourally equivalent states satisfy the same formulae: $x\sim y$ implies that for all formulae $\phi$ , we have $x\in\llbracket\phi\rrbracket$ iff $y\in\llbracket\phi\rrbracket$ .

In our running example $F=\mathcal{P}$ , this instantiates to the well-known fact that modal formulae are bisimulation-invariant, that is, bisimilar states in transition systems satisfy the same formulae of Hennessy-Milner logic.

3 Constructing Distinguishing Formulae

A proof method certifying behavioural equivalence of states $x,y$ in a coalgebra is immediate by definition: One simply needs to exhibit a coalgebra morphism $h$ such that $h(x)=h(y)$ . In fact, for many system types, it suffices to relate $x$ and $y$ by a coalgebraic bisimulation in a suitable sense (e.g. [1, 40, 24, 34]), generalizing the Park-Milner bisimulation principle [35, 37]. It is less obvious how to certify behavioural inequivalence $x\not\sim y$ , showing that such a morphism $h$ does not exist. By 2.1, one option is to exhibit a (coalgebraic) modal formula $\phi$ that is satisfied by $x$ but not by $y$ . In the case of (image-finite) transition systems, such a formula is guaranteed to exist by the Hennessy-Milner theorem, which moreover is known to generalize to coalgebras [39, 42]. More generally, we consider separation of sets of states by formulae, following Cleaveland [13, Def. 2.4]:

Definition 1.

Let $(C,c)$ be an $F$ -coalgebra. A formula $\phi$ distinguishes a set $X\subseteq C$ from a set $Y\subseteq C$ if $X\subseteq\llbracket\phi\rrbracket$ and $Y\cap\llbracket\phi\rrbracket=\emptyset$ . In case $X=\{x\}$ and $Y=\{y\}$ , we just say that $\phi$ distinguishes $x$ from $y$ . We say that $\phi$ is a certificate of $X$ if $\phi$ distinguishes $X$ from $C\setminus X$ , that is if $\llbracket\phi\rrbracket=X$ .

Note that $\phi$ distinguishes $X$ from $Y$ iff $\neg\phi$ distinguishes $Y$ from $X$ . Certificates have also been referred to as descriptions [22]. If $\phi$ is a certificate of a behavioural equivalence class $[x]_{\sim}$ , then by definition $\phi$ distinguishes $x$ from $y$ whenever $x\not\sim y$ . To obtain distinguishing formulae for behaviourally inequivalent states in a coalgebra, it thus suffices to construct certificates for all behavioural equivalence classes, and our algorithm does just that. Of course, every certificate must be at least as large as a smallest distinguishing formula. However, already on transition systems, distinguishing formulae and certificates have the same asymptotic worst-case size (cf. section 6).

A natural approach to computing certificates for behavioural equivalence classes is to extend algorithms that compute these equivalence classes. In particular, partition refinement algorithms compute a sequence $C/R_{0},C/R_{1},\ldots$ of consecutively finer partitions (i.e. $R_{i+1}\subseteq R_{i}$ ) on the state space, where every block $B\in C/R_{i}$ is a union of behavioural equivalence classes, and the final partition is precisely $C/\mathord{\sim}$ . Indeed, Cleaveland’s algorithm for computing certificates on labelled transition systems [13] correspondingly extends Kanellakis and Smolka’s partition refinement algorithm [28, 29], which runs in $\mathcal{O}(mn)$ on systems with $n=|C|$ states and $m$ transitions. Our generic algorithm will be based on a more efficient partition refinement algorithm.

3.1 Paige-Tarjan with Certificates

Before we turn to constructing certificates in coalgebraic generality, we informally recall and extend the Paige-Tarjan algorithm [36], which computes the partition modulo bisimilarity of a given transition system with $n$ states and $m$ transitions in time $\mathcal{O}((m+n)\log n)$ . We fix a given finite transition system, viewed as a $\mathcal{P}$ -coalgebra $c\colon C\to\mathcal{P}C$ .

The algorithm computes two sequences $(C/P_{i})_{i\in\mathbb{N}}$ and $(C/Q_{i})_{i\in\mathbb{N}}$ of partitions of $C$ (with $Q_{i},P_{i}$ equivalence relations), where only the most recent partition is held in memory and $i$ indexes the iterations of the main loop. Throughout the execution, $C/P_{i}$ is finer than $C/Q_{i}$ (that is, $P_{i}\subseteq Q_{i}$ for all $i$ ), and the algorithm terminates when $P_{i}=Q_{i}$ . Intuitively, $P_{i}$ is ‘one transition ahead’ of $Q_{i}$ : if $Q_{i}$ distinguishes states $x$ and $y$ , then $P_{i}$ is based on distinguishing transitions to $x$ from transitions to $y$ .

Initially, $C/Q_{0}:=\{C\}$ consists of only one block and $C/P_{0}$ of two blocks: the live states and the deadlocks (i.e. states with no outgoing transitions). If $P_{i}\subsetneqq Q_{i}$ , then there is a block $B\in C/Q_{i}$ that is the union of at least two blocks in $C/P_{i}$ . In such a situation, the algorithm chooses $S\subseteq B$ in $C/P_{i}$ to have at most half the size of $B$ and then splits the block $B$ into $S$ and $B\setminus S$ in the partition $C/Q_{i}$ :

C/Q_{i+1}=(C/Q_{i}\setminus\{B\})\leavevmode\nobreak\ \cup\leavevmode\nobreak\ \{S,B\setminus S\}.

This is correct because every state in $S$ is already known to be behaviourally inequivalent to every state in $B\setminus S$ . By the definition of bisimilarity, this implies that every block $T\in C/P_{i}$ with some transition to $B$ may contain behaviourally inequivalent states as illustrated in Figure 3; that is, $T$ may need to be split into smaller blocks, as follows:

(C1)

states in $T$ with successors in $S$ but not in $B\setminus S$ (e.g. $x_{1}$ in Figure 3),
(C2)

states in $T$ with successors in $S$ and $B\setminus S$ (e.g. $x_{2}$ ), and
(C3)

states in $T$ with successors $B\setminus S$ but not in $S$ (e.g. $x_{3}$ ).

Figure 3: The refinement step as illustrated in [46, Figure 6].

The partition $C/P_{i+1}$ arises from $C/P_{i}$ by splitting all such predecessor blocks $T$ of $B$ accordingly. If no such $T$ is properly split, then $P_{i+1}=Q_{i+1}$ , and the algorithm terminates. It is straightforward to construct certificates for the blocks arising during the execution:

•

The certificate for the only block $C\in C/Q_{0}$ is $\top$ , and the blocks for live states and deadlocks in $C/P_{0}$ have certificates $\Diamond\top$ and $\neg\Diamond\top$ , respectively.

•

In the refinement step, suppose that $\delta,\beta$ are certificates of $S\in C/P_{i}$ and $B\in C/Q_{i}$ , respectively, where $S\subsetneqq B$ . For every predecessor block $T$ of $B$ , the three blocks obtained by splitting $T$ are distinguished (see 1) as follows:

(C1)

\neg\Diamond(\beta\wedge\neg\delta)

, (C2)

\Diamond(\delta)\wedge\Diamond(\beta\wedge\neg\delta)

, (C3)

\neg\Diamond\delta

(4)

Of course these formulae only distinguish the states in $T$ from each other (e.g. there may be states in other blocks with transitions to both $S$ and $B$ ). Hence, given a certificate $\phi$ of $T$ , one obtains certificates of the three resulting blocks in $C/P_{i+1}$ via conjunction: $\phi\wedge\neg\Diamond(\beta\wedge\neg\delta)$ , etc.

Upon termination, every bisimilarity class $[x]_{\sim}$ in the transition system is annotated with a certificate. A key step in the generic development will be to come up with a coalgebraic generalization of the formulae for (C1)–(C3).

3.2 Generic Partition Refinement

The Paige-Tarjan algorithm has been adapted to other system types, e.g. weighted systems [44], and it has recently been generalized to coalgebras [46, 20]. A crucial step in this generalization is to rephrase the case distinction (C1)–(C3) in terms of the functor $\mathcal{P}$ : Given a predecessor block $T$ in $C/P_{i}$ for $S\subsetneqq B\in C/Q_{i}$ , the three cases distinguish between the equivalence classes $[x]_{\mathcal{P}\chi_{S}^{B}\cdot c}$ for $x\in T$ , where the map $\chi_{S}^{B}\colon C\to 3$ in the composite $\mathcal{P}\chi_{S}^{B}\cdot c\colon C\to\mathcal{P}3$ is defined by

\chi_{S}^{B}\colon C\to 3\qquad\chi_{S}^{B}(x)=\begin{cases}2&\text{if $x\in S$},\\ 1&\text{if $x\in B\setminus S$},\\ 0&\text{if $x\in C\setminus B$},\end{cases}\qquad\text{for sets $S\subseteq B\subseteq C$}.

(5)

Every case is a possible value of $t:=\mathcal{P}\chi_{S}^{B}(c(x))\in\mathcal{P}3$ : (C1) $2\in t\not\mkern 1.0mu\ni 1$ , (C2) $2\in t\ni 1$ , and (C3) $2\notin t\ni 1$ . Since $T$ is a predecessor block of $B$ , the ‘fourth case’ $2\not\in t\not\mkern 1.0mu\ni 1$ is not possible. There is a transition from $x$ to some state outside of $B$ iff $0\in t$ . However, because of the previous refinement steps performed by the algorithm, either all or no states states of $T$ have an edge to $C\setminus B$ (a property called stability [36]), hence no distinction on $0\in t$ is necessary.

It is now easy to generalize from transition systems to coalgebras by simply replacing the functor $\mathcal{P}$ with $F$ in the refinement step. We recall the algorithm:

Algorithm 3.1 ([46, Alg. 4.9, (5.1)]).

Given a coalgebra $c\colon C\to FC$ , put

C/Q_{0}:=\{C\}\qquad\text{and}\qquad P_{0}:=\ker(C\xrightarrow{c}{FC}\xrightarrow{F!}F1).

Starting at iteration $i=0$ , repeat the following while $P_{i}\neq Q_{i}$ :

(A1)

Pick $S\in C/P_{i}$ and $B\in C/Q_{i}$ such that $S\subsetneqq B$ and $2\cdot|S|\leq|B|$
(A2)

$C/Q_{i+1}:=(C/Q_{i}\setminus\{B\})\cup\{S,B\setminus S\}$
(A3)

$P_{i+1}:=P_{i}\cap\ker(\leavevmode\hbox to130.11pt{\vbox to15.73pt{\pgfpicture\makeatletter\hbox{\hskip 65.057pt\lower-8.65137pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-65.057pt}{-7.07637pt}\pgfsys@invoke{ }\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip 8.23679pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.93124pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${C}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 8.23679pt\hfil&\hfil\hskip 41.83704pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.84097pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${FC}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 12.14651pt\hfil&\hfil\hskip 48.94162pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.40973pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${F3}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip 10.71527pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-48.38344pt}{-4.57637pt}\pgfsys@lineto{-19.49287pt}{-4.57637pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.2929pt}{-4.57637pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@rect{-36.2528pt}{-7.08331pt}{5.02927pt}{5.01389pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.2528pt}{-6.08331pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{c}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{5.60011pt}{-4.57637pt}\pgfsys@lineto{43.0265pt}{-4.57637pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{43.22649pt}{-4.57637pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@rect{17.2449pt}{-8.65137pt}{14.53677pt}{8.15pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.2449pt}{-6.2847pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{F\chi_{S}^{B}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

This algorithm formalizes the intuitive steps from subsection 3.1. Again, two sequences of partitions $P_{1}$ , $Q_{i}$ are constructed, and $P_{i}=Q_{i}$ upon termination. Initially, $Q_{0}$ identifies all states and $P_{0}$ distinguishes states by only their output behaviour; e.g. for $F=\mathcal{P}$ and $x\in C$ , the value $\mathcal{P}!(c(x))\in\mathcal{P}1$ is $\emptyset$ if $x$ is a deadlock, and $\{1\}$ if $x$ is a live state, and for $FX=2\times X^{A}$ , the value $F1(c(x))\in F1=2\times 1^{A}\cong 2$ indicates whether $x$ is a final or non-final state.

In the main loop, blocks $S\in C/P_{i}$ and $B\in C/Q_{i}$ witnessing $P_{i}\subsetneqq Q_{i}$ are picked, and $B$ is split into $S$ and $B\setminus S$ , like in the Paige-Tarjan algorithm. Note that step (A2) is equivalent to directly defining the equivalence relation $Q_{i+1}$ as

Q_{i+1}:=Q_{i}\cap\ker{\chi_{S}^{B}}.

A similar intersection of equivalence relations is performed in step (A3). The intersection splits every block $T\in C/P_{i}$ into smaller blocks such that $x,x^{\prime}\in T$ end up in the same block iff $F\chi_{S}^{B}(c(x))=F\chi_{S}^{B}(c(x^{\prime}))$ , i.e. $T$ is replaced by $\{[x]_{F\chi_{S}^{B}(c(x))}\mid x\in T\}$ . Again, this corresponds to the distinction of the three cases (C1)–(C3). For example, for $FX=2\times X^{A}$ , there are $|F3|=2\cdot 3^{|A|}$ cases to be distinguished, and so every $T\in C/P_{i}$ is split into at most that many blocks.

The following property of $F$ is needed for correctness [46, Ex. 5.11].

Definition 2 ([46]).

A functor $F$ is zippable if map

\langle F(A+!),F(!+B)\rangle\colon\leavevmode\nobreak\ F(A+B)\longrightarrow F(A+1)\times F(1+B)

is injective for all sets $A,B$ .

Intuitively, $t\in F(A+B)$ is a term in variables from $A$ and $B$ . If $F$ is zippable, then $t$ is uniquely determined by the two elements in $F(A+1)$ and $F(1+B)$ obtained by identifying all $B$ - and all $A$ -variables with $0\in 1$ , respectively. E.g. $FX=X^{2}$ is zippable: $t=(\mathsf{in}_{1}(a),\mathsf{in}_{2}(b))\in(A+B)^{2}$ is uniquely determined by $(\mathsf{in}_{1}(a),\mathsf{in}_{2}(0))\in(A+1)^{2}$ and $(\mathsf{in}_{1}(0),\mathsf{in}_{2}(b))\in(1+B)^{2}$ , and similarly for the three other cases of $t$ . In fact, all signature functors as well as $\mathcal{P}$ and all monoid-valued functors are zippable. Moreover, the class of zippable functors is closed under products, coproducts, and subfunctors but not under composition, e.g. $\mathcal{P}\mathcal{P}$ is not zippable [46].

Remark 3.

To apply the algorithm to coalgebras for composites $FG$ of zippable functors, e.g. $\mathcal{P}(A\times(-))$ , there is a reduction [46, Section 8] that embeds every $FG$ -coalgebra into a coalgebra for the zippable functor $(F+G)(X):=FX+GX$ . This reduction preserves and reflects behavioural equivalence, but introduces an intermediate state for every transition.

Theorem 3.2 ([46, Thm 4.20, 5.20]).

On a finite coalgebra $(C,c)$ for a zippable functor, 3.1 terminates after $i\leq|C|$ loop iterations, and the resulting partition identifies precisely the behaviourally equivalent states ( $P_{i}=\mathord{\sim}$ ).

3.3 Generic Modal Operators

The extended Paige-Tarjan algorithm (subsection 3.1) constructs a distinguishing formula according to the three cases (C1)–(C3). In the coalgebraic 3.1, these cases correspond to elements of $F3$ , which determine in which block an element of a predecessor block $T$ ends up. Indeed, the elements of $F3$ will also serve as generic modalities in characteristic formulae for blocks of states, essentially by the known equivalence between $n$ -ary predicate liftings and (in this case, singleton) subsets of $F(2^{n})$ [42] (termed tests by Klin [30]):

Definition 4.

The signature of $F3$ -modalities for a functor $F$ is

\Lambda=\{\mathord{\raisebox{1.0pt}{${\ulcorner t\urcorner}$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$2$}}}\mid t\in F3\};

that is, we write ${\ulcorner t\urcorner}$ for the syntactic representation of a binary modality for every $t\in F3$ . The interpretation of ${\ulcorner t\urcorner}$ for $F3$ is given by the predicate lifting

\llbracket{\ulcorner t\urcorner}\rrbracket\colon(2^{X})^{2}\to 2^{FX},\qquad\llbracket{\ulcorner t\urcorner}\rrbracket(S,B)=\{t^{\prime}\in FX\mid F\chi_{S\cap B}^{B}(t^{\prime})=t\}.

The intended use of ${\ulcorner t\urcorner}$ is as follows: Suppose a block $B$ is split into subblocks $S\subseteq B$ and $B\setminus S$ with certificates $\delta$ and $\beta$ , respectively: $\llbracket\delta\rrbracket=S$ and $\llbracket\beta\rrbracket=B$ . As in Figure 3, we then split every predecessor block $T$ of $B$ into smaller parts, each of which is uniquely characterized by the formula ${\ulcorner t\urcorner}(\delta,\beta)$ for some $t\in F3$ .

Example 3.3.

For $F=\mathcal{P}$ , ${\ulcorner{\{0,2\}}\urcorner}(\delta,\beta)$ is equivalent to $\smash{\overbrace{\Diamond\neg\beta}^{\text{\text{`0'}}}}\wedge\neg\smash{\overbrace{\Diamond(\beta\wedge\neg\delta)}^{\text{\text{`1'}}}}\wedge\smash{\overbrace{\Diamond(\delta\wedge\beta)}^{\text{\text{`2'}}}}$ .

Lemma 3.4.

Given an $F$ -coalgebra $(C,c)$ , $x\in C$ , and formulae $\delta$ and $\beta$ such that $\llbracket\delta\rrbracket\subseteq\llbracket\beta\rrbracket\subseteq C$ , we have $x\in\llbracket{\ulcorner t\urcorner}(\delta,\beta)\rrbracket$ if and only if $F\chi_{\llbracket\delta\rrbracket}^{\llbracket\beta\rrbracket}(c(x))=t$ .

In the initial partition $C/P_{0}$ on a transition system $(C,c)$ , we used the formulae $\Diamond\top$ and $\neg\Diamond\top$ to distinguish live states and deadlocks. In general, we can similarly describe the initial partition using modalities induced by elements of $F1$ :

Notation 3.5.

Define the injective map $j_{1}\colon 1\rightarrowtail 3$ by $j_{1}(0)=2$ . Then the injection $Fj_{1}\colon F1\rightarrowtail F3$ provides a way to interpret elements $t\in F1$ as nullary modalities ${\ulcorner t\urcorner}$ :

{\ulcorner t\urcorner}:={\ulcorner Fj_{1}(t)\urcorner}(\top,\top)\qquad\text{for $t\in F1$.}

(Alternatively, we could introduce ${\ulcorner t\urcorner}$ directly as a nullary modality.)

Lemma 3.6.

For $x\in C$ , $c\colon C\to FC$ , and $t\in F1$ , we have $x\in\llbracket{\ulcorner t\urcorner}\rrbracket$ if and only if $F!(c(x))=t$ .

3.4 Algorithmic Construction of Certificates

The $F3$ -modalities introduced above (4) induce an instance of coalgebraic modal logic (subsection 2.2). We refer to coalgebraic modal formulae employing the $F3$ -modalities as $F3$ -modal formulae, and write $\mathcal{M}$ for the set of $F3$ -modal formulae. As in the extended Paige-Tarjan algorithm (subsection 3.1), we annotate every block arising during the execution of 3.1 with a certificate in the shape of an $F3$ -modal formula. Annotating blocks with formulae means that we construct maps

\beta_{i}\colon C/Q_{i}\to\mathcal{M}\qquad\text{and}\qquad\delta_{i}\colon C/P_{i}\to\mathcal{M}\qquad\text{for $i\in\mathbb{N}$}.

As in 3.1, $i$ indexes the loop iterations. For blocks $B,S$ in the respective partition, $\beta_{i}(B)$ , $\delta_{i}(S)$ denote corresponding certificates: we will have

\forall B\in X/Q_{i}\colon\llbracket\beta_{i}(B)\rrbracket=B\qquad\text{and}\qquad\forall S\in X/P_{i}\colon\llbracket\delta_{i}(S)\rrbracket=S.

(6)

We construct $\beta_{i}(B)$ and $\delta_{i}(S)$ iteratively, using certificates for the blocks $S\subsetneqq B$ at every iteration:

Algorithm 3.7.

We extend 3.1 by the following. Initially, put

\beta_{0}(\{C\}):=\top\qquad\text{and}\qquad\delta_{0}([x]_{P_{0}}):={\ulcorner F!(c(x))\urcorner}\quad\text{for every $x\in C$.}

In the $i$ -th iteration, extend steps (A2) and (A3) by the following assignments:

(A’2)

$\mathrlap{\beta_{i+1}(D)}\phantom{\delta_{i+1}([x]_{P_{i+1}})}=\begin{cases}\delta_{i}(S)&\text{if }D=S\\ \beta_{i}(B)\wedge\neg\delta_{i}(S)&\text{if }D=B\setminus S\\ \beta_{i}(D)&\text{if }D\in C/Q_{i}\\ \end{cases}$
(A’3)

$\delta_{i+1}([x]_{P_{i+1}})=\begin{cases}\delta_{i}([x]_{P_{i}})&\text{if }[x]_{P_{i+1}}=[x]_{P_{i}}\\ \delta_{i}([x]_{P_{i}})\wedge{\ulcorner F\chi_{S}^{B}(c(x))\urcorner}(\delta_{i}(S),\beta_{i}(B))&\text{otherwise.}\\ \end{cases}$

Upon termination, return $\delta_{i}$ .

Like in subsection 3.1, the only block of $C/Q_{0}$ has $\beta_{0}(\{C\})=\top$ as a certificate. Since the partition $C/P_{0}$ distinguishes by the ‘output’ (e.g. final vs. non-final states), the certificate of $[x]_{P_{0}}$ specifies what $F!(c(x))\in F1$ is (3.6).

In the $i$ -th iteration of the main loop, we have certificates $\delta_{i}(S)$ and $\beta_{i}(B)$ for $S\subsetneqq B$ in step (A1) satisfying (6) available from the previous iterations. In (A’2), the Boolean connectives describe how $B$ is split into $S$ and $B\setminus S$ . In (A’3), new certificates are constructed for every predecessor block $T\in C/P_{i}$ that is refined. If $T$ does not change, then neither does its certificate. Otherwise, the block $T=[x]_{P_{i}}$ is split into the blocks $[x]_{F\chi_{S}^{B}(c(x))}$ for $x\in T$ in step (A3), which is reflected by the $F3$ modality ${\ulcorner F\chi_{S}^{B}(c(x))\urcorner}$ as per 3.4.

Remark 5.

In step (A’2), $\beta_{i+1}(D)$ can be simplified to be no larger than $\delta_{i}(S)$ . To see this, note that for $S\subseteq B\subseteq C$ , $S\in X/P_{i}$ , and $B\in X/Q_{i}$ , every conjunct of $\beta_{i}(B)$ is also a conjunct of $\delta_{i}(S)$ . In $\beta_{i}(B)\wedge\neg\delta_{i}(S)$ , one can hence remove all conjuncts of $\beta_{i}(B)$ from $\delta_{i}(S)$ , obtaining a formula $\delta^{\prime}$ , and then equivalently use $\beta_{i}(B)\wedge\neg\delta^{\prime}$ in the definition of $\beta_{i+1}(D)$ .

Theorem 3.8.

For zippable $F$ , 3.7 is correct, i.e. (6) holds for all $i$ . Thus, upon termination $\delta_{i}$ assigns certificates to each block of $C/\mathord{\sim}=C/P_{i}$ .

Corollary 3.9 (Hennessy-Milner).

For zippable $F$ , states $x,y$ in a finite $F$ -coalgebra are behaviourally equivalent iff they agree on all $F3$ -modal formulae.

Remark 6.

A smaller formula distinguishing a state $x$ from a state $y$ can be extracted from the certificates in time $\mathcal{O}(|C|)$ . It is the leftmost conjunct that is different in the respective certificates of $x$ and $y$ . This is the subformula starting at the modal operator introduced in $\delta_{i}$ for the least $i$ with $(x,y)\notin P_{i}$ ; hence, $x$ satisfies ${\ulcorner t\urcorner}(\delta,\beta)$ but $y$ satisfies ${\ulcorner t^{\prime}\urcorner}(\delta,\beta)$ for some $t^{\prime}\neq t$ in $F3$ .

3.5 Complexity Analysis

The operations introduced by 3.7 can be implemented with only constant run time overhead. To this end, one implements $\beta$ and $\delta$ as arrays of formulae of length $|C|$ (note that at any point, there are at most $|C|$ -many blocks). In the refinable-partition data structure [45], every block has an index (a natural number) and there is an array of length $|C|$ mapping every state $x\in C$ to the block it is contained in. Hence, for both partitions $C/P$ and $C/Q$ , one can look up a state’s block and a block’s certificate in constant time.

It is very likely that the certificates contain a particular subformula multiple times and that certificates of different blocks share common subformulae. For example, every certificate of a block refined in the $i$ -th iteration using $S\subsetneqq B$ contains the subformulas $\delta_{i}(S)$ and $\beta_{i}(B)$ . Therefore, it is advantageous to represent all certificates constructed as one directed acyclic graph (dag) with nodes labelled by modal operators and conjunction and having precisely two outgoing edges. Moreover, edges have a binary flag indicating whether they represent negation $\neg$ . Initially, there is only one node representing $\top$ , and the operations of 3.7 allocate new nodes and update the arrays for $\beta$ and $\delta$ to point to the right nodes. For example, if the predecessor block $T\in C/P_{i}$ is refined in step (A’3), yielding a new block $[x]_{P_{i+1}}$ , then a new node labelled $\wedge$ is allocated with edges to the nodes $\delta_{i}(T)$ and to another new node labelled $F\chi_{S}^{B}(c(x))$ with edges to the nodes $\delta_{i}(S)$ and $\delta_{i}(B)$ .

For purposes of estimating the size of formulae generated by the algorithm, we use a notion of transition in coalgebras, inspired by the notion of canonical graph [26].

Definition 3.10.

For states $x,y$ in an $F$ -coalgebra $(C,c)$ , we say that there is a transition $x\to y$ if $c(x)\in FC$ is not in the image $Fi[F(C\setminus\{y\})]\leavevmode\nobreak\ (\subseteq FC)$ , where $i\colon C\setminus\{y\}\rightarrowtail C$ is the inclusion map.

Theorem 3.11.

For a coalgebra with $n$ states and $m$ transitions, the formula dag constructed by 3.7 has size $\mathcal{O}(m\cdot\log n+n)$ and height at most ${n+1}$ .

Theorem 3.12.

3.7 adds only constant run time overhead, thus it has the same run time as 3.1 (regardless of the optimization from 5).

For a tighter run time analysis of the underlying partition refinement algorithm, one additionally requires that $F$ is equipped with a refinement interface [46, Def. 6.4], which is based on a given encoding of $F$ -coalgebras in terms of edges between states (encodings serve only as data structures and have no direct semantic meaning, in particular do not entail a semantic reduction to relational structures). This notion of edge yields the same numbers (in $\mathcal{O}$ -notation) as 3.10 for all functors considered. All zippable functors we consider here have refinement interfaces [46, 15]. In presence of a refinement interface, step (A3) can be implemented efficiently, with resulting overall run time $\mathcal{O}((m+n)\cdot\log n\cdot p(c))$ where $n=|C|$ , $m$ is the number of edges in the encoding of the input coalgebra $(C,c)$ , and the run-time factor $p(c)$ is associated with the refinement interface. In most instances, e.g. for $\mathcal{P}$ , $\mathbb{R}^{(-)}$ , one has $p(c)=1$ ; in particular, the generic algorithm recovers the run time of the Paige-Tarjan algorithm.

Remark 7.

The claimed run time relies on close attention to a number of implementation details. This includes use of an efficient data structure for the partition $C/P_{i}$ [31, 45]; the other partition $C/Q_{i}$ is only represented implicitly in terms of a queue of blocks $S\subsetneqq B$ witnessing $P_{i}\subsetneqq Q_{i}$ , requiring additional care when splitting blocks in the queue [44, Fig. 3]. Moreover, grouping the elements of a block by $F3$ involves the consideration of a possible majority candidate [44].

Theorem 3.13.

On a coalgebra with $n$ states and $m$ transitions for a zippable set functor with a refinement interface with factor $p(c)$ , 3.7 runs in time $\mathcal{O}((m+n)\cdot\log n\cdot p(c))$ .

4 Cancellative Functors

Our use of binary modalities relates to the fact that, as observed already by Paige and Tarjan, when splitting a block according to an existing partition of a block $B$ into $S\subseteq B$ and $B\setminus S$ , it is not in general sufficient to look only at the successors in $S$ . However, this does suffice for some transition types; e.g. Hopcroft’s algorithm for deterministic automata [27] and Valmari and Franceschinis’ algorithm for weighted systems (e.g. Markov chains) [44] both split only with respect to $S$ . In the following, we exhibit a criterion on the level of functors that captures that splitting w.r.t. only $S$ is sufficient:

Definition 8.

A functor $F$ is cancellative if the map

\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle\colon F3\to F2\times F2

is injective.

To understand the role of the above map, recall the function $\chi_{S}^{B}\colon C\to 3$ from (5) and note that $\chi_{{\{1,2\}}}\cdot\chi_{S}^{B}=\chi_{B}$ and $\chi_{{\{2\}}}\cdot\chi_{S}^{B}=\chi_{S}$ , so the composite $\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle\cdot F\chi_{S}^{B}$ yields information about the accumulated transition weights into $B$ and $S$ but not about the one into $B\setminus S$ ; the injectivity condition means that for cancellative functors, this information suffices in the splitting step for $S\subseteq B\subseteq C$ . The term cancellative stems from the respective property on monoids; recall that a monoid $M$ is cancellative if $s+b_{1}=s+b_{2}$ implies $b_{1}=b_{2}$ for all $s,b_{1},b_{2}\in M$ .

Proposition 4.1.

The monoid-valued functor $M^{(-)}$ for a commutative monoid $M$ is cancellative if and only if $M$ is a cancellative monoid.

Hence, $\mathbb{R}^{(-)}$ is cancellative, but ${\mathcal{P}_{\textsf{f}}}$ is not. Moreover, all signature functors are cancellative:

Proposition 4.2.

The class of cancellative functors contains the all constant functors as well as the identity functor, and it is closed under subfunctors, products, and coproducts.

For example, ${\mathcal{D}}$ is cancellative, but $\mathcal{P}$ is not because of its subfunctor ${\mathcal{P}_{\textsf{f}}}$ .

Remark 9.

Cancellative functors are neither closed under quotients nor under composition. Zippability and cancellativity are independent properties. Zippability in conjunction with cancellativity implies $m$ -zippability for all $m\in\mathbb{N}$ , the $m$ -ary variant [32] of zippability.

Theorem 4.3.

If $F$ is a cancellative functor, ${\ulcorner F\chi_{S}^{B}(c(x))\urcorner}(\delta_{i}(S),\beta_{i}(B))$ in 3.7 can be replaced with ${\ulcorner F\chi_{S}^{C}(c(x))\urcorner}(\delta_{i}(S),\top)$ . Then, the algorithm still correctly computes certificates in the given $F$ -coalgebra $(C,c)$ .

Note that in this optimized algorithm, the computation of $\beta$ can be omitted because it is not used anymore. Hence, the resulting formulae only involve $\wedge$ , $\top$ , and modalities from the set $F3$ (with the second parameter fixed to $\top$ ). These modalities are equivalently unary modalities induced by elements of $F2$ , which we term $F2$ -modalities; hence, the corresponding Hennessy-Milner Theorem (3.9) adapts to $F2$ for cancellative functors, as follows:

Corollary 4.4.

For zippable and cancellative $F$ , states in an $F$ -coalgebra are behaviourally equivalent iff they agree on modal formulae built using $\top$ , $\wedge$ , and unary $F2$ -modalities.

5 Domain-Specific Certificates

On a given specific system type, one is typically interested in certificates and distinguishing formulae expressed via modalities whose use is established in the respective domain, e.g. $\Box$ and $\Diamond$ for transition systems. We next describe how the generic $F3$ modalities can be rewritten to domain-specific ones in a postprocessing step. The domain-specific modalities will not in general be equivalent to $F3$ -modalities, but still yield certificates.

Definition 10.

The Boolean closure $\bar{\Lambda}$ of a modal signature $\Lambda$ has as $n$ -ary modalities propositional combinations of atoms of the form $\heartsuit(i_{1},\dots,i_{k})$ , for $\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$k$}}}\in\Lambda$ , where $i_{1},\dots,i_{k}$ are propositional combinations of elements of $\{1,\ldots,n\}$ . Such a modality $\mathord{\raisebox{1.0pt}{$\lambda$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}$ is interpreted by predicate liftings $\llbracket\lambda\rrbracket_{X}\colon(2^{X})^{n}\to FX$ defined inductively in the obvious way.

For example, the boolean closure of $\Lambda=\{\mathord{\raisebox{1.0pt}{$\Diamond$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$1$}}}\}$ contains the unary modality $\Box=\neg\Diamond\neg$ .

Definition 11.

Given a modal signature $\Lambda$ for a functor $F$ , a domain-specific interpretation consists of functions $\tau\colon F1\to\bar{\Lambda}$ and $\lambda\colon F3\to\bar{\Lambda}$ assigning to each $o\in F1$ a nullary modality $\tau_{o}$ and to each $t\in F3$ a binary modality $\lambda_{t}$ such that the predicate liftings $\llbracket\tau_{o}\rrbracket_{X}\in 2^{FX}$ and $\llbracket\lambda_{t}\rrbracket_{X}\colon(2^{X})^{2}\to 2^{FX}$ satisfy

\llbracket\tau_{o}\rrbracket_{1}=\{o\}\quad\text{(in $2^{F1}$)}\quad\text{ and }\quad[t]_{F\chi_{\{1,2\}}}\cap\llbracket\lambda_{t}\rrbracket_{3}(\{2\},\{1\})=\{t\}\quad\text{(in $2^{F3}$)}.

(Recall that $\chi_{\{1,2\}}\colon 3\to 2$ is the characteristic function of $\{1,2\}\subseteq 3$ , and $[t]_{F\chi_{\{1,2\}}}\subseteq F3$ denotes the equivalence class of $t$ w.r.t. $F\chi_{\{1,2\}}\colon F3\to F2$ .)

Thus, $\tau_{o}$ holds precisely at states with output behaviour $o\in F1$ . Intuitively, $\lambda_{t}(\delta,\rho)$ describes the refinement step of a predecessor block $T$ when splitting $B:=\llbracket\delta\rrbracket\cup\llbracket\rho\rrbracket$ into $S:=\llbracket\delta\rrbracket$ and $B\setminus S:=\llbracket\rho\rrbracket$ (Figure 3), which translates into the arguments $\{2\}$ and $\{1\}$ of $\llbracket\lambda_{t}\rrbracket_{3}$ . In the refinement step, we know from previous iterations that all elements have the same behaviour w.r.t. $B$ . This is reflected in the intersection with $[t]_{F\chi_{{\{1,2\}}}}$ . The axiom guarantees that $\lambda_{t}$ characterizes $t\in F3$ uniquely, but only within the equivalence class representing a predecessor block. Thus, $\lambda_{t}$ can be much smaller than equivalents of ${\ulcorner t\urcorner}$ (cf. 3.3):

Example 5.1.

For $F=\mathcal{P}$ , we have a domain-specific interpretation over the modal signature $\Lambda={\{\Diamond/1\}}$ . For $\emptyset,\{0\}\in\mathcal{P}1$ , take $\tau_{{\{0\}}}=\Diamond\top$ and $\tau_{\emptyset}=\neg\Diamond\top$ . For $t\in\mathcal{P}3$ , we put

\begin{array}[]{rl@{~~~}l@{\qquad}rl@{~~~}l}\lambda_{t}(\delta,\rho)&=\neg\Diamond\rho\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ &\text{if }2\in t\not\mkern 1.0mu\ni 1&\lambda_{t}(\delta,\rho)&=\Diamond\delta\wedge\Diamond\rho\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ &\text{if }2\in t\ni 1\\ \lambda_{t}(\delta,\rho)&=\neg\Diamond\delta\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ &\text{if }2\notin t\ni 1&\lambda_{t}(\delta,\rho)&=\top\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ &\text{if }2\not\in t\not\mkern 1.0mu\ni 1.\end{array}

The certificates obtained via this translation are precisely the ones generated in the example using the Paige-Tarjan algorithm, cf. (4), with $\rho$ in lieu of $\beta\wedge\neg\delta$ .

For a signature (functor) $\Sigma$ , take $\Lambda=\{\mathord{\raisebox{1.0pt}{$\sigma$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$0$}}}\mid\mathord{\raisebox{1.0pt}{$\sigma$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Sigma\}\cup\{\mathord{\raisebox{1.0pt}{${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\raisebox{-1.0pt}{$\scriptstyle I$}$}}\rangle}$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$1$}}}\mid I\in{\mathcal{P}_{\textsf{f}}}(\mathbb{N})\}$ . We interpret $\Lambda$ by the predicate liftings

	$\displaystyle\llbracket\sigma\rrbracket_{X}$	$\displaystyle=\{\sigma(x_{1},\ldots,x_{n})\mid x_{1},\ldots,x_{n}\in X\}\subseteq\Sigma X,$
	$\displaystyle\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\raisebox{-1.0pt}{$\scriptstyle I$}$}}\rangle}\rrbracket(S)$	$\displaystyle=\{\sigma(x_{1},\ldots,x_{n})\in\Sigma X\mid\forall i\in\mathbb{N}\colon i\in I\leftrightarrow(1\leq i\leq n\leavevmode\nobreak\ \wedge\leavevmode\nobreak\ x_{i}\in S)\}.$

Intuitively, ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\raisebox{-1.0pt}{$\scriptstyle I$}$}}\rangle}\,\phi$ states that the $i$ th successor satisfies $\phi$ iff $i\in I$ . We then have a domain-specific interpretation $(\tau,\lambda)$ given by $\tau_{o}:=\sigma$ for $o=\sigma(0,\ldots,0)\in\Sigma 1$ and $\lambda_{t}(\delta,\rho):={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}I$}}\rangle}\delta$ for $t=\sigma(x_{1},\ldots,x_{n})\in\Sigma 3$ and $I=\{i\in\{1,\ldots,n\}\mid x_{i}=2\}$ .

For a monoid-valued functor $M^{(-)}$ , take $\Lambda=\{\mathord{\raisebox{1.0pt}{${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$1$}}}\mid m\in M\}$ , interpreted by the predicate liftings $\llbracket{{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}}\rrbracket_{X}\colon 2^{X}\to 2^{M^{(X)}}$ given by

\llbracket{{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}}\rrbracket_{X}(S)=\{\mu\in M^{(X)}\mid m=\textstyle\sum_{x\in S}\mu(x)\}.

A formula ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}\,\delta$ thus states that the accumulated weight of the successors satisfying $\delta$ is exactly $m$ . A domain-specific interpretation $(\tau,\lambda)$ is then given by $\tau_{o}={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}o(0)$}}\rangle}\,\top$ for $o\in M^{(1)}$ and $\lambda_{t}(\delta,\rho)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\,\delta\wedge{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(1)$}}\rangle}\,\rho$ for $t\in M^{(3)}$ . In case $M$ is cancellative, we can also simply put $\lambda_{t}(\delta,\rho)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\,\delta$ .

For labelled Markov chains, i.e. $FX=({\mathcal{D}}X+1)^{A}$ , let $\Lambda=\{\mathord{\raisebox{1.0pt}{$\langle a\rangle_{p}$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$1$}}}\mid a\in A,p\in[0,1]\}$ , where $\langle a\rangle_{p}\phi$ denotes that on input $a$ , the next state will satisfy $\phi$ with probability at least $p$ , as in cited work by Desharnais et al. [17]. This gives rise to the interpretation:

\tau_{o}=\bigwedge_{\begin{subarray}{c}a\in A\\ o(a)\in{\mathcal{D}}1\end{subarray}}\langle a\rangle_{1}\top\wedge\bigwedge_{\begin{subarray}{c}a\in A\\ o(a)\in 1\end{subarray}}\neg\langle a\rangle_{1}\top\qquad\lambda_{t}(\delta,\rho)=\bigwedge_{\begin{subarray}{c}a\in A\\ t(a)\in{\mathcal{D}}3\end{subarray}}(\langle a\rangle_{t(a)(2)}\,\delta\wedge\langle a\rangle_{t(a)(1)}\,\rho)

Given a domain-specific interpretation $(\tau,\lambda)$ for a modal signature $\Lambda$ for the functor $F$ , we can postprocess certificates $\phi$ produced by 3.7 by replacing the modalities ${\ulcorner t\urcorner}$ for $t\in F3$ according to the translation $T$ recursively defined by the following clauses for modalities and by commutation with propositional operators:

T\big{(}{\ulcorner t\urcorner}(\top,\top)\big{)}=\tau_{F!(t)}\qquad T\big{(}{\ulcorner t\urcorner}(\delta,\beta))=\lambda_{t}\big{(}T(\delta),T(\beta)\wedge\neg T(\delta)\big{)}.

Note that one can replace $T(\beta)\wedge\neg T(\delta)$ with $T(\beta)\wedge\neg T(\delta^{\prime})$ for the optimized $\delta^{\prime}$ from 5; the latter conjunction has essentially the same size as $T(\delta)$ .

Proposition 5.2.

For every certificate $\phi$ of a behavioural equivalence class of a given coalgebra produced by either 3.7 or its optimization (Theorem 4.3), $T(\phi)$ is also a certificate for that class.

Thus, the domain-specific modal signatures also inherit a Hennessy-Milner Theorem.

Example 5.3.

For labelled Markov chains ( $FX=({\mathcal{D}}X+1)^{A}$ ) and the interpretation via the modalities $\langle a\rangle_{p}$ (5.1.4), this yields certificates (thus in particular distinguishing formulae) in run time $\mathcal{O}(|A|\cdot m\cdot\log n)$ , with the same bound on formula size. Desharnais et al. describe an algorithm [17, Fig. 4] that computes distinguishing formulae in the negation-free fragment of the same logic (they note also that this fragment does not suffice for certificates). They do not provide a run-time analysis, but the nested loop structure indicates that the asymptotic complexity is roughly $|A|\cdot n^{4}$ .

6 Worst Case Tree Size of Certificates

In the complexity analysis (subsection 3.5), we have seen that certificates – and thus also distinguishing formulae – have dag size $\mathcal{O}(m\cdot\log n+n)$ on input coalgebras with $n$ states and $m$ transitions. However, when formulae are written in the usual linear way, multiple occurrences of the same subformula lead to an exponential blow up of the formula size in this sense, which for emphasis we refer to as the tree size.

Figueira and Gorín [22] show that exponential tree size is inevitable even for distinguishing formulae. The proof is based on winning strategies in bisimulation games, a technique that is also applied in other results on lower bounds on formula size [23, 3, 4].

Open Problem 6.1.

Do states in $\mathbb{R}^{(-)}$ -coalgebras generally have certificates of subexponential tree size in the number of states? If yes, can small certificates be computed efficiently?

We note that for another cancellative functor, the answer is well-known: On deterministic automata, i.e. coalgebras for $FX=2\times X^{A}$ , the standard minimization algorithm constructs distinguishing words of linear length.

Remark 12.

Cleaveland [13, p. 368] also mentions that minimal distinguishing formulae may be exponential in size, however for a slightly different notion of minimality: a formula $\phi$ distinguishing $x$ from $y$ is minimal if no $\phi$ obtained by replacing a non-trivial subformula of $\phi$ with the formula $\top$ distinguishes $x$ from $y$ . This is weaker than demanding that the formula size of $\phi$ is as small as possible. For example, in the transition system

for $n\in\mathbb{N}$ ,

the formula $\phi=\Diamond^{n+2}\top$ distinguishes $x$ from $y$ and is minimal in the above sense. However, $x$ can in fact be distinguished from $y$ in size $\mathcal{O}(1)$ , by the formula $\Diamond\neg\Diamond\top$ .

7 Conclusions and Further Work

We have presented a generic algorithm that computes distinguishing formulae for behaviourally inequivalent states in state-based systems of various types, cast as coalgebras for a functor capturing the system type. Our algorithm is based on coalgebraic partition refinement [46], and like that algorithm runs in time $\mathcal{O}((m+n)\cdot\log n\cdot p(c))$ , with a functor-specific factor $p(c)$ that is $1$ in many cases of interest. Independently of this factor, the distinguishing formulae constructed by the algorithm have dag size $\mathcal{O}(m\cdot\log n+n)$ ; they live in a dedicated instance of coalgebraic modal logic [39, 42], with binary modalities extracted from the type functor in a systematic way. We have shown that for cancellative functors, the construction of formulae and, more importantly, the logic can be simplified, requiring only unary modalities and conjunction. We have also discussed how distinguishing formulae can be translated into a more familiar domain-specific syntax (e.g. Hennessy-Milner logic for transition systems).

There is an open source implementation of the underlying partition refinement algorithm [15], which may serve as a basis for a future implementation.

In partition refinement, blocks are successively refined in a top-down manner, and this is reflected by the use of conjunction in distinguishing formulae. Alternatively, bisimilarity may be computed bottom-up, as in a recent partition aggregation algorithm [11]. It is an interesting point for future investigation whether this algorithm can be extended to compute distinguishing formulae, which would likely be of a rather different shape than those computed via partition refinement.

References

[1] Peter Aczel and Nax Mendler. A final coalgebra theorem. In Proc. Category Theory and Computer Science (CTCS), volume 389 of LNCS, pages 357–365. Springer, 1989.
[2] Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial algebras, terminal coalgebras, and the theory of fixed points of functors. draft book, available online at https://www8.cs.fau.de/ext/milius/publications/files/CoalgebraBook.pdf, 2021.
[3] Micah Adler and Neil Immerman. An n! lower bound on formula size. In LICS 2001, pages 197–206. IEEE Computer Society, 2001.
[4] Micah Adler and Neil Immerman. An n! lower bound on formula size. ACM Trans. Comput. Log., 4(3):296–314, 2003.
[5] Abel Armas-Cervantes, Paolo Baldan, Marlon Dumas, and Luciano García-Bañuelos. Behavioral comparison of process models based on canonically reduced event structures. In Business Process Management, pages 267–282. Springer, 2014.
[6] Abel Armas-Cervantes, Luciano García-Bañuelos, and Marlon Dumas. Event structures as a foundation for process model differencing, part 1: Acyclic processes. In Web Services and Formal Methods, pages 69–86. Springer, 2013.
[7] Falk Bartels, Ana Sokolova, and Erik de Vink. A hierarchy of probabilistic system types. Theoret. Comput. Sci., 327:3–22, 2004.
[8] Marco Bernardo. TwoTowers 5.1 user manual, 2004.
[9] Marco Bernardo, Rance Cleaveland, Steve Sims, and W. Stewart. TwoTowers: A tool integrating functional and performance analysis of concurrent systems. In Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE / PSTV 1998, volume 135 of IFIP Conference Proceedings, pages 457–467. Kluwer, 1998.
[10] Marco Bernardo and Marino Miculan. Constructive logical characterizations of bisimilarity for reactive probabilistic systems. Theoretical Computer Science, 764:80 – 99, 2019. Selected papers of ICTCS 2016.
[11] Johanna Björklund and Loek Cleophas. Aggregation-based minimization of finite state automata. Acta Informatica, 2020.
[12] Ufuk Celikkan and Rance Cleaveland. Generating diagnostic information for behavioral preorders. Distributed Computing, 9(2):61–75, 1995.
[13] Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Computer-Aided Verification, pages 364–372. Springer, 1991.
[14] Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of LIPIcs, pages 78–93. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2015.
[15] Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic partition refinement and weighted tree automata. In Formal Methods – The Next 30 Years, Proc. 3rd World Congress on Formal Methods (FM 2019), volume 11800 of LNCS, pages 280–297. Springer, 10 2019.
[16] J. Desharnais, A. Edalat, and P. Panangaden. A logical characterization of bisimulation for labeled markov processes. In Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pages 478–487, 1998.
[17] Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled markov processes. Information and Computation, 179(2):163–193, 2002.
[18] Remco Dijkman. Diagnosing differences between business process models. In Business Process Management, pages 261–277, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
[19] Ernst-Erich Doberkat. Stochastic Coalgebraic Logic. Springer, 2009.
[20] Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient coalgebraic partition refinement. In Proc. 28th International Conference on Concurrency Theory (CONCUR 2017), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
[21] Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Predicate liftings and functor presentations in coalgebraic expression languages. In Coalgebraic Methods in Computer Science, CMCS 2018, volume 11202 of LNCS, pages 56–77. Springer, 2018.
[22] Santiago Figueira and Daniel Gorín. On the size of shortest modal descriptions. In Advances in Modal Logic 8, papers from the eighth conference on "Advances in Modal Logic," held in Moscow, Russia, 24-27 August 2010, pages 120–139. College Publications, 2010.
[23] Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. On the succinctness of some modal logics. Artificial Intelligence, 197:56 – 85, 2013.
[24] Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, volume 8089 of LNCS, pages 253–266. Springer, 2013.
[25] H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185–204. Elsevier, 2001.
[26] H.Peter Gumm. From $T$ -coalgebras to filter structures and transition systems. In Algebra and Coalgebra in Computer Science, volume 3629 of LNCS, pages 194–212. Springer, 2005.
[27] John Hopcroft. An $n\log n$ algorithm for minimizing states in a finite automaton. In Theory of Machines and Computations, pages 189–196. Academic Press, 1971.
[28] Paris C. Kanellakis and Scott A. Smolka. Ccs expressions, finite state processes, and three problems of equivalence. In Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC ’83, pages 228–240. ACM, 1983.
[29] Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43–68, 1990.
[30] Bartek Klin. The least fibred lifting and the expressivity of coalgebraic modal logic. In Algebra and Coalgebra in Computer Science, CALCO 2005, volume 3629 of LNCS, pages 247–262. Springer, 2005.
[31] Timo Knuutila. Re-describing an algorithm by Hopcroft. Theor. Comput. Sci., 250:333 – 363, 2001.
[32] Barbara König, Christina Mika-Michalski, and Lutz Schröder. Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Coalgebraic Methods in Computer Science, pages 133–154. Springer, 2020.
[33] Kim Guldstrand Larsen and Arne Arne Skou. Bisimulation through probabilistic testing. Inform. Comput., 94(1):1–28, 1991.
[34] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81(5):880–900, 2015.
[35] R. Milner. Communication and Concurrency. International series in computer science. Prentice-Hall, 1989.
[36] Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973–989, 1987.
[37] D. Park. Concurrency and automata on infinite sequences. In Proceedings of 5th GI-Conference on Theoretical Computer Science, volume 104 of LNCS, pages 167–183, 1981.
[38] Dirk Pattinson. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177 – 193, 2003.
[39] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19–33, 2004.
[40] Jan Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249:3–80, 2000.
[41] Jan Rutten and Erik de Vink. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoret. Comput. Sci., 221:271–293, 1999.
[42] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230–247, 2008.
[43] Věra Trnková. On a descriptive classification of set functors I. Commentationes Mathematicae Universitatis Carolinae, 12(1):143–174, 1971.
[44] Antti Valmari and Giuliana Franceschinis. Simple $\mathcal{O}(m\log n)$ time Markov chain lumping. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, volume 6015 of LNCS, pages 38–52. Springer, 2010.
[45] Antti Valmari and Petri Lehtinen. Efficient minimization of dfas with partial transition. In Theoretical Aspects of Computer Science, STACS 2008, volume 1 of LIPIcs, pages 645–656. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Germany, 2008.
[46] Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020.

Appendix A Appendix: Omitted Proofs

Details for section 2 (Preliminaries)

Details for subsection 2.1.

Given a pair of $F$ -coalgebra $(C,c)$ and $(D,d)$ , we have a canonical $F$ -coalgebra structure on the the disjoint union $C+D$ of their carriers:

C+D\xrightarrow{c+d}FC+FD\xrightarrow{[F\mathsf{in}_{1},F\mathsf{in}_{2}]}F(C+D).

The canonical inclusion maps $\mathsf{in}_{1}\colon C\to C+D$ and $\mathsf{in}_{2}\colon D\to C+D$ are $F$ -coalgebra morphisms. We say that states $x\in C$ and $y\in D$ are behavioural equivalent if $\mathsf{in}_{1}(x)\sim\mathsf{in}_{2}(y)$ .

Note that this definition extends the original definition of $\sim$ , in the sense that $x,y$ in the same coalgebra $(C,c)$ are behaviourally equivalent ( $x\sim y$ ) iff $\mathsf{in}_{1}(x)\sim\mathsf{in}_{2}(y)$ in the canonical coalgebra on $C+C$ .

Details on Predicate Liftings in subsection 2.2.

The naturality of $\llbracket\heartsuit\rrbracket_{X}\colon(2^{X})^{n}\to 2^{FX}$ in $X$ for $\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}$ means that for every map $f\colon X\to Y$ , the diagram

commutes. Since $2^{(-)}$ is contravariant, the map $f\colon X\to Y$ is sent to $2^{f}\colon 2^{Y}\to 2^{X}$ which takes inverse images; writing down the commutativity element-wise yields (3). By the Yoneda lemma, one can define predicate liftings

Lemma A.1.

A predicate lifting $\llbracket\heartsuit\rrbracket_{X}\colon(2^{X})^{n}\to 2^{FX}$ for $\mathord{\raisebox{1.0pt}{$\heartsuit$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}$ is uniquely defined by a map $f\colon F(2^{n})\to 2$ . Then $\llbracket\heartsuit\rrbracket_{X}$ is given by

\llbracket\heartsuit\rrbracket_{X}(P_{1},\ldots,P_{n})(\underbrace{t}_{\in\,FX})=f(F(\underbrace{x\mapsto(P_{1}(x),\ldots,P_{n}(x))}_{X\to 2^{n}})(t))

or written as sets (considering $f\subseteq F(2^{n}),P_{i}\subseteq X$ ):

\llbracket\heartsuit\rrbracket_{X}(P_{1},\ldots,P_{n})=\{t\in FX\mid F\langle\chi_{P_{1}},\ldots,\chi_{P_{n}}\rangle(t)\in f\}

Proof A.2.

The following mathematical objects are in one-to-one correspondence

\dfrac{F(2^{n})\to 2}{\dfrac{(2^{n})^{X}\to 2^{FX}\text{ natural in $X$}}{(2^{X})^{n}\to 2^{FX}\text{ natural in $X$}}}\qquad\qquad\dfrac{f}{\dfrac{p\mapsto t\mapsto f(Fp(t))}{(P_{1},\ldots,P_{n})\mapsto t\mapsto f(F\langle P_{1},\ldots,P_{n}\rangle(t))}}

The first correspondence is the Yoneda lemma and the second correspondence is a power law. On the right, the inhabitants of the sets are listed when starting with $f\colon F(2^{n})\to 2$ . By the definition of $\langle-,-\rangle$ we have:

\langle P_{1},\ldots,P_{n}\rangle\colon X\to 2^{n}\qquad x\mapsto(P_{1}(x),\ldots,P_{n}(x))

Details for section 3 (Constructing Distinguishing Formulae)

Verification of 4.

We verify that for every $t\in F3$

\llbracket{\ulcorner t\urcorner}\rrbracket_{X}\colon(2^{X})^{2}\to 2^{FX},\qquad\llbracket{\ulcorner t\urcorner}\rrbracket_{X}(S,B)=\{t^{\prime}\in FX\mid F\chi_{S\cap B}^{B}(t^{\prime})=t\}

defines a predicate lifting (3). For $f\colon X\to Y$ and $S,B\in 2^{X}$ , note that we have

\chi_{S\cap B}^{B}\cdot f=\chi_{f^{-1}[S\cap B]}^{f^{-1}[B]}

because $f(x)\in X^{\prime}$ iff $x\in f^{-1}[X^{\prime}]$ for all $x\in X$ and $X^{\prime}\subseteq X$ . We verify:

$\displaystyle Ff^{-1}\big{[}\llbracket{\ulcorner t\urcorner}\rrbracket_{Y}(S,B)\big{]}$	$\displaystyle=Ff^{-1}\big{[}{\{t^{\prime}\in FY\mid F\chi_{S\cap B}^{B}(t^{\prime})=t\}}\big{]}$	(4)
	$\displaystyle={\{t^{\prime\prime}\in FX\mid F\chi_{S\cap B}^{B}(Ff(t^{\prime\prime}))=t\}}\big{]}$	(def. inv. Image)
	$\displaystyle={\{t^{\prime\prime}\in FX\mid F(\chi_{S\cap B}^{B}\cdot f)(t^{\prime\prime}))=t\}}\big{]}$	(Functoriality)
	$\displaystyle={\{t^{\prime\prime}\in FX\mid F\chi_{f^{-1}[S\cap B]}^{f^{-1}[B]}(t^{\prime\prime})=t\}}\big{]}$	$(*)$
	$\displaystyle={\{t^{\prime\prime}\in FX\mid F\chi_{f^{-1}[S]\cap f^{-1}[B]}^{f^{-1}[B]}(t^{\prime\prime})=t\}}\big{]}$
	$\displaystyle=\llbracket{\ulcorner t\urcorner}\rrbracket_{X}(f^{-1}[S],f^{-1}[B])$	(4)

Hence, $\llbracket{\ulcorner t\urcorner}\rrbracket$ is a predicate lifting.

Proof of 3.4.

This follows directly from 4 for $S:=\llbracket\phi_{S}\rrbracket$ and $B:=\llbracket\phi_{B}\rrbracket$ , using that $S\cap B=S$ :

	$\displaystyle\llbracket{\ulcorner t\urcorner}(\phi_{S},\phi_{B})\rrbracket$	$\displaystyle=c^{-1}[\llbracket{\ulcorner t\urcorner}\rrbracket_{C}(\llbracket\phi_{S}\rrbracket,\llbracket\phi_{B}\rrbracket)]$
		$\displaystyle=c^{-1}[\llbracket{\ulcorner t\urcorner}\rrbracket_{C}(S,B)]$
		$\displaystyle=c^{-1}[\{t^{\prime}\in FC\mid F\chi_{S\cap B}^{B}(t^{\prime})=t\}]$
		$\displaystyle=\{x\in C\mid F\chi_{S}^{B}(c(x))=t\}.$

Proof of 3.6.

Note that for $\chi_{C}^{C}\colon C\to 3$ , we have $\chi_{C}^{C}=(C\xrightarrow{\leavevmode\nobreak\ !\leavevmode\nobreak\ }1\xrightarrow{\leavevmode\nobreak\ j_{1}\leavevmode\nobreak\ }3)$ where $j_{1}(0)=2$ .

$\displaystyle\llbracket{\ulcorner t\urcorner}\rrbracket$	$\displaystyle=\llbracket{\ulcorner Fj_{1}(t)\urcorner}(\top,\top)\rrbracket$	(3.5)
	$\displaystyle=\{x\in C\mid F\chi_{C}^{C}(c(x))=Fj_{1}(t)\}$	(3.4, $\llbracket\top\rrbracket=C$ )
	$\displaystyle=\{x\in C\mid Fj_{1}(F!(c(x)))=Fj_{1}(t)\}$	( $\chi_{C}^{C}=j_{1}\cdot!$ )
	$\displaystyle=\{x\in C\mid F!(c(x))=t\}$	( $Fj_{1}$ injective)

In the last step use that, w.l.o.g., $F$ preserves injective maps (subsection 2.1). ∎

Proof of Theorem 3.8.

We first observe that given $x\in C$ , $S\subseteq B\subseteq C$ , and formulae $\phi_{S}$ and $\phi_{B}$ which characterize $S$ and $B$ , respectively, we have:

	$\displaystyle\llbracket{\ulcorner F\chi_{S}^{B}(c(x))\urcorner}(\phi_{S},\phi_{B})\rrbracket$	$\displaystyle=\{x^{\prime}\in C\mid F\chi_{\llbracket\phi_{S}\rrbracket}^{\llbracket\phi_{B}\rrbracket}(c(x^{\prime}))=F\chi_{S}^{B}(c(x))\}$		(7)
		$\displaystyle=[x]_{F\chi_{S}^{B}(c(x))},$		(8)

where (7) uses 3.4 and (8), holds since $\llbracket\phi_{B}\rrbracket=B$ and $\llbracket\phi_{S}\rrbracket=S$ .

We proceed to the verification of (6) by induction on $i$ .

•

In the base case $i=0$ , we have $\llbracket\beta_{0}(\{C\})\rrbracket=\llbracket\top\rrbracket=\{C\}$ for the only block in $X/Q_{0}$ . Since $P_{0}=\ker(F!\cdot c)$ , $\delta_{0}$ is well-defined, and by 3.6 we have

\llbracket\delta_{0}([x]_{P_{0}})\rrbracket=\llbracket{\ulcorner F!(c(x))\urcorner}\rrbracket=\{y\in C\mid F!(c(x))=F!(c(y))\}=[x]_{P_{0}}.

•

The inductive hypothesis states that

\llbracket\delta_{i}(S)\rrbracket=S\qquad\text{and}\qquad\llbracket\beta_{i}(B)\rrbracket=B.

We prove that $\beta_{i+1}$ is correct:

	$\displaystyle\llbracket\beta_{i+1}([x]_{Q_{i+1}})\rrbracket$
	$\displaystyle=\begin{cases}\llbracket\delta_{i}(S)\rrbracket&\text{if }[x]_{Q_{i+1}}=S\text{, hence }S=[x]_{P_{i}}\\ \llbracket\beta_{i}(B)\rrbracket\leavevmode\nobreak\ \cap\leavevmode\nobreak\ C\setminus\llbracket\delta_{i}(S)\rrbracket&\text{if }[x]_{Q_{i+1}}=B\setminus S\text{, hence }B=[x]_{Q_{i}}\\ \llbracket\beta_{i}([x]_{Q_{i}})\rrbracket&\text{if }[x]_{Q_{i+1}}\in C/Q_{i}\\ \end{cases}$
	$\displaystyle\overset{\mathclap{\text{(IH)}}}{=}\begin{cases}S&\text{if }[x]_{Q_{i+1}}=S\\ B\leavevmode\nobreak\ \cap\leavevmode\nobreak\ C\setminus S&\text{if }[x]_{Q_{i+1}}=B\setminus S\\ [x]_{Q_{i}}&\text{if }[x]_{Q_{i+1}}\in C/Q_{i}\\ \end{cases}$
	$\displaystyle=\begin{cases}[x]_{Q_{i+1}}&\text{if }[x]_{Q_{i+1}}=S=[x]_{P_{i}}\\ [x]_{Q_{i+1}}&\text{if }[x]_{Q_{i+1}}=B\setminus S\qquad\text{(since $B\cap C\setminus S=B\setminus S$)}\\ [x]_{Q_{i+1}}&\text{if }[x]_{Q_{i+1}}\in C/Q_{i}\qquad\text{(since $[x]_{Q_{i}}$ is not split)}\\ \end{cases}$
	$\displaystyle=[x]_{Q_{i+1}}.$

For $\delta_{i+1}$ , we compute as follows:

	$\displaystyle\llbracket\delta_{i+1}([x]_{P_{i+1}})\rrbracket$
	$\displaystyle=\qquad\begin{cases}\llbracket\delta_{i}([x]_{P_{i}})\rrbracket&\text{if }[x]_{P_{i+1}}=[x]_{P_{i}}\\ \llbracket\delta_{i}([x]_{P_{i}})\rrbracket\cap\llbracket{\ulcorner F\chi_{S}^{B}(c(x))\urcorner}(\delta_{i}(S),\beta_{i}(B))\rrbracket&\text{otherwise}\end{cases}$
	$\displaystyle\overset{\mathclap{\text{(IH) \& \eqref{eqF3ModBS}}}}{=}\qquad\begin{cases}[x]_{P_{i}}&\text{if }[x]_{P_{i+1}}=[x]_{P_{i}}\\ [x]_{P_{i}}\cap[x]_{F\chi_{S}^{B}(c(x))}&\text{otherwise}\end{cases}$
	$\displaystyle\overset{\mathclap{\text{def. }P_{i+1}}}{=}\qquad\begin{cases}[x]_{P_{i+1}}&\text{if }[x]_{P_{i+1}}=[x]_{P_{i}}\\ [x]_{P_{i+1}}&\text{otherwise}\end{cases}$
	$\displaystyle=\quad[x]_{P_{i+1}}$

Details for 6.

In order to verify that the first differing conjunct is a distinguishing formula, we perform a case distinction on the least $i$ with $(x,y)\notin P_{i}$ :

If $x$ and $y$ are already split by $P_{0}$ , then the conjunct at index $0$ in the respective certificates of $[x]_{\sim}$ and $[y]_{\sim}$ differs, and we have $t=F!(c(x))$ and $t^{\prime}=F!(c(y))$ . By 3.6, ${\ulcorner t\urcorner}$ distinguishes $x$ from $y$ (and ${\ulcorner t^{\prime}\urcorner}$ distinguishes $y$ from $x$ ).

If $x$ and $y$ are split by $P_{i+1}$ (but $(x,y)\in P_{i}$ ) in the $i$ th iteration, then

\underbrace{F\chi_{S}^{B}(c(x))}_{t\leavevmode\nobreak\ :=}\neq\underbrace{F\chi_{S}^{B}(c(y))}_{t^{\prime}\leavevmode\nobreak\ :=}.

Thus, the conjuncts that differs in the respective certificates for $[x]_{\sim}$ and $[y]_{\sim}$ are the following conjuncts at index $i+1$ :

{\ulcorner t\urcorner}(\delta_{i}(S),\beta_{i}(B))\qquad\text{and}\qquad{\ulcorner t^{\prime}\urcorner}(\delta_{i}(S),\beta_{i}(B)).

By 3.4, ${\ulcorner t\urcorner}(\delta_{i}(S),\beta_{i}(B))$ distinguishes $x$ from $y$ (and ${\ulcorner t\urcorner}(\delta_{i}(S),\beta_{i}(B))$ distinguishes $y$ from $x$ ).

Proof of Theorem 3.11.

Before proving Theorem 3.11, we need to establish a sequence of lemmas on the underlying partition refinement algorithm. We assume wlog that $F$ preserves finite intersections; that is pullbacks of pairs of injective maps. In fact, the functor $G$ mentioned in subsection 2.1, which coincides with $F$ on all nonempty sets and map and therefore has the same coalgebras, preserves finite intersections..

Let $(C,c)$ be a coalgebra for $F$ . As additional notation, we define for all sets $T\subseteq C$ and $S\subseteq C$ :

T\to S\qquad:\Longleftrightarrow\qquad\exists x\in T,y\in S\colon x\to y.

In other words, we write $T\to S$ if there is a transition from (some state of) $T$ to (some state of) $S$ . Also we define the set of predecessor states of a set as:

\mathsf{pred}(S)=\{x\in C\mid\{x\}\to S\}\qquad\text{for }S\subseteq C.

Lemma A.3.

For every $F$ -coalgebra $(C,c)$ , $x\in C$ , and $S\subseteq B\subseteq C$ with $S$ finite, we have

\{x\}\not\to S\qquad\Longrightarrow\qquad F\chi_{S}^{B}(c(x))=F\chi_{\emptyset}^{B}(c(x)).

Proof A.4.

For every $y\in S$ , we have that $x\not\to y$ . Hence, for every $y\in S$ , there exists $t_{y}\in F(C\setminus\{y\})$ such that

c(x)=Fi(t_{y})\qquad\text{for }i\colon C\setminus\{y\}\rightarrowtail C.

The set $C\setminus S$ is the intersection of all sets $C\setminus\{y\}$ with $y\in S$ :

C\setminus S=\bigcap_{y\in S}(C\setminus\{y\}).

Since $F$ preserves finite intersections and $S$ is finite, we have that

F(C\setminus S)=\bigcap_{y\in S}F(C\setminus\{y\}).

Since $c(x)\in FC$ is contained in every $F(C\setminus\{y\})$ (as witnessed by $t_{y}$ ) it is also contained in their intersection. That is, for $m\colon C\setminus S\rightarrowtail C$ being the inclusion map, there is $t^{\prime}\in F(C\setminus S)$ with $Fm(t^{\prime})=c(x)$ . Now consider the following diagrams:

and

Both triangles commute because $\chi_{\emptyset}^{B}=\chi_{S}^{B}\cdot m$ and $\chi_{\emptyset}^{B}=\chi_{\emptyset}^{B}\cdot m$ . Thus, we conclude

F\chi_{S}^{B}(c(x))=F\chi_{S}^{B}(Fm(t^{\prime}))=F\chi_{\emptyset}^{B}(t^{\prime})=F\chi_{\emptyset}^{B}(Fm(t^{\prime}))=F\chi_{\emptyset}^{B}(c(x)).

Lemma A.5.

For all $(x,x^{\prime})\in P_{i}$ and $B\in C/Q_{i}$ in 3.1, we have

F\chi_{\emptyset}^{B}(c(x))=F\chi_{\emptyset}^{B}(c(x^{\prime})).

Proof A.6.

One can show[46, Prop. 4.12] that in every iteration there is a map $c_{i}\colon C/P_{i}\to F(C/Q_{i})$ that satisfies $F[-]_{Q_{i}}\cdot c=c_{i}\cdot[-]_{P_{i}}$ :

where the maps $[-]_{P_{i}},[-]_{Q_{i}}$ send elements of $C$ to their equivalence class (section 2). The map $\chi_{\emptyset}^{B}\colon C\to 3$ for $B\in C/Q_{i}$ can be decomposes as:

Combining these two diagrams, we obtain:

F\chi_{\emptyset}^{B}\cdot c=F\chi_{\emptyset}^{\{B\}}\cdot F[-]_{Q_{i}}\cdot c=F\chi_{\emptyset}^{\{B\}}\cdot c_{i}\cdot[-]_{P_{i}}.

(9)

For all $(x,x^{\prime})\in P_{i}$ , we have $[x]_{P_{i}}=[x^{\prime}]_{P_{i}}$ , and thus we have

F\chi_{\emptyset}^{B}(c(x))\overset{\eqref{eqChiEq}}{=}F\chi_{\emptyset}^{\{B\}}(c_{i}([x]_{P_{i}}))=F\chi_{\emptyset}^{\{B\}}(c_{i}([x^{\prime}]_{P_{i}}))\overset{\eqref{eqChiEq}}{=}F\chi_{\emptyset}^{B}(c(x^{\prime})).

Lemma A.7.

For $S\subsetneqq B\in C/Q_{i}$ in the $i$ th iteration of 3.1, any block $T\in C/P_{i}$ with no edge to $S$ is not modified; in symbols:

T\not\to S\quad\Longrightarrow\quad T\in C/P_{i+1}

Proof A.8.

Since $T\not\to S$ , we have $\{x\}\not\to S$ and $\{x^{\prime}\}\not\to S$ for all $x,x^{\prime}\in T$ . Thus,

$\displaystyle F\chi_{S}^{B}(c(x))$	$\displaystyle=F\chi_{\emptyset}^{B}(c(x))$	(A.3, $\{x\}\not\to S$ )
	$\displaystyle=F\chi_{\emptyset}^{B}(c(x^{\prime}))$	(A.5, $(x,x^{\prime})\in P_{i}$ )
	$\displaystyle=F\chi_{S}^{B}(c(x^{\prime}))$	(A.3, $\{x^{\prime}\}\not\to S$ )

as desired.

Lemma A.9.

For $S\subseteq C$ and finite $C$ in the $i$ th iteration of 3.1,

|\{T^{\prime}\in C/P_{i+1}\mid T^{\prime}\not\in C/P_{i}\}|\leavevmode\nobreak\ \leq\leavevmode\nobreak\ 2\cdot|\mathsf{pred}(S)|.

Proof A.10.

Let $S\subsetneqq B\in C/Q_{i}$ be used for splitting in iteration $i$ . By contraposition, A.7 implies that if $T^{\prime}\in C/P_{i+1}$ and $T^{\prime}\not\in C/P_{i}$ , then (the unique) $T\in C/P_{i}$ with $T^{\prime}\subseteq T$ satisfies $T\not\in C/P_{i+1}$ and thefore has a transition to $S$ . By the finiteness of $C$ , the block $T\in C/P_{i}$ is split into finitely many blocks $T_{1},\ldots,T_{k}\in C/P_{i+1}$ , representing the equivalence classes for $F\chi_{S}^{B}\cdot c\colon C\to F3$ . By A.3 we know that if $x\in T$ has no transition to $S$ , then $F\chi_{S}^{B}(c(x))=F\chi_{\emptyset}^{B}(c(x))$ . Moreover, all elements of $T\in C/P_{i}$ are sent to the same value by $F\chi_{\emptyset}^{B}\cdot c$ (A.5). Hence, there is at most one block $T_{j}$ with no transition to $S$ , and all other blocks $T_{j^{\prime}}$ , $j^{\prime}\neq j$ , have a transition to $S$ .Therefore the number blocks $T_{j}$ is bounded above as follows: $k\leq|T\cap\mathsf{pred}(S)|+1$ . Summing over all predecessor blocks $T$ we obtain:

	$\displaystyle\|\{T^{\prime}\in C/P_{i+1}\mid T^{\prime}\not\in C/P_{i}\}\|$
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle\|\{T^{\prime}\in C/P_{i+1}\mid T^{\prime}\subseteq T\in C/P_{i}\text{ and }T\to S\}\|$	(A.7)
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\sum_{\begin{subarray}{c}T\in C/P_{i}\\ T\to S\end{subarray}}\|\{T^{\prime}\in C/P_{i+1}\mid T^{\prime}\subseteq T\}\|$
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle\sum_{\begin{subarray}{c}T\in C/P_{i}\\ T\to S\end{subarray}}(\|T\cap\mathsf{pred}(S)\|+1)$	(bound on $k$ above)
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle 2\cdot\sum_{\begin{subarray}{c}T\in C/P_{i}\\ T\to S\end{subarray}}\|T\cap\mathsf{pred}(S)\|$	$\|T\cap\mathsf{pred}(S)\|\geq 1$
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle 2\cdot\|\mathsf{pred}(S)\|$	( $T\in C/P_{i}$ are disjoint)

This completes the proof

Lemma A.11.

Throughout the execution of 3.1 for an input coalgebra $(C,c)$ with $n=|C|$ states and $m$ transitions, we have

|\{T\subseteq C\mid T\in C/P_{i}\text{ for some }i\}|\leq 2\cdot m\cdot\log_{2}n+2\cdot m+n.

Remark.

Note that the proof is similar to arguments given in the complexity analysis of the Paige-Tarjan algorithm; for instance, compare to [36, p. 980] (or [46, Lem. 7.15]).

Proof A.12.

Because $|S|\leq\frac{1}{2}\cdot|B|$ holds in step (A1) of 3.1, one can show that every state $x\in C$ is contained in the set $S$ in at most $(\log_{2}(n)+1)$ iterations [46, Lem. 7.15]. More formally, let $S_{i}\subsetneq B_{i}\in C/Q_{i}$ be the blocks picked in the $i$ th iteration of 3.1. Then we have

|\{S_{i}\mid x\in S_{i}\}|\leq\log_{2}n+1\qquad\text{for all }x\in C.

(9)

Let the algorithm terminate after $\ell$ iterations returning $C/P_{\ell}$ . Then, the number of new blocks introduced by step (A3) is bounded as follows (note that after the third step, $x\in S_{i}$ is a side condition enforcing that we have a summand $|\mathsf{pred}({\{x\}})|$ provided that $x$ lies in $S_{i}$ , whereas before we sum over all $x\in S_{i}$ ):

	$\displaystyle\sum_{0\leq i<\ell}\|\{T^{\prime}\in C/P_{i+1}\mid T^{\prime}\notin C/P_{i}\}\|$
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle\sum_{0\leq i<\ell}2\cdot\|\mathsf{pred}(S_{i})\|$	(A.9)
$\displaystyle\leq\leavevmode\nobreak\$	$\displaystyle 2\cdot\sum_{0\leq i<\ell}\,\sum_{x\in S_{i}}\|\mathsf{pred}(\{x\})\|$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle 2\cdot\sum_{x\in C}\,\sum_{\begin{subarray}{c}0\leq i<\ell\\ x\in S_{i}\end{subarray}}\|\mathsf{pred}(\{x\})\|$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle 2\cdot\sum_{x\in C}\,\|\mathsf{pred}(\{x\})\|\cdot\sum_{\begin{subarray}{c}0\leq i<\ell\\ x\in S_{i}\end{subarray}}1$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle 2\cdot\sum_{x\in C}\,\|\mathsf{pred}(\{x\})\|\cdot(\log_{2}n+1)$	by (9)
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle 2\cdot m\cdot(\log_{2}n+1)=2\cdot m\cdot\log_{2}n+2\cdot m$

The only blocks we have not counted so far are the blocks of $C/P_{0}$ , since $|C/P_{0}|\leq n$ , we have at most $2\cdot m\cdot\log_{2}n+2\cdot m+n$ different blocks in $(C/P_{i})_{0\leq i<\ell}$ .

We are now ready to prove the main theorem on the dag size of formulae created by 3.7.

Proof A.13 (Proof of Theorem 3.11).

Regarding the height of the dag, it is immediate that $\delta_{i}$ and $\beta_{i}$ have a height of at most $i+1$ . Since $|C/Q_{i}|<|C/Q_{i+1}|\leq|C|=n$ for all $i$ , there are at most $n$ iterations, with the final partition being $C/P_{n+1}=C/Q_{n+1}$ .

In 3.7 we create a new modal operator formula whenever 3.1 creates a new block in $C/P_{i}$ . By A.11, the number of modalities in the dag is thus bounded by

2\cdot m\cdot\log_{2}n+2\cdot m+n

In every iteration of the main loop, $\beta$ is extended by two new formulae, one for $S$ and one for $B\setminus S$ . The formula $\beta_{i+1}(S)$ does not increase the size of the dag, because no new node needs to be allocated. For $\beta_{i+1}(B\setminus S)$ , we need to allocate one new node for the conjunction, so there are at most $n$ new such nodes allocated throughout the execution of the whole algorithm. Even if the optimization in 5 is applied, the additional run time can be neglected under the $\mathcal{O}$ -notation.

Proof of Theorem 3.12.

We implement every operation of 3.7 in constant time. The arrays for $\beta$ and $\delta$ are re-used in every iteration. Hence the index $i$ is entirely neglected and only serves as an indicator for whether we refer to a value before or after the loop iteration. We proceed by case distinction as follows:

1.
Initialization step:
- •
  
  The only block $\{C\}$ in $C/Q_{0}$ has index 0, and so we make $\beta(0)$ point to the node $\top$ .
- •
  
  For every block $T$ in $C/P_{0}$ , 3.1 has computed $F!(c(x))\in F1$ for some (in fact every) $x\in T$ . Since $F1$ canonically embeds into $F3$ (3.5), we create a new node labelled ${\ulcorner Fj_{1}(F!(c(x)))\urcorner}$ with two edges to $\top$ .
  
  For every $T\in C/P_{0}$ , this runs in constant time and can be performed whenever the original 3.1 creates a new such block $T$ .

In the refinement step, we can look up the certificates $\delta_{i}(S)$ resp. $\beta_{i}(B)$ for $S$ resp. $B$ in constant time using the indices of the blocks $S$ and $B$ . Whenever the original algorithm creates a new block, we also immediately construct the certificate of this new block by creating at most two new nodes in the dag (with at most four outgoing edges). However, if a block does not change (that is, $[x]_{Q_{i}}=[x]_{Q_{i+1}}$ or $[x]_{P_{i}}=[x]_{P_{i+1}}$ , resp.), then the corresponding certificate is not changed either in steps item (A’2) resp. item (A’3).

In the loop body we update the certificates as follows:

(A’2)

The new block $S\in C/Q_{i+1}$ just points to the certificate $\delta_{i}(S)$ constructed earlier. For the new block $(B\setminus S)\in C/Q_{i+1}$ , we allocate a new node $\wedge$ , with one edge to $\beta_{i}(B)$ and one negated edge to $\delta_{i}(S)$ . (See also details for 5 on the run time for computing the optimized negation.)

(A’3)

Not all resulting blocks have a transition to $S$ . There may be (at most) one new block $T^{\prime}\in C/P_{i+1}$ , $T^{\prime}\subseteq T$ with no transition to $S$ (see the proof of A.9). In the refinable partition structure, such a block will inherit the index from $T$ (i.e. the index of $T$ in $C/P_{i}$ equals the index of $T^{\prime}$ in $C/P_{i+1}$ ). Moreover, every $x\in T^{\prime}$ fulfils $F\chi_{S}^{B}(c(x))=F\chi_{\emptyset}^{B}(c(x))$ (by A.3), and $F\chi_{\emptyset}^{B}(c(x))=F\chi_{\emptyset}^{B}(c(y))$ for every $y\in T$ (by A.5).

Now, one first saves the node of the certificate $\delta_{i}(T)$ in some variable $\delta^{\prime}$ , say. Then the array $\delta$ is updated at index $T$ by the formula

{\ulcorner F\chi_{\emptyset}^{B}(c(y))\urcorner}(\delta_{i}(S),\beta_{i}(B))\qquad\text{for an arbitrary $y\in T$.}

Consequently, any block $T^{\prime}$ inheriting the index of $T$ automatically has the correct certificate.

The allocation of nodes for this formula is completely analogous to the one for an ordinary block $[x]_{P_{i+1}}\subsetneqq T$ having edges to $S$ : One allocates a new node labelled $\wedge$ with edges to the saved node $\delta^{\prime}$ (the original value of $\delta_{i}(T)$ ) and to another newly allocated node labelled ${\ulcorner F\chi_{S}^{B}(c(x))\urcorner}$ with edges to the nodes $\delta_{i}(S)$ and $\delta_{i}(B)$ . ∎

Details for 5.

In order to keep the formula size smaller, one can implement the optimization of 5, but one has to take care not to increase the run time. To this end, mark every modal operator node ${\ulcorner t\urcorner}(\delta,\beta)$ in the formula dag with a boolean flag expressing whether:

${\ulcorner t\urcorner}(\delta,\beta)$ is a conjunct of some $\beta_{i}$ -formula.

Thus, every new modal operator in (A’3) is flagged ‘false’ initially. When splitting the block $B$ in $C/Q_{i}$ into $S$ and $B\setminus S$ in step (A’2), the formula for block $B\setminus S$ is a conjunction of $\beta_{i}(B)$ and the negation of all ‘false’-marked conjuncts of $\delta_{i}(S)$ . Afterwards these conjuncts are all marked ‘true’, because they are inherited by $\beta_{i}(S)$ . The ‘false’-marked conjuncts always form a prefix of all conjuncts of a formula in $\delta_{i}$ . It therefore suffices to greedily take conjuncts from the root of a formula graph while they are marked ‘false’.

As a consequence, step (A’3) does not run in constant time but instead takes as many steps as there are ‘false’-marked conjuncts in $\delta_{i}(S)$ . However, over the whole execution of the algorithm this eventually amortizes because every newly allocated modal operator allocated is initially marked ‘false’ and later marked ‘true’ precisely once.

Proof of Theorem 3.13.

The overall run time is immediate, because the underlying 3.1 has run time $\mathcal{O}((m+n)\cdot\log n\cdot p(c))$ and 3.7 preserves this run time by Theorem 3.12.

Details for section 4 (Cancellative Functors)

Proof of 4.1.

First note that for $FX=M^{(X)}$ the maps in 8 are defined by:

\begin{array}[]{r@{\ }l@{\qquad}l}M^{(\chi_{{\{1,2\}}})}\colon&M^{(3)}\to M^{(2)},&t\mapsto(t(0),t(1)+t(2)),\\[5.0pt] M^{(\chi_{{\{2\}}})}\colon&M^{(3)}\to M^{(2)},&t\mapsto(t(0)+t(1),t(2)),\end{array}

where we write $s\in M^{(2)}$ as the pair $(s(0),s(1))$ .

For $(\Leftarrow)$ , let $s,t\in M^{(3)}$ with

\langle M^{(\chi_{{\{1,2\}}})},M^{(\chi_{{\{2\}}})}\rangle(s)=\langle M^{(\chi_{{\{1,2\}}})},M^{(\chi_{{\{2\}}})}\rangle(t),

which is written point-wise as follows:

	$\displaystyle(s(0),s(1)+s(2))$	$\displaystyle=(t(0),t(1)+t(2))$
	$\displaystyle(s(0)+s(1),s(2))$	$\displaystyle=(t(0)+t(1),t(2)).$

Hence, $s(0)=t(0)$ , $s(2)=t(2)$ and moreover

s(1)+s(2)=t(1)+t(2)=t(1)+s(2).

Since $M$ is cancellative, we have $s(1)=t(1)$ , which proves that $s=t$ . Thus, the map $\langle M^{(\chi_{{\{1,2\}}})},M^{(\chi_{{\{2\}}})}\rangle$ is injective.

For $(\Rightarrow)$ , let $a,b,c\in M$ with $c+a=c+b$ . Define $s,t\in M^{(3)}$ by

s(0)=s(2)=c,\quad s(1)=a\qquad\text{and}\qquad t(0)=t(2)=c,\quad t(1)=b.

Thus,

\begin{aligned} M^{(\chi_{{\{1,2\}}})}(s)&=(s(0),s(1)+s(2))\\ &=(c,a+c)\\ &=(c,b+c)\\ &=(t(0),t(1)+t(2))\\ &=M^{(\chi_{{\{1,2\}}})}(t),\end{aligned}\qquad\qquad\begin{aligned} M^{(\chi_{{\{2\}}})}(s)&=(s(0)+s(1),s(2))\\ &=(c+a,c)\\ &=(c+b,c)\\ &=(t(0)+t(1),t(2))\\ &=M^{(\chi_{{\{2\}}})}(t).\end{aligned}

Since $\langle M^{(\chi_{{\{1,2\}}})},M^{(\chi_{{\{2\}}})}\rangle$ is injective, we see that $s=t$ holds. Thus, we have $a=s(1)=t(1)=b$ , which proves that $M$ is cancellative.∎

Proof of 4.2.

1.

For the constant functor $C_{X}$ with value $X$ , $C_{X}\chi_{S}$ is the identity map on $X$ for every set $S$ . Therefore $C_{X}$ is cancellative.
2.

The identity functor is cancellative because the map $\langle\chi_{{\{1,2\}}},\chi_{{\{2\}}}\rangle$ is clearly injective.

Let $\alpha\colon F\rightarrowtail G$ a natural transformation with injective components and let $G$ be cancellative. Combining the naturality squares of $\alpha$ for $\chi_{{\{1,2\}}}$ and $\chi_{{\{2\}}}$ , we obtain the commutative square:

Every composition of injective maps is injective, and so by standard cancellation laws for injective maps, $\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle$ is injective as well, showing that the subfunctor $F$ is cancellative.

Let $(F_{i})_{i\in I}$ be a family of cancellative functors, and suppose that we have elements $s,t\in(\prod_{i\in I}F_{i})(3)=\prod_{i\in I}F_{i}3$ with

\big{(}\prod_{i\in I}F_{i}\chi_{{\{1,2\}}}\big{)}(s)=\big{(}\prod_{i\in I}F_{i}\chi_{{\{1,2\}}}\big{)}(t)\quad\text{and}\quad\big{(}\prod_{i\in I}F_{i}\chi_{{\{2\}}}\big{)}(s)=\big{(}\prod_{i\in I}F_{i}\chi_{{\{2\}}}\big{)}(t).

Write $\mathsf{pr}_{i}$ for the $i$ th projection function from the product. For every $i\in I$ we have:

F_{i}\chi_{{\{1,2\}}}(\mathsf{pr}_{i}(s))=F_{i}\chi_{{\{1,2\}}}(\mathsf{pr}_{i}(t))\qquad\text{and}\qquad F_{i}\chi_{{\{2\}}}(\mathsf{pr}_{i}(s))=F_{i}\chi_{{\{2\}}}(\mathsf{pr}_{i}(t)).

Since every $F_{i}$ is cancellative, we have $\mathsf{pr}_{i}(s)=\mathsf{pr}_{i}(t)$ for every $i\in I$ . This implies $s=t$ since the product projections $(\mathsf{pr}_{i})_{i\in I}$ are jointly injective.

Again, let $(F_{i})_{i\in I}$ be a family of cancellative functors. Suppose that we have elements $s,t\in(\coprod_{i\in I}F_{i})(3)=\coprod_{i\in I}F_{i}3$ satisfying

\big{(}\coprod_{i\in I}F_{i}\chi_{{\{1,2\}}}\big{)}(s)=\big{(}\coprod_{i\in I}F_{i}\chi_{{\{1,2\}}}\big{)}(t)\quad\text{and}\quad\big{(}\coprod_{i\in I}F_{i}\chi_{{\{2\}}}\big{)}(s)=\big{(}\coprod_{i\in I}F_{i}\chi_{{\{2\}}}\big{)}(t).

This implies that there exists an $i\in I$ and $t^{\prime},s^{\prime}\in F_{i}$ with $s=\mathsf{in}_{i}(s^{\prime})$ , $t=\mathsf{in}_{i}(t^{\prime})$ , and

F_{i}\chi_{{\{1,2\}}}(s)=F_{i}\chi_{{\{1,2\}}}(t)\qquad\text{and}\qquad F_{i}\chi_{{\{2\}}}(s)=F_{i}\chi_{{\{2\}}}(t).

Since $F_{i}$ is cancellative, we have $s=t$ as desired. ∎

Details for 9.

Operation	cancellative	non-cancellative
Quotient	$X\mapsto\coprod_{n\in\mathbb{N}}X^{n}$	${\mathcal{P}_{\textsf{f}}}$
Composition	$\mathcal{B}=\mathbb{N}^{(-)}$	$\mathcal{B}\mathcal{B}$

	cancellative	non-cancellative
zippable	$X\mapsto X$	${\mathcal{P}_{\textsf{f}}}$
non-zippable	see (10)	${\mathcal{P}_{\textsf{f}}}{\mathcal{P}_{\textsf{f}}}$

1.

Cancellative functors are not closed under quotients: e.g. the non-cancellative functor ${\mathcal{P}_{\textsf{f}}}$ is a quotient of the signature functor $X\mapsto\coprod_{n\in\mathbb{N}}X^{n}$ (which is cancellative by 4.2).

Cancellative functors are not closed under composition. For the additive monoid $(\mathbb{N},+,0)$ of natural numbers, the monoid-valued functor $\mathcal{B}=\mathbb{N}^{(-)}$ sends $X$ to the set of finite multisets on $X$ (‘bags’). Since $\mathbb{N}$ is cancellative, $\mathcal{B}$ is a cancellative functor. However, $\mathcal{B}\mathcal{B}$ is not:

	$\displaystyle\langle\mathcal{B}\mathcal{B}\chi_{{\{1,2\}}},\mathcal{B}\mathcal{B}\chi_{{\{2\}}}\rangle\big{(}{\big{\lBrace}{\lBrace 0,1\rBrace},{\lBrace 1,2\rBrace}\big{\rBrace}}$
	$\displaystyle=\big{(}{\big{\lBrace}{\lBrace 0,1\rBrace},{\lBrace 1,1\rBrace}\big{\rBrace}},{\big{\lBrace}{\lBrace 0,0\rBrace},{\lBrace 0,1\rBrace}\big{\rBrace}}\big{)}$
	$\displaystyle=\big{(}{\big{\lBrace}{\lBrace 0,1\rBrace},{\lBrace 1,1\rBrace}\big{\rBrace}},{\big{\lBrace}{\lBrace 0,1\rBrace},{\lBrace 0,0\rBrace}\big{\rBrace}}\big{)}$
	$\displaystyle=\langle\mathcal{B}\mathcal{B}\chi_{{\{1,2\}}},\mathcal{B}\mathcal{B}\chi_{{\{2\}}}\rangle\big{(}{\big{\lBrace}{\lBrace 0,2\rBrace},{\lBrace 1,1\rBrace}\big{\rBrace}}\big{)}$

Here, we use ${\lBrace\cdots\rBrace}$ to denote multisets, so ${\lBrace 0,1\rBrace}={\lBrace 1,0\rBrace}$ but ${\lBrace 1\rBrace}\neq{\lBrace 1,1\rBrace}$ .

3.

The identity functor $X\mapsto X$ is both zippable [46] and cancellative (4.2).
4.

The monoid-valued functor ${\mathcal{P}_{\textsf{f}}}={\mathbb{B}}^{(-)}$ is zippable [46], but not cancellative (4.1), because ${\mathbb{B}}$ is a non-cancellative monoid.

The functor $\mathcal{P}\mathcal{P}$ is neither zippable [46, Ex. 5.10] nor cancellative because

	$\displaystyle\langle\mathcal{P}\mathcal{P}\chi_{{\{1,2\}}},\mathcal{P}\mathcal{P}\chi_{{\{2\}}}\rangle(\big{\{}{\{0\}},{\{2\}}\big{\}})$	$\displaystyle=({\big{\{}{\{0\}},{\{1\}}\big{\}}},{\big{\{}{\{0\}},{\{1\}}\big{\}}})$
		$\displaystyle=\langle\mathcal{P}\mathcal{P}\chi_{{\{1,2\}}},\mathcal{P}\mathcal{P}\chi_{{\{2\}}}\rangle(\big{\{}{\{0\}},{\{1\}},{\{2\}}\big{\}}).$

Every functor $F$ satisfying $|F(2+2)|>1$ and $|F3|=1$ is cancellative but not zippable:

•

Indeed, every map with domain $1$ is injective, in particular the map

$\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle\colon 1\cong F3\longrightarrow F2\times F2,$

whence $F$ is cancellative.

•

If $|F(2+2)|>1$ and $|F3|=1$ we have that the map

\langle 2+\mathord{!},\mathord{!}+2\rangle\colon\underbrace{F(2+2)}_{|-|\mathrlap{\,>1}}\to\underbrace{F(2+1)}_{\cong F3\cong 1}\times\underbrace{F(1+2)}_{\cong F3\cong 1}\cong 1

is not injective, whence $F$ is not zippable.

An example for such a functor is given by

FX=\{S\subseteq X:|S|=0\text{ or }|S|=4\}

(10)

which sends a map $f\colon X\to Y$ to the map $Ff\colon FX\to FY$ defined by

Ff(S)=\begin{cases}f[S]&\text{if }|f[S]|=4\\ \emptyset&\text{otherwise}.\end{cases}

For the proof of

F\text{ zippable }\&\leavevmode\nobreak\ F\text{ cancellative }\leavevmode\nobreak\ \leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ F\text{ $m$-zippable }\qquad\text{for all }m\in\mathbb{N}

recall from König et al. [32] that a functor $F$ is $m$ -zippable if the canonical map

\mathsf{unzip}_{m}\colon\leavevmode\nobreak\ \leavevmode\nobreak\ F(A_{1}+A_{2}+\ldots+A_{m})\leavevmode\nobreak\ \leavevmode\nobreak\ \longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ F(A_{1}+1)\times F(A_{2}+1)\times\ldots\times F(A_{m}+1)

is injective. Formally, $\mathsf{unzip}_{m}$ is given by

\langle F[\Delta_{i,j}]_{j\in\bar{m}}\rangle_{i\in\bar{m}}\colon\leavevmode\nobreak\ \leavevmode\nobreak\ F\coprod_{j=1}^{m}A_{j}\longrightarrow\prod_{i=1}^{m}F(A_{i}+1)

where $\bar{m}$ is the set $\bar{m}={\{1,\ldots,m\}}$ and the map $\Delta_{i,j}$ is defined by

\Delta_{i,j}\colon A_{j}\to A_{i}+1\qquad\Delta_{i,j}:=\begin{cases}A_{j}\xrightarrow{\mathsf{in}_{1}}A_{i}+1&\text{if }i=j\\ A_{j}\xrightarrow{!}1\xrightarrow{\mathsf{in}_{2}}A_{i}+1&\text{if }i\neq j.\end{cases}

First, we show that for a zippable and cancellative functor $F$ , the map

g_{A,B}\leavevmode\nobreak\ \leavevmode\nobreak\ :=\leavevmode\nobreak\ \leavevmode\nobreak\ F(A+1+B)\xrightarrow{\langle F(A+!),F(!+B)\rangle}F(A+1)\times F(1+B)

is injective for all sets $A,B$ . Indeed, we have the following chain of injective maps, where the index at the $1$ is only notation to distinguish coproduct components more easily:

	$\displaystyle F(A+(1_{M}+B))$
	$\displaystyle\quad\leavevmode\hbox to9.36pt{\vbox to11.11pt{\pgfpicture\makeatletter\hbox{\hskip 4.67966pt\lower-5.55557pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-2.54428pt}{5.55557pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\rightarrowtail$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{}{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\langle F(A+!),F(!+(1_{M}+B))\rangle$		( $F$ is zippable)
	$\displaystyle F(A+1)\times F(1_{A}+1_{M}+B)$
	$\displaystyle\quad\leavevmode\hbox to9.36pt{\vbox to11.11pt{\pgfpicture\makeatletter\hbox{\hskip 4.67966pt\lower-5.55557pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-2.54428pt}{5.55557pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\rightarrowtail$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{}{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathsf{id}\times\langle F(!+B),F(1_{A}+1_{M}+!)\rangle$		( $F$ is zippable)
	$\displaystyle F(A+1)\times F(1+B)\times F(1_{A}+1_{M}+1_{B})$
	$\displaystyle\quad\leavevmode\hbox to9.36pt{\vbox to11.11pt{\pgfpicture\makeatletter\hbox{\hskip 4.67966pt\lower-5.55557pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-2.54428pt}{5.55557pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\rightarrowtail$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{}{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathsf{id}\times\mathsf{id}\times\langle F\chi_{1_{M}+1_{B}},F\chi_{1_{B}}\rangle$		( $F$ is cancellative, $1_{A}+1_{M}+1_{B}\cong\{0,1,2\}$ )
	$\displaystyle F(A+1)\times F(1+B)\times F2\times F2$

Call this composition $f$ . The injective map $f$ factors through $g_{A,B}$ , because it matches with $g_{A,B}$ on the components $F(A+1)$ and $F(1+B)$ , and for the other components, one has the map

h\leavevmode\nobreak\ :=\leavevmode\nobreak\ F(A+1)\times F(1+B)\xrightarrow{F\chi_{1}\times F\chi_{B}}F2\times F2

with $f=\langle\mathsf{id}_{F(A+1)\times F(1+B)},h\rangle\cdot g_{A,B}$ . Since $f$ is injective, $g_{A,B}$ must be injective, too.

Also note that a function $F$ is cancellative iff equivalently the map

\langle F(1+!),F(!+1)\rangle\colon F(1+1+1)\longrightarrow F(1+1)\times F(1+1)

is injective, for $!\colon 1+1\to 1$ and $1+1+1\cong 3$ and $1+1\cong 2$ .

We now proceed with the proof of the desired implication by induction on $m$ . In the base cases $m=0$ and $m=1$ there is nothing to show because every functor is $0$ - and $1$ -zippable, and for $m=2$ , the implication is trivial (zippability and $2$ -zippability are identical properties). In the inductive step, given that $F$ is $2$ -zippable, $m$ -zippable ( $m\geq 2$ ), and cancellative, we show that $F$ is $(m+1)$ -zippable.

We have the following chain of injective maps, where we again annotate some of the singleton sets $1$ with indices to indicate from which coproduct components they come:

	$\displaystyle F(A_{1}+\ldots+A_{m-1}+(A_{m}+A_{m+1}))$
	$\displaystyle\qquad\leavevmode\hbox to9.36pt{\vbox to11.11pt{\pgfpicture\makeatletter\hbox{\hskip 4.67966pt\lower-5.55557pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-2.54428pt}{5.55557pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\rightarrowtail$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{}{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathsf{unzip}_{m}$	( $F$ is $m$ -zippable)
	$\displaystyle\prod_{i=1}^{m-1}F(A_{i}+1)\times F(A_{m}+A_{m+1}+1_{1..(m-1)})$
$\displaystyle\cong\leavevmode\nobreak\$	$\displaystyle\prod_{i=1}^{m-1}F(A_{i}+1)\times F(A_{m}+1_{1..(m-1)}+A_{m+1})$
	$\displaystyle\quad\leavevmode\hbox to9.36pt{\vbox to11.11pt{\pgfpicture\makeatletter\hbox{\hskip 4.67966pt\lower-5.55557pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-2.54428pt}{5.55557pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\rightarrowtail$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{}{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}{\mathsf{id}\times g_{A_{m},A_{m+1}}}$	(the above injective helper map $g$ )
	$\displaystyle\prod_{i=1}^{m-1}F(A_{i}+1)\times F(A_{m}+1)\times F(1+A_{m+1})$
$\displaystyle\cong\leavevmode\nobreak\$	$\displaystyle\prod_{i=1}^{m-1}F(A_{i}+1)\times F(A_{m}+1)\times F(A_{m+1}+1)$

This composition thus is injective as well, and in fact the composition is precisely $\mathsf{unzip}_{m+1}$ , showing that $F$ is $(m+1)$ -zippable. ∎

The optimization present in the algorithms for Markov chains [44] and automata [27] can now be adapted to coalgebras for cancellative functors, where it suffices to split only according to transitions into $S$ , neglecting transitions into $B\setminus S$ . More formally, this means that we replace the three-valued $\chi_{S}^{B}\colon C\to 3$ with $\chi_{S}\colon C\to 2$ in the refinement step (A3):

Proposition A.14.

Let $F$ be a cancellative set functor. For $S\in C/P_{i}$ in the $i$ -th iteration of 3.1, we have $P_{i+1}=P_{i}\cap\ker(C\xrightarrow{c}{FC}\xrightarrow{F\chi_{S}}F2).$

Proof of A.14.

From the definition (1) of the kernel, we immediately obtain the following properties for all maps $f,g\colon Y\to Z$ , $h\colon X\to Y$ :

$\displaystyle f\text{ injective}\leavevmode\nobreak\ \leavevmode\nobreak\$	$\displaystyle\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \ker(f\cdot h)=\ker(h)$	(11)
$\displaystyle\ker(f)=\ker(g)\leavevmode\nobreak\ \leavevmode\nobreak\$	$\displaystyle\Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\ \ker(f\cdot h)=\ker(g\cdot h)$	(12)
$\displaystyle\ker(\langle f,g\rangle)$	$\displaystyle=\ker(f)\cap\ker(g).$	(13)

For every coalgebra $c\colon C\to FC$ and $S\subseteq B\subseteq C$ we have

\langle F\chi_{B},F\chi_{S}\rangle=\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle\cdot F\chi_{S}^{B}.

Since $F$ is cancellative, $\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle$ is injective, and we thus obtain

\ker(\langle F\chi_{B},F\chi_{S}\rangle)=\ker(\langle F\chi_{{\{1,2\}}},F\chi_{{\{2\}}}\rangle\cdot F\chi_{S}^{B})\overset{\text{\eqref{kerInjective}}}{=}\ker(F\chi_{S}^{B}).

(14)

By (12), this implies that

\ker(\langle F\chi_{B},F\chi_{S}\rangle\cdot c)=\ker(F\chi_{S}^{B}\cdot c).

(15)

Let $B\in C/Q_{i}$ be the block that is split into $S$ and $B\setminus S$ in iteration $i$ . Since $P_{i}$ is finer than $Q_{i}$ and $B\in C/Q_{i}$ , we have $P_{i}\subseteq Q_{i}\subseteq\ker(F\chi_{B}\cdot c)$ ; thus:

P_{i}=P_{i}\cap\ker(C\xrightarrow{c}{FC}\xrightarrow{F\chi_{B}}F2).

(16)

Now we verify the desired property:

$\displaystyle P_{i+1}$	$\displaystyle=\leavevmode\nobreak\ P_{i}\cap\ker(C\xrightarrow{c}{FC}\xrightarrow{F\chi_{S}^{B}}F2)$	(by (A3))
	$\displaystyle\overset{\mathclap{\text{}}}{=}\leavevmode\nobreak\ P_{i}\cap\ker(\langle F\chi_{B},F\chi_{S}\rangle\cdot c)$	(by (15))
	$\displaystyle=P_{i}\cap\ker(\langle F\chi_{B}\cdot c,F\chi_{S}\cdot c\rangle)$	(def. $\langle-,-\rangle$ )
	$\displaystyle=P_{i}\cap\ker(F\chi_{B}\cdot c)\cap\ker(F\chi_{S}\cdot c)$	(by (13))
	$\displaystyle=P_{i}\cap\ker(F\chi_{S}\cdot c)$	(by (16))

This completes the proof. ∎

Example A.15.

For coalgebras for a signature functor $\Sigma$ or a monoid-valued functor $M^{(-)}$ for cancellative $M$ , the refinement step (A3) of 3.1 can be optimized to compute $P_{i+1}$ according to A.14.

Observe that, in the optimized step (A3), $B$ is no longer mentioned. It is therefore unsurprising that we do not need a certificate for it when constructing certificates for the blocks of $P_{i+1}$ . Instead, we can reflect the map $F\chi_{S}\cdot c\colon C\to F2$ in the coalgebraic modal formula and take $F2$ as the (unary) modal operators. Just like $F1$ in 3.5, the set $F2$ canonically embeds into $F3$ :

Proof of Theorem 4.3.

Before proving Theorem 4.3, we define a new set of (unary) modalities (A.16), establish a lemma about its semantics (A.17), fully phrase the entire optimized algorithm (A.19), and then show its correctness (Theorem A.21).

Notation A.16.

Define the injective map $j_{2}\colon 2\rightarrowtail 3$ by $j_{2}(0)=1$ and $j_{2}(1)=2$ . Then the injection $Fj_{2}\colon F2\rightarrowtail F3$ provides a way to interpret elements $t\in F2$ as unary modalities ${\ulcorner t\urcorner}$ :

{\ulcorner t\urcorner}(\delta):={\ulcorner Fj_{2}(t)\urcorner}(\delta,\top).

Remark to A.16.

There are several different ways to define ${\ulcorner t\urcorner}(\delta)$ for $t\in F2$ , depending on the definition of the inclusion $j_{2}$ .

$j_{2}\colon 2\rightarrowtail 3$	$j_{2}\cdot\chi_{S}$ for $S\subseteq C$	Definition for $t\in F2$
$0\mapsto 0,1\mapsto 1$	$j_{2}\cdot\chi_{S}=\chi_{\emptyset}^{S}$	${\ulcorner t\urcorner}(\delta):={\ulcorner Fj_{2}(t)\urcorner}(\bot,\delta)$
$0\mapsto 0,1\mapsto 2$	$j_{2}\cdot\chi_{S}=\chi_{S}^{S}$	${\ulcorner t\urcorner}(\delta):={\ulcorner Fj_{2}(t)\urcorner}(\delta,\delta)$
$0\mapsto 1,1\mapsto 2$	$j_{2}\cdot\chi_{S}=\chi_{S}^{C}$	${\ulcorner t\urcorner}(\delta):={\ulcorner Fj_{2}(t)\urcorner}(\delta,\top)$

All these variants make the following A.17 true because in any case:

{\ulcorner t\urcorner}(\delta)={\ulcorner Fj_{2}(t)\urcorner}(\phi,\psi)\qquad\text{implies}\qquad j_{2}\cdot\chi_{\llbracket\delta\rrbracket}=\chi_{\llbracket\phi\rrbracket}^{\llbracket\psi\rrbracket}.

(17)

Analogously to 3.4 we can show:

Lemma A.17.

Given a cancellative functor $F$ , an $F$ -coalgebra $(C,c)$ , $t\in F2$ , a formula $\delta$ , and $x\in C$ , we have $x\in\llbracket{\ulcorner t\urcorner}(\delta)\rrbracket$ if and only if $F\chi_{\llbracket\delta\rrbracket}(c(x))=t$ .

In 3.7, the family $\beta$ is only used in the definition of $\delta_{i+1}$ to characterize the larger block $B$ that has been split into the smaller blocks $S\subseteq B$ and $B\setminus S$ . For a cancellative functor, we can replace

{\ulcorner F\chi_{S}^{B}(c(x))\urcorner}(\delta_{i}(S),\beta_{i}(B))\quad\text{ with }\quad{\ulcorner F\chi_{S}(c(x))\urcorner}(\delta_{i}(S))

in the definition of $\delta_{i+1}$ . Hence, we can omit $\beta_{i}$ from 3.7 altogether, obtaining the following algorithm, which is again based on coalgebraic partition refinement (3.1).

Proof A.18 (Proof of A.17).

Since we put $j_{2}\colon 2\rightarrowtail 3$ with $j_{2}(0)=1$ and $j_{2}(1)=2$ , we have $j_{2}\cdot\chi_{S}=\chi_{S}^{C}$ for all $S\subseteq C$ .

$\displaystyle\llbracket{\ulcorner t\urcorner}(\delta)\rrbracket$	$\displaystyle=\llbracket{\ulcorner Fj_{2}(t)\urcorner}(\delta,\top)\rrbracket$	(A.16)
	$\displaystyle=\{x\in C\mid F\chi_{\llbracket\delta\rrbracket}^{C}(c(x))=Fj_{2}(t)\}$	(3.4, $\llbracket\top\rrbracket=C$ )
	$\displaystyle=\{x\in C\mid Fj_{2}(F\chi_{\llbracket\delta\rrbracket}(c(x)))=Fj_{2}(t)\}$	( $\chi_{\llbracket\delta\rrbracket}^{C}=j_{2}\cdot\chi_{\llbracket\delta\rrbracket}$ )
	$\displaystyle=\{x\in C\mid F\chi_{\llbracket\delta\rrbracket}(c(x))=t\}$	( $Fj_{2}$ injective)

In the last step, we use that $F$ preserves injective maps (subsection 2.1)

Algorithm A.19.

We extend 3.1 as follows. Initially, define

\delta_{0}([x]_{P_{0}})={\ulcorner F!(c(x))\urcorner}.

In the $i$ -th iteration, extend step (A3) by the additional assignment

(A $\!{}^{\prime}$ 1)

$\delta_{i+1}([x]_{P_{i+1}})=\begin{cases}\delta_{i}([x]_{P_{i}})&\text{if }[x]_{P_{i+1}}=[x]_{P_{i}}\\ \delta_{i}([x]_{P_{i}})\wedge{\ulcorner F\chi_{S}(c(x))\urcorner}(\delta_{i}(S))&\text{otherwise.}\\ \end{cases}$

The certificates thus computed are reduced to roughly half the size compared to 3.7; the asymptotic run time and formula size (subsection 3.5) remain unchanged. More importantly:

Remark 13.

The certificates constructed by A.19 do not contain negation (or disjunction); they are built from $\top$ , conjunction $\wedge$ , and unary modal operators ${\ulcorner t\urcorner}$ for $t\in F2$ (the nullary operators ${\ulcorner t\urcorner}$ for $t\in F1$ embed into $F2$ ).

Proof A.20 (Details on 13).

Define the injective map $j_{12}\colon 1\rightarrowtail 2$ by $j_{12}(0)=1$ . Hence, we can also embed the nullary $t\in F1$ into $F2$ :

{\ulcorner t\urcorner}={\ulcorner Fj_{12}(t)\urcorner}(\top)\qquad\text{(cf.\leavevmode\nobreak\ \autoref{notationF2Mod})}.

This is compatible with the notations established so far because we have $j_{2}\cdot j_{12}=j_{1}\colon 1\rightarrowtail 3$ for the inclusions defined in 3.5 and A.16. Thus, we obtain the same modal operator regardless of whether we embed $t\in F1$ first into $F2$ and from there into $F3$ ( $j_{2}$ , A.16) or directly into $F3$ ( $j_{1}$ , 3.5): ${\ulcorner t\urcorner}={\ulcorner Fj_{12}(t)\urcorner}(\top)={\ulcorner Fj_{2}(Fj_{12}(t))\urcorner}(\top,\top)={\ulcorner Fj_{1}(t)\urcorner}(\top,\top).$

Theorem A.21.

For cancellative functors, A.19 is correct; that is, for all $i\in\mathbb{N}$ we have:

\forall S\in X/P_{i}\colon\llbracket\delta_{i}(S)\rrbracket=S.

Note that the optimized A.19 can also be implemented by directly constructing certificates for the unary modal operators $F2$ . That is, one can treat the modal operators $F2$ as first class citizens, in lieu of embedding them into the set $F3$ as we did in A.16. The only difference between the two implementation approaches w.r.t. the size of the formula dag is one edge per modality, namely the edge to the node $\top$ from the node ${\ulcorner Fj_{2}(F\chi_{S}(c(x)))\urcorner}(\delta_{i}(\delta_{i}),\top)$ , which arises when step 21 is expanded according to A.16.

Proof A.22 (Proof of Theorem A.21).

We prove the desired correctness by induction over $i$ , the index of loop iterations.

The definition of $\delta_{0}$ is identical to the definition in 3.7 whence

\llbracket\delta_{0}(S)\rrbracket=S\qquad\text{for all }S\in C/P_{0},

proved completely analogously as in the proof of Theorem 3.8.

In the $i$ -th iteration with chosen block $S\in C/P_{i}$ , we distinguish two cases, whether a block $[x]_{P_{i+1}}\in C/P_{i+1}$ remains the same or is split into other blocks:

•

If $[x]_{P_{i+1}}=[x]_{P_{i}}$ , then we have

\llbracket\delta_{i+1}([x]_{P_{i}})\rrbracket\overset{\text{\ref{defDeltai1Optimized}}}{=}\llbracket\delta_{i}([x]_{P_{i}})\rrbracket\overset{\text{I.H.}}{=}[x]_{P_{i}}=[x]_{P_{i+1}}.

•

If $[x]_{P_{i+1}}\neq[x]_{P_{i}}$ , we compute as follows:

	$\displaystyle\llbracket\delta_{i+1}([x]_{P_{i+1}})\rrbracket$
$\displaystyle=$	$\displaystyle\llbracket\delta_{i}([x]_{P_{i}})\wedge{\ulcorner F\chi_{S}(c(x))\urcorner}(\delta_{i}(S))\rrbracket$	21
$\displaystyle=$	$\displaystyle\llbracket\delta_{i}([x]_{P_{i}})\rrbracket\cap\llbracket{\ulcorner F\chi_{S}(c(x))\urcorner}(\delta_{i}(S))\rrbracket$
$\displaystyle=$	$\displaystyle[x]_{P_{i}}\cap\llbracket{\ulcorner F\chi_{S}(c(x))\urcorner}(\delta_{i}(S))\rrbracket$	(I.H.)
$\displaystyle=$	$\displaystyle[x]_{P_{i}}\cap\{x^{\prime}\in C\mid F\chi_{\llbracket\delta_{i}(S)\rrbracket}(c(x^{\prime}))=F\chi_{S}(c(x))\}$	(A.17)
$\displaystyle=$	$\displaystyle[x]_{P_{i}}\cap\{x^{\prime}\in C\mid F\chi_{S}(c(x^{\prime}))=F\chi_{S}(c(x))\}$	(I.H.)
$\displaystyle=$	$\displaystyle[x]_{P_{i}}\cap\{x^{\prime}\in C\mid(x,x^{\prime})\in\ker(F\chi_{S}\cdot c)\}$	(def. $\ker$ )
$\displaystyle=$	$\displaystyle[x]_{P_{i}}\cap[x]_{F\chi_{S}\cdot c}$	(def. $[x]_{R}$ )
$\displaystyle=$	$\displaystyle[x]_{P_{i+1}}$

The last step is the block-wise definition of $P_{i+1}=P_{i}\cap\ker(F\chi_{S}\cdot c)$ (see A.14).

Details for section 5 (Domain-Specific Certificates)

Details for 10.

For every set $X$ , define the set ${\mathcal{B}\!\ell}(X)$ as terms $K$ over the grammar

K::=X\leavevmode\nobreak\ |\leavevmode\nobreak\ \neg K\leavevmode\nobreak\ |\leavevmode\nobreak\ K\wedge K.

(18)

There is an obvious way to evaluate boolean combinations of predicates using the maps

e_{X}\colon{\mathcal{B}\!\ell}(2^{X})\to 2^{X}

defined inductively as follows:

e_{X}(S\subseteq X)=X,\qquad e_{X}(\neg K)=X\setminus K,\qquad e_{X}(K_{1}\wedge K_{2})=K_{1}\cap K_{2}.

Given a signature $\Lambda$ of modal operators $\lambda$ and corresponding predicate liftings $\llbracket\lambda\rrbracket$ , we can combine all of them. To this end, write $\Lambda$ for the corresponding signature functor (cf. subsection 2.1.3); we define a family of maps $\llbracket\Lambda\rrbracket_{X}$ as follows:

\llbracket\Lambda\rrbracket_{X}\colon\Lambda(2^{X})=\coprod_{\mathord{\raisebox{1.0pt}{$\scriptstyle\lambda$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$\scriptstyle n$}}}\in\Lambda}(2^{X})^{n}\xrightarrow{\leavevmode\nobreak\ \big{[}\llbracket\lambda\rrbracket\big{]}_{\lambda\in\Lambda}\leavevmode\nobreak\ }2^{FX}.

Since every $\llbracket\lambda\rrbracket_{X}\colon(2^{X})^{n}\to 2^{FX}$ is natural in $X$ , so is $\llbracket\Lambda\rrbracket_{X}$ . We can replace $\Lambda$ with the signature

\Lambda^{\prime}:=\coprod_{n\in\mathbb{N}}{\mathcal{B}\!\ell}(\Lambda({\mathcal{B}\!\ell}(n))),

where $\mathsf{in}_{n}(K)\in\Lambda^{\prime}$ , $K\in{\mathcal{B}\!\ell}(\Lambda({\mathcal{B}\!\ell}(n)))$ has the arity $n$ . Observe that ${\mathcal{B}\!\ell}$ is functorial; in fact, it is the (free or term) monad for the signature functor $\Sigma X=X+X\times X$ associated to the grammar in (18). Thus ${\mathcal{B}\!\ell}\cdot\Lambda\cdot{\mathcal{B}\!\ell}$ is a functor, too. Applying the Yoneda-Lemma to this functor, we have for every $\mathord{\raisebox{1.0pt}{$t$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Lambda^{\prime}$ the (natural) family of maps $\alpha^{t}$ :

\alpha^{t}_{X}\colon X^{n}\to{\mathcal{B}\!\ell}(\Lambda({\mathcal{B}\!\ell}(X)))\qquad\text{for every set }X.

Hence, we obtain a predicate lifting for $t$ by defining:

\llbracket t\rrbracket_{X}\colon\!\!\leavevmode\hbox to304.02pt{\vbox to19.8pt{\pgfpicture\makeatletter\hbox{\hskip 152.0075pt\lower-9.75955pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-152.0075pt}{-9.65971pt}\pgfsys@invoke{ }\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip 17.24788pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.94234pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\big{(}(2^{X})^{n}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 17.24788pt\hfil&\hfil\hskip 53.98427pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-29.7618pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\mathcal{B}\!\ell}(\Lambda({\mathcal{B}\!\ell}(2^{X})))}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 34.06734pt\hfil&\hfil\hskip 45.30365pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.08118pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\mathcal{B}\!\ell}(\Lambda(2^{X}))}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 25.38672pt\hfil&\hfil\hskip 40.13197pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.9095pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\mathcal{B}\!\ell}(2^{FX})}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 20.21504pt\hfil&\hfil\hskip 35.1736pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.95113pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${2^{FX}\big{)}.}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip 15.25667pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-117.31175pt}{-7.15971pt}\pgfsys@lineto{-98.19478pt}{-7.15971pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-97.9948pt}{-7.15971pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-110.51445pt}{-2.9714pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{\alpha^{t}_{2^{X}}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-29.26015pt}{-7.15971pt}\pgfsys@lineto{-10.14317pt}{-7.15971pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.94319pt}{-7.15971pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-33.92447pt}{2.6336pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{{\mathcal{B}\!\ell}(\Lambda(e_{X}))}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{41.43022pt}{-7.15971pt}\pgfsys@lineto{60.5472pt}{-7.15971pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{60.74718pt}{-7.15971pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{35.86781pt}{2.6336pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{{\mathcal{B}\!\ell}(\llbracket\Lambda\rrbracket_{X})}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{101.77724pt}{-7.15971pt}\pgfsys@lineto{120.89421pt}{-7.15971pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{121.0942pt}{-7.15971pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{100.70181pt}{2.6336pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{{\mathcal{B}\!\ell}(e_{FX})}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}

It is a composition of natural transformations and so is itself natural in $X$ .

Definition 14.

Given a modal signature $\Lambda$ for a functor $F$ , a simple domain-specific interpretation consists of functions $\tau\colon F1\to\bar{\Lambda}$ and $\kappa\colon F2\to\bar{\Lambda}$ assigning a nullary modality $\tau_{o}$ to each $o\in F1$ and a unary modality $\kappa_{s}$ to each $s\in F2$ such that the predicate liftings $\llbracket\tau_{o}\rrbracket_{X}\in 2^{FX}$ and $\llbracket\kappa_{s}\rrbracket\colon 2^{X}\to 2^{FX}$ satisfy

\llbracket\tau_{o}\rrbracket_{1}=\{f\}\quad\text{(in $2^{F1}$)}\qquad\text{and}\qquad[s]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}(\{1\})=\{s\}\qquad\text{(in $2^{F2}$).}

Proposition A.23.

Let $\Lambda$ be a modal signature for a cancellative functor $F$ , and $(\tau,\kappa)$ a simple domain-specific interpretation. Define $\lambda\colon F3\to\bar{\Lambda}$ by $\lambda_{t}(\delta,\rho)=\kappa_{F\chi_{{\{2\}}}(t)}(\delta)$ . Then $(\tau,\lambda)$ is a domain-specific interpretation.

Proof A.24.

We verify that $(\tau,\lambda)$ is a domain-specific interpretation (11) by verifying that for every $t\in F3$ , defining

\tau_{t}(\delta,\rho)=\kappa_{F\chi_{{\{2\}}}(t)}(\delta)

satisfies

[t]_{F\chi_{\{1,2\}}}\cap\llbracket\tau_{t}\rrbracket_{3}(\{2\},\{1\})=\{t\}\qquad\text{in $2^{F3}$}.

In the following, we put $s:=F\chi_{{\{2\}}}(t)\in F2$ . By the naturality of the predicate lifting of $\kappa_{s}$ , the following square commutes (recall that $2^{(-)}$ is contravariant):

(19)

We thus have:

$\displaystyle\llbracket\tau_{t}\rrbracket_{3}({\{2\}},{\{1\}})$	$\displaystyle=\llbracket\kappa_{s}\rrbracket_{3}({\{2\}})$	(def. $\tau_{t}$ )
	$\displaystyle=\llbracket\kappa_{s}\rrbracket_{3}(\chi_{{\{2\}}}^{-1}[{\{1\}}])$	(def. $\chi_{{\{2\}}}$ )
	$\displaystyle=\llbracket\kappa_{s}\rrbracket_{3}(2^{\chi_{{\{2\}}}}({\{1\}}))$	(def. $2^{(-)}$ )
	$\displaystyle=2^{F\chi_{{\{2\}}}}(\llbracket\kappa_{s}\rrbracket_{2}({\{1\}}))$	(by (19))
	$\displaystyle=\{t^{\prime}\in F3\mid F\chi_{{\{2\}}}(t^{\prime})\in\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})\}$

For every $t^{\prime}\in F3$ , we have

	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\cap\llbracket\tau_{t}\rrbracket_{3}(\{2\},\{1\})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }t^{\prime}\in\llbracket\tau_{t}\rrbracket_{3}(\{2\},\{1\})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})$	(by the above calculation)
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in[F\chi_{{\{2\}}}(t^{\prime})]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})$	( $\ker$ reflexive)
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in[F\chi_{{\{2\}}}(t)]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})$	( $t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in[s]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})$	(def. $s$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in\{s\}$	(assumption on $\kappa_{s}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{\{1,2\}}}\text{ and }F\chi_{{\{2\}}}(t^{\prime})\in\{F\chi_{{\{2\}}}(t)\}$	(def. $s$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F\chi_{\{1,2\}}(t^{\prime})=F\chi_{\{1,2\}}(t)\text{ and }F\chi_{{\{2\}}}(t^{\prime})=F\chi_{{\{2\}}}(t)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle\langle F\chi_{\{1,2\}},F\chi_{\{2\}}\rangle(t^{\prime})=\langle F\chi_{\{1,2\}},F\chi_{\{2\}}\rangle(t)$	(def. $\langle-,-\rangle$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}=t$	( $F$ cancellative)

Note that $\langle F\chi_{\{1,2\}},F\chi_{\{2\}}\rangle$ is injective because $F$ is cancellative.

Details for 5.1.

(a)

We verify that 5.1.1 indeed provides domain-specific certificate (11). For $t\in\mathcal{P}3$ , we have

\lambda_{t}(\delta,\rho)\leavevmode\nobreak\ =\leavevmode\nobreak\ \begin{cases}\neg\Diamond\rho&\text{if }2\in t\not\mkern 1.0mu\ni 1\\ \Diamond\delta\wedge\Diamond\rho&\text{if }2\in t\ni 1\\ \neg\Diamond\delta&\text{if }2\not\in t\ni 1\\ \top&\text{if }2\not\in t\not\mkern 1.0mu\ni 1\\ \end{cases}

We proceed by the following case distinction:

•

If $1\notin\mathcal{P}\chi_{{\{1,2\}}}(t)$ , then $t=\emptyset$ or $t=\{0\}$ . In both cases we have $[t]_{\mathcal{P}\chi_{1,2}}=\{t\}$ . Since $\lambda_{t}(\delta,\rho)=\top$ ,

$[t]_{\mathcal{P}\chi_{1,2}}\cap\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}})=\{t\}$

as desired.

•

If $1\in\mathcal{P}\chi_{{\{1,2\}}}(t)$ , then $2\in t$ or $1\in t$ . This yields

	$\displaystyle 2\in t\not\mkern 1.0mu\ni 1$	$\displaystyle\Longrightarrow\leavevmode\nobreak\ \llbracket\overbrace{(\delta,\rho)\mapsto\mathrlap{\neg\Diamond\rho}\phantom{\Diamond\delta\wedge\Diamond\rho}}^{\textstyle\lambda_{t}}\rrbracket_{3}({\{2\}},{\{1\}})=\{t^{\prime}\in F3\mid 1\notin t^{\prime}\}$
	$\displaystyle 2\in t\ni 1$	$\displaystyle\Longrightarrow\leavevmode\nobreak\ \llbracket(\delta,\rho)\mapsto\Diamond\delta\wedge\Diamond\rho\rrbracket_{3}({\{2\}},{\{1\}})=\{t^{\prime}\in F3\mid 2\in t^{\prime}\text{ and }1\in t^{\prime}\}$
	$\displaystyle 2\notin t\ni 1$	$\displaystyle\Longrightarrow\leavevmode\nobreak\ \llbracket(\delta,\rho)\mapsto\mathrlap{\neg\Diamond\delta}\phantom{\Diamond\delta\wedge\Diamond\rho}\rrbracket_{3}({\{2\}},{\{1\}})=\{t^{\prime}\in F3\mid 2\notin t^{\prime}\}$

Consequently, we have for every $t^{\prime}\in\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}})$ that

\text{$1\in t$ iff $1\in t^{\prime}$}\qquad\text{and}\qquad\text{$2\in t$ iff $2\in t^{\prime}$}.

To conclude, note that if $t^{\prime}\in[t]_{\mathcal{P}\chi_{{\{1,2\}}}}$ then $0\in t^{\prime}$ iff $0\in t$ . Thus

[t]_{\mathcal{P}\chi_{\{1,2\}}}\cap\llbracket\lambda_{t}\rrbracket_{3}(\{2\},\{1\})=\{t\}.

(b)

5.1.2: For the verification for signature functors, define a helper map $v\colon\Sigma 2\to{\mathcal{P}_{\textsf{f}}}\mathbb{N}$ by $v(\sigma(x_{1},\ldots,x_{n}))$ $=\{i\in\mathbb{N}\mid x_{i}=1\}$ . The predicate lifting for the (unary) modal operator ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\raisebox{-1.0pt}{$\scriptstyle I$}$}}\rangle}$ , for $I\subseteq\mathbb{N}$ , is obtained from A.1 by the predicate $f_{I}\colon\Sigma 2\to 2$ corresponding to the set

f_{I}=\{t\in\Sigma 2\mid v(t)=I\}.

This gives rise to the predicate lifting

	$\displaystyle\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\raisebox{-1.0pt}{$\scriptstyle I$}$}}\rangle}\rrbracket_{X}(P)$	$\displaystyle=\{t\in\Sigma X\mid F\chi_{P}(t)\in f_{I}\}$		(A.1)
		$\displaystyle=\{t\in\Sigma X\mid v(F\chi_{P}(t))=I\}.$		(def. $f_{I}$ )

Similarly, for the nullary modal operator $\sigma$ (for the $n$ -ary operation symbol $\mathord{\raisebox{1.0pt}{$\sigma$}\mkern-1.5mu/\mkern-1.5mu{\raisebox{-1.0pt}{$n$}}}\in\Sigma$ ), take $\Sigma 1\to 2$ given by the set

g_{\sigma}=\{\sigma(0,\ldots,0)\}

(noting that $2^{0}=1$ ). This gives rise to the predicate lifting

$\displaystyle\llbracket\sigma\rrbracket_{X}$	$\displaystyle=\{t\in\Sigma X\mid F!(t)\in g_{\sigma}\}$	(A.1)
	$\displaystyle=\big{\{}t\in\Sigma X\mid F\chi_{P}(t)\in\{\sigma(0,\ldots,0)\}\big{\}}$	(def. $g_{\sigma}$ )
	$\displaystyle=\{\sigma(x_{1},\ldots,x_{n})\mid x_{1},\ldots,x_{n}\in X\}.$

For the verification of the (simple) domain-specific interpretation (14), we put

\kappa_{s}(\delta):={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}v(s)$}}\rangle}\delta\qquad\text{for }s\in\Sigma 2

with then induces the claimed $\lambda_{t}$ via A.23:

\lambda_{\sigma(x_{1},\ldots,x_{n})}(\delta,\rho)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}\{i\in\mathbb{N}\mid x_{i}=2\}$}}\rangle}\delta\qquad\text{for }\sigma(x_{1},\ldots,x_{n})\in\Sigma 3

There is nothing to show for $\tau_{o}:=\sigma$ since it has the correct semantics by the definition of $\llbracket\sigma\rrbracket_{1}$ . Note that $\langle F!,v\rangle\colon\Sigma 2\to\Sigma 1\times{\mathcal{P}_{\textsf{f}}}\mathbb{N}$ is injective because for every $s\in\Sigma 2$ the operation symbol and all its parameters (from $2$ ) are uniquely determined by $F!(s)$ and $v(s)$ . For $\kappa_{s}:={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}v(s)$}}\rangle}$ , $s\in F2$ , we have

[s]_{F!}=\{s^{\prime}\in F2\mid F!(s)=F!(s^{\prime})\}.

Thus, we compute

	$\displaystyle[s]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s^{\prime}\in\Sigma 2\mid s^{\prime}\in[s]_{F!}\text{ and }s^{\prime}\in\llbracket\kappa_{s}\rrbracket_{2}({\{1\}})\}$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s^{\prime}\in\Sigma 2\mid F!(s)=F!(s^{\prime})\text{ and }s^{\prime}\in\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}v(s)$}}\rangle}\rrbracket_{2}({\{1\}})\}$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s^{\prime}\in\Sigma 2\mid F!(s)=F!(s^{\prime})\text{ and }v(F\chi_{{\{1\}}}(s^{\prime}))=v(s)\}$	(def. $\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}v(s)$}}\rangle}\rrbracket_{2}$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s^{\prime}\in\Sigma 2\mid F!(s)=F!(s^{\prime})\text{ and }v(s^{\prime})=v(s)\}$	( $\mathsf{id}_{2}=\chi_{{\{1\}}}\colon 2\to 2$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s^{\prime}\in\Sigma 2\mid\langle F!,v\rangle(s)=\langle F!,v\rangle(s^{\prime})\}$	(def. $\langle-,-\rangle$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\{s\}$	( $\langle F!,v\rangle$ injective)

(c)

5.1.3: For every $m\in M$ , define the map

f_{m}\colon M^{(2)}\to 2\qquad\text{with}\qquad\{\mu\in M^{(2)}\mid\mu(1)=m\}.

which gives rise to the predicate lifting of the unary modal operator ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}$ :

	$\displaystyle\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}\rrbracket_{X}(P)$	$\displaystyle=\{\mu\in M^{(X)}\mid M^{(P)}(\mu)\in f_{m}\}$		(A.1)
		$\displaystyle=\{\mu\in M^{(X)}\mid M^{(P)}(\mu)(1)=m\}$		(def. $f_{m}$ )

For the verification of the axioms of the domain-specific interpretation (11), we have that $\tau$ satisfies the axiom:

	$\displaystyle\llbracket\tau_{o}\rrbracket_{1}=\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}o(0)$}}\rangle}\top\rrbracket_{1}$	$\displaystyle=\{\mu\in M^{(1)}\mid\sum_{x\in\llbracket\top\rrbracket_{1}}\mu(x)=o(0)\}$
		$\displaystyle=\{\mu\in M^{(1)}\mid\mu(0)=o(0)\}=\{o\}$		( $\llbracket\top\rrbracket_{1}=1=\{0\}$ )

For the other component of the domain-specific interpretation, we proceed by case distinction:

•

If $M$ is non-cancellative, we have $\lambda_{t}(\delta,\rho)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\delta\wedge{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(1)$}}\rangle}\rho$ for $t\in M^{(3)}$ and thus we have for every $t^{\prime}\in M^{(3)}$ :

	$\displaystyle t^{\prime}\in([t]_{F\chi_{{\{1,2\}}}}\cap\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}}))$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\llbracket(\delta,\rho)\mapsto{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\delta\wedge{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(1)$}}\rangle}\rho\rrbracket_{3}({\{2\}},{\{1\}})$	(def. $\lambda_{t}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\rrbracket_{3}({\{2\}})\cap\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(1)$}}\rangle}\rrbracket_{3}({\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(2)$}}\rangle}\rrbracket_{3}({\{2\}})\text{ and }t^{\prime}\in\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}t(1)$}}\rangle}\rrbracket_{3}({\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}(2)=t(2)\text{ and }t^{\prime}(1)=t(1)$	(def. $\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}m$}}\rangle}\rrbracket$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}(0)=t(0)\text{ and }t^{\prime}(1)+t^{\prime}(2)=t(1)+t(2)$
	$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \text{ and }t^{\prime}(2)=t(2)\text{ and }t^{\prime}(1)=t(1)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}(0)=t(0)\text{ and }t^{\prime}(2)=t(2)\text{ and }t^{\prime}(1)=t(1)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}=t$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in\{t\}$

•

If $M$ is cancellative, we put $\kappa_{s}(\delta)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}s(1)$}}\rangle}\,\delta$ for $s\in M^{(2)}$ , which then induces $\lambda_{t}(\delta,\rho)={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}s(2)$}}\rangle}\,\delta$ via A.23. We verify 14 for all $s^{\prime}\in M^{(2)}$ :

	$\displaystyle s^{\prime}\in([s]_{F!}\cap\llbracket\kappa_{s}\rrbracket_{2}(\{1\}))$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle s^{\prime}\in[s]_{F!}\text{ and }s^{\prime}\in\llbracket\kappa_{s}\rrbracket_{2}(\{1\})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F!(s^{\prime})=F!(s)\text{ and }s^{\prime}\in\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}s(1)$}}\rangle}\rrbracket_{2}(\{1\})$	(def. $\kappa_{s}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F!(s^{\prime})=F!(s)\text{ and }\sum_{x\in\{1\}}s^{\prime}(x)=s(1)$	(def. ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}s(1)$}}\rangle}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F!(s^{\prime})=F!(s)\text{ and }s^{\prime}(1)=s(1)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle s^{\prime}(0)+s^{\prime}(1)=s(0)+s(1)\text{ and }s^{\prime}(1)=s(1)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle s^{\prime}(0)=s(0)\text{ and }s^{\prime}(1)=s(1)$	( $M$ cancellative)
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle s^{\prime}=s$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle s^{\prime}\in\{s\}$

(d)

5.1.4: For $FX=({\mathcal{D}}X+1)^{A}$ , the predicate lifting of $\langle a\rangle_{p}$ , $a\in A$ , $p\in[0,1]$ is:

\llbracket\langle a\rangle_{p}\rrbracket_{X}(S):=\{\text{if }t\in FX\mid p>0\text{ then }t(a)\in{\mathcal{D}}X\text{ and }\sum_{x\in S}t(a)(x)\geq p\}

first note that

\llbracket\langle a\rangle_{1}\top\rrbracket_{1}=\{o\in F1\mid o(a)\in{\mathcal{D}}1\}\qquad\text{ and }\qquad\llbracket\neg\langle a\rangle_{1}\top\rrbracket_{1}=\{o\in F1\mid o(a)\in 1\}.

Thus, we have:

	$\displaystyle\llbracket\tau_{o}\rrbracket_{1}$	$\displaystyle=\big{\llbracket}\bigwedge_{\begin{subarray}{c}a\in A\\ o(a)\in{\mathcal{D}}1\end{subarray}}\langle a\rangle_{1}\top\wedge\bigwedge_{\begin{subarray}{c}a\in A\\ o(a)\in 1\end{subarray}}\neg\langle a\rangle_{1}\top\big{\rrbracket}_{1}$
		$\displaystyle=\bigcap_{\begin{subarray}{c}a\in A\\ o(a)\in{\mathcal{D}}1\end{subarray}}\{o^{\prime}\in F1\mid o^{\prime}(a)\in{\mathcal{D}}1\}\cap\bigcap_{\begin{subarray}{c}a\in A\\ o(a)\in 1\end{subarray}}\{o^{\prime}\in F1\mid o^{\prime}(a)\in 1\}=\{o\}$

For the axiom of $\lambda_{t}$ , $t\in F3=({\mathcal{D}}3+1)^{A}$ , we verify for all $t^{\prime}\in F3$ , where the crucial step is the arithmetic argument for replacing the inequalities by equalities:

	$\displaystyle t^{\prime}\in([t]_{F\chi_{{\{1,2\}}}}\cap\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}}))$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\llbracket\lambda_{t}\rrbracket_{3}({\{2\}},{\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\big{\llbracket}(\delta,\rho)\mapsto\bigwedge_{\begin{subarray}{c}a\in A\\ t(a)\in{\mathcal{D}}3\end{subarray}}(\langle a\rangle_{t(a)(2)}\,\delta\wedge\langle a\rangle_{t(a)(1)}\,\rho)\big{\rrbracket}_{3}({\{2\}},{\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\bigcap_{\begin{subarray}{c}a\in A\\ t(a)\in{\mathcal{D}}3\end{subarray}}\llbracket(\delta,\rho)\mapsto\langle a\rangle_{t(a)(2)}\,\delta\wedge\langle a\rangle_{t(a)(1)}\,\rho\rrbracket_{3}({\{2\}},{\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }t^{\prime}\in\bigcap_{\begin{subarray}{c}a\in A\\ t(a)\in{\mathcal{D}}3\end{subarray}}\llbracket\langle a\rangle_{t(a)(2)}\rrbracket_{3}({\{2\}})\cap\llbracket\langle a\rangle_{t(a)(1)}\rrbracket_{3}({\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }\forall a\in A,t(a)\in{\mathcal{D}}3:t^{\prime}\in\llbracket\langle a\rangle_{t(a)(2)}\rrbracket_{3}({\{2\}})\cap\llbracket\langle a\rangle_{t(a)(1)}\rrbracket_{3}({\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{{\{1,2\}}}}\text{ and }\forall a\in A,t(a)\in{\mathcal{D}}3:t^{\prime}(a)(2)\geq t(a)(2)\wedge t^{\prime}(a)(1)\geq t(a)(1)$	(Def. $\llbracket\langle a\rangle p\rrbracket$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle\forall a\in A\colon(t^{\prime}(a)\in 1\leftrightarrow t(a)\in 1)\text{ and if }a\in{\mathcal{D}}3\text{ then:}$
	$\displaystyle\qquad t^{\prime}(a)(0)=t(a)(0),\leavevmode\nobreak\ \leavevmode\nobreak\ t^{\prime}(a)(1)+t^{\prime}(a)(2)=t(a)(1)+t(a)(2),$
	$\displaystyle\qquad t^{\prime}(a)(2)\geq t(a)(2),\leavevmode\nobreak\ \leavevmode\nobreak\ t^{\prime}(a)(1)\geq t(a)(1)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle\forall a\in A\colon(t^{\prime}(a)\in 1\leftrightarrow t(a)\in 1)\text{ and if }a\in{\mathcal{D}}3\text{ then:}$
	$\displaystyle\qquad t^{\prime}(a)(0)=t(a)(0),\leavevmode\nobreak\ \leavevmode\nobreak\ t^{\prime}(a)(1)=t(a)(2),\leavevmode\nobreak\ \leavevmode\nobreak\ t^{\prime}(a)(2)=t(a)(2)$	(arithmetic)
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle\forall a\in A\colon(t^{\prime}(a)\in 1\leftrightarrow t(a)\in 1)\text{ and if }a\in{\mathcal{D}}3\text{ then }t^{\prime}(a)=t(a)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in{\{t\}}$

Proof of 5.2.

Lemma A.25.

Let $(\tau,\lambda)$ be a domain-specific interpretation for $F$ . For all $t\in FC$ and $S\subseteq B\subseteq C$ we have:

\big{(}[t]_{F\chi_{B}}\leavevmode\nobreak\ \cap\leavevmode\nobreak\ \llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{C}(S,B\setminus S)\big{)}=[t]_{F\chi_{S}^{B}}\qquad\text{in $2^{FC}$.}

Proof A.26.

Put $d:=F\chi_{S}^{B}(t)$ ; the naturality square of $\llbracket\lambda_{d}\rrbracket$ for $\chi_{S}^{B}\colon C\to 3$ is

Hence:

	$\displaystyle(F\chi_{S}^{B})^{-1}\big{[}\llbracket\lambda_{d}\rrbracket_{3}({\{2\}},{\{1\}})\big{]}$	$\displaystyle=\llbracket\lambda_{d}\rrbracket_{C}((\chi_{S}^{B})^{-1}[{\{2\}}],(\chi_{S}^{B})^{-1}[{\{1\}}])$
		$\displaystyle=\llbracket\lambda_{d}\rrbracket_{C}(B,B\setminus S).$		( $*$ )

Now we verify for every $t^{\prime}\in FC$ that

	$\displaystyle t^{\prime}\in\big{(}[t]_{F\chi_{B}}\leavevmode\nobreak\ \cap\leavevmode\nobreak\ \llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{C}(S,B\setminus S)\big{)}$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{B}}\text{ and }t^{\prime}\in\llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{C}(S,B\setminus S)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{B}}\text{ and }t^{\prime}\in(F\chi_{S}^{B})^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{3}({\{2\}},{\{1\}})\big{]}$	( $*$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F\chi_{S}^{B}(t^{\prime})\in[F\chi_{S}^{B}(t)]_{F\chi_{{\{1,2\}}}}\text{ and }F\chi_{S}^{B}(t^{\prime})\in\llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{3}({\{2\}},{\{1\}})$	( $\chi_{{\{1,2\}}}\cdot\chi_{S}^{B}=\chi_{B}$ )
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F\chi_{S}^{B}(t^{\prime})\in[F\chi_{S}^{B}(t)]_{F\chi_{{\{1,2\}}}}\cap\llbracket\lambda_{F\chi_{S}^{B}(t)}\rrbracket_{3}({\{2\}},{\{1\}})$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F\chi_{S}^{B}(t^{\prime})\in\{F\chi_{S}^{B}(t)\}$	(11)
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle F\chi_{S}^{B}(t^{\prime})=F\chi_{S}^{B}(t)$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\$	$\displaystyle t^{\prime}\in[t]_{F\chi_{S}^{B}}.$

Proof A.27 (Proof of 5.2).

We prove by induction over the index $i$ of main loop iterations that $T(\delta_{i}([x]_{P_{i}}))$ and $T(\beta_{i}([x]_{Q_{i}}))$ are a certificates for $[x]_{P_{i}}$ and $[x]_{Q_{i}}$ , respectively. (In the cancellative case, $Q_{i}$ and $\beta_{i}$ are not defined; so just put $C/Q_{i}=\{C\}$ , $\beta_{i}(C)=\top$ for convenience.)

(a)

For $i=0$ , we trivially have

\llbracket T(\beta_{0}([x]_{P_{i}}))\rrbracket=\llbracket T(\top)\rrbracket=\llbracket\top\rrbracket=C.

Furthermore, unravelling 3.5,

\delta_{0}([x]_{P_{0}})={\ulcorner F!(c(x))\urcorner}={\ulcorner Fj_{1}(F!(c(x)))\urcorner}(\top,\top).

Consequently,

T(\delta_{0}([x]_{P_{0}}))=\tau_{F!(Fj_{1}(F!(c(x))))}=\tau_{F!(c(x))}

using $!\cdot j_{1}\cdot\mathord{!}=\mathord{!}\colon C\to 1$ . The naturality of $\llbracket\tau_{o}\rrbracket$ , $o\in F1$ , implies that $\llbracket\tau_{o}\rrbracket_{X}=\{t\in FX\mid F!(t)=o\}$ . Hence,

\llbracket T(\delta_{0}([x]_{P_{0}}))\rrbracket=c^{-1}[\llbracket\tau_{F!(c(x))}\rrbracket_{C}]=\{x^{\prime}\in C\mid F!(c(x^{\prime}))=F!(c(x))\}=[x]_{P_{0}}.

(b)

In the inductive step, there is nothing to show for $\beta_{i+1}$ because it is only a boolean combination of $\beta_{i}$ and $\delta_{i}$ . For $\delta_{i+1}$ , we distinguish two cases: whether the class $[x]_{P_{i}}$ is refined or not. If $[x]_{P_{i+1}}=[x]_{P_{i}}$ , then

\llbracket T(\delta_{i+1}([x]_{P_{i+1}}))\rrbracket=\llbracket T(\delta_{i}([x]_{P_{i}}))\rrbracket=[x]_{P_{i}},

and we are done. Now suppose that $[x]_{P_{i+1}}\neq[x]_{P_{i}}$ in the $i$ -th iteration with chosen $S\subsetneqq B\subseteq C$ . By (A’3) resp. 21 we have:

\delta_{i+1}([x]_{P_{i+1}})=\delta_{i}([x]_{P_{i}})\wedge{\ulcorner t\urcorner}(\delta_{i}(S),\beta^{\prime})

where $\beta^{\prime}$ is $\beta_{i}(B)$ or $\top$ ; in any case $\llbracket\delta_{i}(S)\rrbracket=S\subseteq\llbracket\beta^{\prime}\rrbracket$ . Note that $t$ here is either $F\chi_{S}^{B}(c(x))$ (3.7) or $Fj_{2}(F\chi_{S}(c(x)))$ (A.19). Put $B^{\prime}=B$ in the first case and $B^{\prime}=C$ else. Using $\chi_{S}^{C}=j_{2}\cdot\chi_{S}$ , we see that

t=F\chi_{S}^{B^{\prime}}(c(x))\qquad\llbracket\beta^{\prime}\rrbracket=B^{\prime},\qquad\text{and}\qquad\llbracket T(\beta^{\prime})\rrbracket=B^{\prime},

where the last equation follows from the inductive hypothesis. Thus, we have

\delta_{i+1}([x]_{P_{i+1}})=\delta_{i}([x]_{P_{i}})\wedge{\ulcorner F\chi_{S}^{B^{\prime}}(c(x))\urcorner}(\delta_{i}(S),\beta^{\prime}),

and therefore

T(\delta_{i+1}([x]_{P_{i+1}}))=T(\delta_{i}([x]_{P_{i}}))\wedge\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\big{(}T(\delta_{i}(S)),T(\beta^{\prime})\wedge\neg T(\delta_{i}(S))\big{)}.

Moreover, we have

P_{i+1}=P_{i}\cap\ker(F\chi_{S}^{B^{\prime}}\cdot c),

in the first case by item (A3), in the second case by A.14, recalling that $\chi_{S}=\chi_{S}^{C}$ .

We are now prepared for our final computation:

	$\displaystyle\llbracket T(\delta_{i+1}([x]_{P_{i+1}}))\rrbracket$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\llbracket T(\delta_{i}([x]_{P_{i}}))\wedge\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}(T(\delta_{i}(S)),T(\beta^{\prime})\wedge\neg T(\delta_{i}(S)))\rrbracket$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\llbracket T(\delta_{i}([x]_{P_{i}}))\rrbracket\cap\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}(T(\delta_{i}(S)),T(\beta^{\prime})\wedge\neg T(\delta_{i}(S)))\rrbracket$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle\llbracket T(\delta_{i}([x]_{P_{i}}))\rrbracket\cap c^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(\llbracket T(\delta_{i}(S))\rrbracket,\llbracket T(\beta^{\prime})\rrbracket\cap C\setminus\llbracket T(\delta_{i}(S))\rrbracket)\big{]}$	(Semantics of $\heartsuit$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap c^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(S,B^{\prime}\cap C\setminus S)\big{]}$	(I.H.)
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap c^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(S,B^{\prime}\setminus S)\big{]}$	( $B^{\prime}\cap C\setminus S=B^{\prime}\setminus S$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap[x]_{F\chi_{B^{\prime}}\cdot c}\cap c^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(S,B^{\prime}\setminus S)\big{]}$	( $P_{i}\subseteq\ker F\chi_{B^{\prime}}\cdot c$ )
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap c^{-1}\big{[}[c(x)]_{F\chi_{B^{\prime}}}\big{]}\cap c^{-1}\big{[}\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(S,B^{\prime}\setminus S)\big{]}$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap c^{-1}\big{[}[c(x)]_{F\chi_{B^{\prime}}}\cap\llbracket\lambda_{F\chi_{S}^{B^{\prime}}(c(x))}\rrbracket_{C}(S,B^{\prime}\setminus S)\big{]}$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap c^{-1}\big{[}[c(x)]_{F\chi_{S}^{B^{\prime}}}\big{]}$	(domain-specific interpret. (A.25))
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i}}\cap[x]_{F\chi_{S}^{B^{\prime}}\cdot c}$
$\displaystyle=\leavevmode\nobreak\$	$\displaystyle[x]_{P_{i+1}}$	( $P_{i+1}=P_{i}\cap\ker(F\chi_{S}^{B^{\prime}}\cdot c$ ))

This completes the proof.

Details for 5.3.

The 3.7 runs in $\mathcal{O}(m\cdot\log n)$ producing certificates of a total size of $\mathcal{O}(m\cdot\log n)$ . When translating these certificates for the modalities $\langle a\rangle_{p}$ by the translation $T$ , we obtain certificates for the input coalgebra (5.2). However, the formula size has a blow up by the additional factor $|A|$ because of the big conjunctions in the domain-specific interpretation (5.1.4).

This represents is a better run time than that of the algorithm by Desharnais et al. [17, Fig. 4], which nests multiple loops: four loops over blocks all blocks seen so far and one loop over $A$ , roughly leading to a total run time in $\mathcal{O}(|A|\cdot n^{4})$ .

Details for section 6 (Worst Case Tree Size of Certificates)

Details for 12.

To verify the minimality of $\varphi=\Diamond^{n+2}\top$ , one considers all possible replacements of subformulae of $\varphi$ by $\top$ :

\Diamond\top\qquad\Diamond\Diamond\top\qquad\ldots\qquad\Diamond^{n}\top\qquad\Diamond^{n+1}\top

All of these hold at both $x$ and $y$ , because $x$ can perform arbitrarily many transitions and $y$ can perform $n+1$ transitions.

We note additionally that even the optimized algorithm for cancellative functors (cf. A.19) constructs certificates of exponential worst-case tree size:

Example A.28.

Define the $\mathbb{R}^{(-)}$ -coalgebra $c$ on $C=\bigcup_{k\in\mathbb{N}}\{w_{k},x_{k},y_{k},z_{k}\}$ by

\begin{array}[]{r@{\,}l@{\,}l@{\,}l@{\,}l@{\qquad\qquad}r@{}c@{\,}c@{\,}r}c(w_{k+1})=&\{w_{k}\mapsto 1,&x_{k}\mapsto 2,&y_{k}\mapsto 1,&z_{k}\mapsto 2\}&c(w_{0})=\{&w_{0}&\mapsto&1\}\\ c(x_{k+1})=&\{w_{k}\mapsto 1,&x_{k}\mapsto 2,&y_{k}\mapsto 2,&z_{k}\mapsto 1\}&c(x_{0})=\{&x_{0}&\mapsto&2\}\\ c(y_{k+1})=&\{w_{k}\mapsto 2,&x_{k}\mapsto 1,&y_{k}\mapsto 1,&z_{k}\mapsto 2\}&c(y_{0})=\{&y_{0}&\mapsto&3\}\\ c(z_{k+1})=&\{w_{k}\mapsto 2,&x_{k}\mapsto 1,&y_{k}\mapsto 2,&z_{k}\mapsto 1\}&c(z_{0})=\{&z_{0}&\mapsto&4\}\end{array}

The optimized A.19 constructs a certificate of size $2^{k}$ in the $k$ -th layer. In this example, however, linear-sized certificates do exist for all states, e.g.

\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}2$}}\rangle}{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}3$}}\rangle}^{k}({\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}\top\vee{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\top)\rrbracket={\{x_{k+1}\}}.

Details for A.28.

Define the $\mathbb{R}^{(-)}$ -coalgebra $c\colon C\to\mathbb{R}^{(C)}$ on the carrier

C:=4\times\mathbb{N}\cong\bigcup{\big{\{}L_{k}\mid k\in\mathbb{N}\big{\}}}\qquad\text{for }L_{k}={\{w_{k},x_{k},y_{k},z_{k}\}}.

We put

\begin{array}[]{r@{\,}l@{\,}l@{\,}l@{\,}l@{\qquad\qquad}r@{}c@{\,}c@{\,}r}c(w_{k+1})=&\{w_{k}\mapsto 1,&x_{k}\mapsto 2,&y_{k}\mapsto 1,&z_{k}\mapsto 2\}&c(w_{0})=\{&w_{0}&\mapsto&1\}\\ c(x_{k+1})=&\{w_{k}\mapsto 1,&x_{k}\mapsto 2,&y_{k}\mapsto 2,&z_{k}\mapsto 1\}&c(x_{0})=\{&x_{0}&\mapsto&2\}\\ c(y_{k+1})=&\{w_{k}\mapsto 2,&x_{k}\mapsto 1,&y_{k}\mapsto 1,&z_{k}\mapsto 2\}&c(y_{0})=\{&y_{0}&\mapsto&3\}\\ c(z_{k+1})=&\{w_{k}\mapsto 2,&x_{k}\mapsto 1,&y_{k}\mapsto 2,&z_{k}\mapsto 1\}&c(z_{0})=\{&z_{0}&\mapsto&4\}\end{array}

For the complexity class of the formulae generated, consider the subcoalgebra on $L_{0}\cup\cdots\cup L_{n}$ .

The initial partition $P_{0}={\big{\{}{\{w_{0}\}},{\{x_{0}\}},{\{y_{0}\}},{\{z_{0}\}},L_{1}\cup\cdots L_{n}\big{\}}}$ distinguishes on the total out-degree (being 1, 2, 3, 4, or 6). Consider that after $i\in\mathbb{N}$ iterations of the main loop of the algorithm, the states $w_{k},x_{k},y_{k},z_{k}$ have just been found to be behaviourally different and all states of $L_{k+1}\cup\cdots\cup L_{n}$ are still identified. Then the algorithm has to use some of the blocks ${\{w_{k}\}}$ , ${\{x_{k}\}}$ , ${\{y_{k}\}}$ , ${\{z_{k}\}}$ as the splitter $S$ for further refinement. Assume wlog that $S:=\{w_{k}\}$ is used as the splitter, first. This will have the effect that $L_{k+1}\cup\cdots\cup L_{n}$ will be refined into the blocks

\{w_{k+1},x_{k+1}\},\qquad\{y_{k+1},z_{k+1}\},\qquad L_{k+2}\cup\cdots\cup L_{n}.

Assume, that the formula for $w_{k}$ is $\delta({\{w_{k}\}})$ at this point (we omit the index, since the singleton block ${\{w_{k}\}}$ can not be refined further). The definition of $\delta$ in the algorithm annotates the block $\{w_{k+1},x_{k+1}\}$ with ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}\delta({\{w_{k}\}})$ and the block $\{y_{k+1},z_{k+1}\}$ with ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}2$}}\rangle}\delta({\{w_{k}\}})$ .

Splitting by $\{x_{k}\}$ does not lead to further refinement. However, when splitting by $S:=\{y_{k}\}$ (or equivalently $\{z_{k}\}$ ), ${\{w_{k+1},x_{k+1}\}}$ is split into ${\{w_{k+1}\}}$ and ${\{x_{k+1}\}}$ and likewise ${\{y_{k+1},z_{k+1}\}}$ into ${\{y_{k+1}\}}$ and ${\{z_{k+1}\}}$ . Let $\delta({\{y_{k}\}})$ be the certificate constructed for ${\{y_{k}\}}$ . This implies that the formulas for ${\{w_{k+1}\}}$ and ${\{y_{k+1}\}}$ are respectively extended by the conjunct ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}\delta({\{y_{k}\}})$ ; likewise, the formulas for ${\{x_{k+1}\}}$ and ${\{z_{k+1}\}}$ obtain a new conjunct ${\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}2$}}\rangle}\delta{\{y_{k}\}}$ . Hence, for every $s\in L_{k+1}$ the tree-size of the formula constructed is at least:

|\delta({\{s\}})|\geq|\delta({\{w_{k}\}})|+|\delta({\{y_{k}\}})|.

Thus the tree-size of the certificate constructed for cancellative functors may grow exponentially with the state count.

Despite the exponential tree-size of the formulas constructed, there exist linearly sized certificates for all states in the above coalgebra $(C,c)$ . First, we have

\phi_{k}:={\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}3$}}\rangle}^{k}({\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}\top\vee{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\top)\text{ with }\llbracket\phi_{k}\rrbracket={\{w_{k},z_{k}\}}

This lets us define certificates for $x_{k+1}$ and $y_{k+1}$ :

\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}2$}}\rangle}\phi_{k}\rrbracket={\{x_{k+1}\}}\quad\text{and}\quad\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\phi_{k}\rrbracket={\{y_{k+1}\}}

For the remaining two state sequences $w$ and $z$ we first note

\llbracket{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\phi_{k}\rrbracket={\{w_{k+2},y_{k+2}\}}

and thus have certificates

\llbracket\phi_{k+2}\wedge{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\phi_{k}\rrbracket={\{w_{k+2}\}}\quad\text{and}\quad\llbracket\phi_{k+2}\wedge\neg{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}1$}}\rangle}{\langle{\raisebox{1.0pt}{$\scriptstyle\mathord{=}4$}}\rangle}\phi_{k}\rrbracket={\{z_{k+2}\}}.

Since $\phi_{k}$ involves $k+2$ modal operators, every state in $L_{k}$ has a certificate with at most $2\cdot k+8$ modal operators.

Explaining Behavioural Inequivalence Generically in Quasilinear Time

Abstract

keywords:

1 Introduction

Related Work

2 Preliminaries

Notation \thetheorem (Partitions).

2.1 Coalgebra

Definition \thetheorem.

Example \thetheorem.

Definition \thetheorem.

Example \thetheorem.

Remark \thetheorem.

2.2 Coalgebraic Logics

Syntax

Example \thetheorem.

Semantics

Example \thetheorem.

Proposition 2.1 (Adequacy [38, 42]).

3 Constructing Distinguishing Formulae

Definition 1.

3.1 Paige-Tarjan with Certificates

3.2 Generic Partition Refinement

Algorithm 3.1 ([46, Alg. 4.9, (5.1)]).

Definition 2 ([46]).

Remark 3.

Theorem 3.2 ([46, Thm 4.20, 5.20]).

3.3 Generic Modal Operators

Definition 4.

Example 3.3.

Lemma 3.4.

Notation 3.5.

Lemma 3.6.

3.4 Algorithmic Construction of Certificates

Algorithm 3.7.

Remark 5.

Theorem 3.8.

Corollary 3.9 (Hennessy-Milner).

Remark 6.

3.5 Complexity Analysis

Definition 3.10.

Theorem 3.11.

Theorem 3.12.

Remark 7.

Theorem 3.13.

4 Cancellative Functors

Definition 8.

Proposition 4.1.

Proposition 4.2.

Remark 9.

Theorem 4.3.

Corollary 4.4.

5 Domain-Specific Certificates

Definition 10.

Definition 11.

Example 5.1.

Proposition 5.2.

Example 5.3.

6 Worst Case Tree Size of Certificates

Open Problem 6.1.

Remark 12.

7 Conclusions and Further Work

References

Appendix A Appendix: Omitted Proofs

Details for section 2 (Preliminaries)

Details for subsection 2.1.

Details on Predicate Liftings in subsection 2.2.

Lemma A.1.

Proof A.2.

Details for section 3 (Constructing Distinguishing Formulae)

Verification of 4.

Proof of 3.4.

Proof of 3.6.

Proof of Theorem 3.8.

Details for 6.

Proof of Theorem 3.11.

Lemma A.3.

Proof A.4.

Lemma A.5.

Proof A.6.

Explaining Behavioural Inequivalence Generically
in Quasilinear Time