Abstract 1 Introduction 2 Syntax 3 Operational Semantics 4 Axioms 5 Completeness 6 Decidability and Complexity 7 Related Work 8 Conclusion References

Weighted GKAT: Completeness and Complexity

Spencer Van Koevering ORCID Cornell University, Ithaca, NY, USA Wojciech Różowski ORCID University College London, UK Alexandra Silva ORCID Cornell University, Ithaca, NY, USA
Abstract

We propose Weighted Guarded Kleene Algebra with Tests (wGKAT), an uninterpreted weighted programming language equipped with branching, conditionals, and loops. We provide an operational semantics for wGKAT using a variant of weighted automata and introduce a sound and complete axiomatization. We also provide a polynomial time decision procedure for bisimulation equivalence.

Keywords and phrases:
Weighted Programming, Automata, Axiomatization, Decision Procedure
Category:
Track B: Automata, Logic, Semantics, and Theory of Programming
Funding:
Spencer Van Koevering: Partially supported by a Cornell Bowers CIS Deans Excellence Fellowship.
Wojciech Różowski: Partially supported by ERC grant Autoprobe (grant agreement 101002697).
Alexandra Silva: Partially supported by ONR grant N68335-22-C-0411, ERC grant 101002697, and a Royal Society Wolfson fellowship.
Copyright and License:
[Uncaptioned image] © Spencer Van Koevering, Wojciech Różowski, and Alexandra Silva; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation Models of computation
Related Version:
Full Version: http://arxiv.org/abs/2504.20385 [13]
Editors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis

1 Introduction

Weighted programming is a recently introduced paradigm [1] in which computational branches of programs are associated with quantities. For example, the program e2535f does e with weight 25 and f with weight 35. Semantically, each branch is executed, its results scaled, and then results of different branches added. If we were to interpret weights as probabilities and use addition of real numbers, then the above example would be a classic randomized program: a biased coin flip. If we interpret the weights as costs rather than probabilities, and addition as minimum rather than traditional addition, then e2535f would model selecting the cheapest resulting branch and be well suited for optimization problems.

Weighted programs can model problems from a variety of domains, including optimization, model checking, and combinatorics [1]. However, reasoning about their behavior is difficult as different interpretations of the weights lead to different properties of the programs and their semantics, impacting, for instance, whether the equivalence of weighted programs is decidable. In this paper, we propose an algebraic approach to reason about equivalence of weighted programs and devise a decision procedure which applies to a large class of weights.

The starting point of our development is Guarded Kleene Algebra with Tests (GKAT) [25], an algebraic framework for reasoning about equivalence of uninterpreted imperative programs. Its equational axiomatization offers a simple framework for deductive reasoning, and it also has a decision procedure. We propose and axiomatize a GKAT-inspired weighted programming language, wGKAT, which enables reasoning about the equivalence of deterministic, uninterpreted programs with weighted branching. We design this language with the goals of offering an equational axiomatization and a polynomial-time decision procedure for the equivalence of expressions, both derived uniformly for a broad class of weights.

One of the primary challenges we address is identifying a suitable class of semirings which is sufficient to prove that bisimulation is a complete proof technique for behavioural equivalence and, moreover, to define a operational semantics of loops. Using this class of semirings we were able to generalize traditional arguments for soundness and completeness from process algebra to our setting [23]. Another challenge is the decidability of equivalence for weighted programs, which hinges on properties of the semiring as well. We leverage existing work on monoid labeled transition systems to design the operational semantics and establish that equivalence up to bisimilarity is decidable for wGKAT.

Our work was developed concurrently with another weighted variant of Kleene Algebra with Tests, called Kleene Algebra with Weights and Tests (KAWT) [24]. KAWT lacks a decision procedure and admits only a restrictive class of weights. The key difference in our work that enables us to significantly enlarge the class of weights we can consider is that KAWT extends KAT directly whereas our starting point is GKAT, the deterministic fragment of KAT. This is what allows us to offer a decision procedure and a sound and complete axiomatization: by carefully selecting the class of weights we retain the general road map to soundness and completeness of GKAT as well as the efficient decision procedure.

In a nutshell, our contributions are as follows.

  1. 1.

    We propose a weighted version of GKAT and equip it with an operational semantics using a variant of weighted automata (Sections 2 and 3).

  2. 2.

    We identify a class of semirings for which the semantics of weighted loops can be computed when considering bisimulation equivalence (Section 3.2).

  3. 3.

    We axiomatize bisimulation equivalence for wGKAT and provide a proof soundness (Section 4) and a proof of completeness (Section 5).

  4. 4.

    We design a decision procedure for bisimilarity which runs in O(n3log2n) time if the number of tests is fixed, where n is the size of the programs considered (Section 6).

We conclude and discuss directions for future work in Section 8. Omitted proofs appear in the full version [13].

2 Syntax

e,fExp pAct do p
bBExp assert b
e+bf if b do e else do f
e;f do e then do f
e(b) while b do e
vOut return v
ersf do e with weight r and f with weight s

Figure 1: Syntax of wGKAT.

In this section, we introduce the syntax of our language and examples on how to use it to model simple quantitative programs. The syntax of wGKAT (Figure 1) is two-sorted, consisting of the set Exp of expressions containing a sort BExp of Boolean expressions also called tests. Intuitively, Exp represents the overall syntax of weighted programs, while BExp is used to specify assertions, as well as conditional expressions appearing in the scope of if-then-else and while constructs. Given a finite set T of primitive tests, we define BExp, the grammar of tests, to be given by the following:

b,cBExp01tTb¯b+cbc

In the above, 0 and 1 respectively represent false and true, ¯ denotes negation, + represents disjunction and juxtaposition is conjunction. We will write BA to denote Boolean equivalence in BExp. Logical entailment defines a preorder given by bBAcb+cBAc. The quotient of BExp by the relation BA, denoted by BExp/BA is in one-to-one correspondence with the Boolean Algebra freely generated by the set T. The entailment [b]BA[c]BAbBAc defines a partial order on BExp/BA. The minimal nonzero elements in that order are called atoms and we will write At for the set of them.

The syntax of wGKAT is parametric on two fixed sets: Act of uninterpreted program actions and Out of possible return values. The first five constructs in Figure 1, namely uninterpreted program actions, Boolean assertions, conditionals, sequential composition and while loops capture the syntax of GKAT. The return values are inherited from ProbGKAT [21] and intuitively correspond to the return operation from imperative programming languages.

The new syntactic construct in wGKAT is weighted choice denoted by ersf. Intuitively, given two programs e and f, ersf represents a program that runs e with the weight of r and f with the weight of s. To lighten up notation, we will follow a convention that sequential composition binds tighter than weighted choice. Moreover, we define a scaling operation as the following syntactic sugar for a program that immediately continues with the weight of r.

Definition 2.1 (Scaling).

r1r0 0

As a notational convention, scaling will take the highest precedence out of all wGKAT operators.

Weights in the aforementioned syntactic constructs are drawn from the set R equipped with a structure of a semiring. The usage of semirings for modeling weighted computation has been standard in automata theory, program semantics and verification communities [5]. We start by recalling the appropriate definitions concerning semirings.

Definition 2.2 ([8]).

A semiring (R,+,,0,1) is a nonempty carrier set R equipped with two monoid structures interacting in the suitable way.

  1. 1.

    (R,+,0) is a commutative monoid with identity 0

  2. 2.

    (R,,1) is a monoid with identity element 10

  3. 3.

    a(b+c)=ab+ac and (b+c)a=ba+ca for all a,b,cR

  4. 4.

    0a=0=a0 for all a in R

We will abuse the notation and write multiplication in (R,,1) as juxtaposition; additionally we will write R to denote the whole algebraic structure when the operations defined on the carrier are clear from the context. Note that additive and multiplicative identities of the semiring (respectively denoted by 0 and 1) are distinct from false and true tests (respectively denoted by 0 and 1).

Classic examples of semirings include (non-negative) reals/rationals with addition and multiplication and the tropical semiring of extended non-negative natural numbers (denoted by +), where the addition is given by pairwise minimum and semiring multiplication is a sum of extended natural numbers.

Later, we will consider semirings subject to some mild algebraic constraints, allowing us to meaningfully define an operational model for wGKAT programs, in particular with loops. We will make those constraints precise in further sections. Before we do so, we first give two examples of problems that could be encoded using the syntax that we have just described.

Example 2.1 (Ski Rental [1]).

Consider the problem of a person going on a ski trip for n days. Each day they either rent skis for a cost of 1, or they buy them for a cost of y and no longer have the need to rent. We can encode the situation of making this choice on the trip lasting n days, via the following wGKAT expression over the tropical semiring:

(11yv)n;v

Here, for positive n, we write en the n-fold sequential composition of the expression eExp.

Essentially, we perform at most n choices between paying 1 and immediately terminating upon paying y. The immediate termination is represented using a return value v.

Example 2.2 (Coin Game).

Consider the problem of playing a game where a coin is flipped and if it is heads the player wins a dollar and the game continues but if it is tails no money is won and the game ends. How much money should a player expect to make? To model expected value we will use weights to represent both values and probabilities. If we let $⃝ be a return value representing the outcome of winning a dollar, then we can encode this situation via the following wGKAT expression over the semiring of extended non-negative rationals:

((111(1;$⃝)).5.5(0;$⃝))(1)

The while true makes the program continue to execute until some terminating output is reached. We interpret the choice weights as probabilities. The outer weighted choice captures the coin flip, so each branch executes with probability .5. The inner weighted choice is slightly different, it represents an “and”. Each branch executes with probability 1. This can be thought of as similar to concurrently executing both branches rather than nondeterministically choosing one. The intuitive difference stems from the fact that addition in the rationals is not idempotent. The weights in the scalings represent the value of the outcome $⃝, it is how many dollars the player wins.

3 Operational Semantics

In this section, we present an operational semantics for wGKAT using a variant of weighted automata [5], which are akin to GKAT automata [25], where additionally each transition carries a weight taken from a semiring. Before we formally introduce our operational model, we recall the necessary definitions concerning weighted transitions.

For a set X and a fixed semiring 𝕊, define ω(X)={φφ:X𝕊,𝗌𝗎𝗉𝗉(φ) is finite}. Here, 𝗌𝗎𝗉𝗉 refers to the support of a function given by supp(ν)={xX|ν(x)0}. Elements of the set ω(X) are functions ν:X𝕊 which we will refer to as weightings on X over 𝕊. We can view these as formal sums over X with coefficients from 𝕊 or, alternatively, as a generalization of finitely supported distributions obtained by replacing probabilities in an unit interval with weights taken from a semiring and by dropping the normalization requirement. Because of this analogy, given an element xX, we can define an analog of Dirac delta specialized to weightings, namely δx:X𝕊, which maps its argument to the semiring multiplicative identity 1 if it is equal to x, and the semiring additive identity 0 otherwise. Given a set AX, we will write ν[A]xAν(x) for the total weight of the set A under the weighting ν. Moreover, any function h:Xω(Y) can be uniquely extended to a function 𝗅𝗂𝗇(h):ω(X)ω(Y), called the linearization of h, given by

𝗅𝗂𝗇(h)(φ)(y)=xXφ(x)h(x)(y)

Crucially, the above satisfies the property that 𝗅𝗂𝗇(h)δ=h, where δ:Xω(X) is defined by δ(x)=δx. A categorically minded reader might observe that weightings are precisely free semimodules over 𝕊 and hence form a monad on the category of sets. The linerization 𝗅𝗂𝗇(h) is the unique 𝕊-semimodule homomorphism of the type ω(X)ω(Y), that allows to factor h through δ. This is a consequence of a free-forgetful adjunction between the category of sets and the category of 𝕊-semimodules.

wGKAT automata.

A wGKAT automaton is a pair (X,β) consisting of a set of states X and a transition function β:Xω(2+Out+Act×X)At that assigns to each state and a Boolean atom (capturing the current state of the variables) a weighting over three kinds of elements, representing different ways a state might perform a transition:

  • an element of 2={,}, representing immediate acceptance or rejection;

  • an element of Out, representing a return value;

  • a pair consisting of an atomic program action Act and a next state in X, representing performing a labelled transition to a next state.

To lighten up notation, we will write β(x)α instead of β(x)(α).

Example 3.1.

Let X={x1,x2,x3},𝕊=(+,+,,0,1),At={α,β},Act={p1,p2,p3}, Out={v}. We consider a wGKAT automaton (X,τ), whose pictorial representation is below on the left, while the definition of τ is below to the right.

τ(x1)α =4δ+3δ(p1,x2)
τ(x1)β =1δv+5δ(p2,x2)+2δ(p3,x3)
τ(x2)α =τ(x2)β=τ(x3)α=τ(x3)β=15δ

3.1 Operational semantics of Expressions

We are now ready to define the operational semantics of wGKAT expressions: we will construct a wGKAT automaton with transition function :Expω(2+Out+Act×Exp)At, whose states are wGKAT expressions. The semantics of an expression e, will be given by the behavior of the corresponding state in that automaton. This construction is reminiscent of the Brzozowski/Antimirov derivative construction for DFA and NFA respectively. For αAt, we define (e)α by structural induction on e.

Tests, actions, output variables.

Suppose bBExp,vOut,pAct, we let

(b)α={δαBAbδαBAb¯(v)α=δv(p)α=δ(p,)

A test either accepts or aborts with weight 1 depending on whether the given atom entails the truth of the test. An output variable outputs itself with weight 1 and then terminates. An action outputs the atomic program action and then accepts with weight 1, allowing for further computation after the action has been taken. We note here that when we do sequential composition, we will rewire acceptance into the composed expression. For this reason δ can also be thought of as skipping with weight 1.

Guarded Choice.

A guarded choice +b is an if-then-else statement conditioned on b. To capture this, we let e+bf have the outgoing edges of e if αBAb and f otherwise.

(e+bf)α={(e)ααb(f)ααb¯

Weighted Choice.

The intuition here is that the automaton executes both arguments and scales their output by the given quantity. We define ersf as the automaton with all outgoing edges of e, scaled by r, and all outgoing edges of f, scaled by s. The derivative is:

(ersf)α=r(e)α+s(f)α

where these operations are the addition and scalar multiplication of the weightings.

Sequential Composition.

We define the derivative of sequential composition as:

(e;f)α=(e)ααf

where given α and f we let (αf):ω(2+Out+Act×Exp)ω(2+Out+Act×Exp) be the linearization of cα,f:2+Out+Act×Expω(2+Out+Act×Exp), given by:

cα,f(x)={(f)αx=δxx{}Outδ(p,e;f)x=(p,e)

The intuition here is that if e skips, then the behavior of the composition is the behavior of f. If e aborts or returns a value then the derivative is the behavior of e. Finally, if e executes an action and transitions to another state, then the behavior is the next step of e composed with f along with emitting the given action.

Guarded loops.

A desired feature of the semantics of a program that performs loops is that each loop can be equivalently written as a guarded choice between acceptance and performing the loop body followed again by the loop. However, if the loop body could immediately accept, then the loop itself could non-productively accept any number of times before making a productive transition. Each time the loop immediately accepts the computation is scaled again by the weight of acceptance. One can represent this unbounded accumulation of weights through the notion of a fixpoint. There is a well-studied class of semirings featuring such a construct, namely Conway semirings. We first recall the necessary definitions.

Definition 3.1 ([6]).

A semiring 𝕊 is a Conway Semiring if there exists a function :RR such that a,bR

(a+b) =a(ba) (1)
(ab) =1+a(ba)b (2)

We note that the fixpoint rule aa+1=a holds in all Conway Semirings [6, p. 6].

The properties of Conway semirings are enough to guarantee that we can meaningfully define semantics of loops. We will see in Section 4 that these additional identities, Equations 1 and 2 in ˜3.1, play a crucial role in the proof of soundness.

We now define the semantics of loops by iterating the weight of immediate acceptance:

(e(b))α(x)={1x= and αBAb¯(e)α()(e)α(x)x{}Out and αBAb(e)α()(e)α(p,e)x=(p,(e;e(b))) and αBAb0otherwise

The loop could fail the Boolean test and then it just skips and does not execute the loop body (case 1). If the loop passes the test the body executes. Recall that the body might skip with some weight. So in this case the loop must either execute an action (case 3) or terminate (case 2) after some number of iterations. If the loop terminates (case 2) then we scale the weight of termination by the accumulated weight and terminate. If the loop takes an action (case 3), then we scale the weight of the action by the accumulated weight, emit the action, and compose the loop with the next step of e to re-enter the loop once computation of e has finished. We identify the behavior of divergent loops (case 4) with the zero weighting, since they never take a productive action nor terminate. Such a weighting simply assigns the weight zero to all possible branches of the program. This is distinct from the program that asserts false, which immediately aborts with weight one.

We now show that all expressions have a finite number of derivatives. This will be important for the completeness of our axiomatization and decidability of equivalence. We denote the set of states in the automaton reachable from expression e as e.

Lemma 3.1.

For all eExp, e is finite. We bound it by #(e):Exp where

#(b)=1,#(v)=1,#(p)=2,#(ersf)=#(e)+#(f),
#(e+bf)=#(e)+#(f),#(e;f)=#(e)+#(f),#(e(b))=#(e)

3.2 Characterizing Equivalence

We will use bisimilarity as our notion of equivalence. Intuitively, two states of wGKAT automata are bisimilar if at each step of the continuing computation they are indistinguishable to an outside observer. This is a canonical notion of equivalence that is more strict than language equivalence, and will allow us to present an efficient decision procedure in Section 6. We formalize what it means for states to be bisimilar in terms of automaton homomorphisms.

Definition 3.2.

Given two wGKAT automata (X,β),(Y,γ) a function f:XY is a wGKAT homomorphism if for all xX and αAt

  1. 1.

    For any o2+Out   γ(f(x))α(o)=β(x)α(o)

  2. 2.

    For any (p,y)Act×Y   γ(f(x))α(p,y)=β(x)α[{p}×f1(y)]

We concretely instantiate the definition of bisimulation [19] for our automata, for the general version see the full version of the paper [13, Appendix A].

Definition 3.3.

Let (X,β) and (Y,γ) be wGKAT automata. A relation RX×Y is a bisimulation if there exists a transition function ρ:Rω(2+Out+Act×R)At such that the projections π1:RX,π2:RY are wGKAT homomorphisms from (R,ρ) to (X,β) and (Y,γ) respectively. We say the elements xX,yY are bisimilar if there exists a bisimulation R such that (x,y)R.

To be able to build the combined transition structure over R in ˜3.3 we require some additional properties that enable us to refine the original weightings on each set to construct more granular weightings over the relation. We achieve this by requiring that the additive monoid of the semiring has two properties: refinement [26] and positivity [9].

Definition 3.4.

A monoid M is a refinement monoid if x+y=z+w implies that there exist s,t,u,v such that s+t=x,s+u=z,u+v=y,t+v=w. A monoid M with identity e is positive (conical) if for all x,yM, x+y=ex=e=y.

Refinement extends inductively to sums with any (finite) number of summands [26]. Positivity says that no element other than the additive identity has an additive inverse. We now have a full characterization of the semirings we will consider: positive, Conway, and refinement. We offer the following list of semirings as examples for interpretation due to their relevance to weighted programming [1], and assume that all semirings discussed from now on have these three properties.

Corollary 3.1.

The following semirings are positive, Conway, and refinement:

  1. 1.

    Tropical (+,min,+,,0)

  2. 2.

    Arctic (+,max,+,,0)

  3. 3.

    Bottleneck (+,max,min,,)

  4. 4.

    Formal languages (2Γ,,,,{ε})

  5. 5.

    Extended naturals (+,+,,0,1)

  6. 6.

    Viterbi ([0,1],max,,0,1)

  7. 7.

    Boolean ({0,1},,,0,1)

  8. 8.

    Extended non-negative rationals (0+,+,,0,1)

4 Axioms

In this section, we present an axiomatization of bisimulation equivalence for wGKAT expressions (Figure 2). We also derive some facts from the axioms which will be useful for both the examples and the proof of completeness (Section 4.1).

To explain the axioms in Figure 2, we first need to define a property similar to Salomaa’s empty word property [22], which will be a familiar side condition for a fixpoint axiom.

Definition 4.1.

We define E:ExpAt𝕊 inductively as follows

E(p)α =E(v)α=0
E(b)α ={1αBAb0αBAb¯
E(ersf)α =rE(e)α+sE(f)α
E(e+bf)α ={E(e)ααBAbE(f)ααBAb¯
E(e;f)α =E(e)αE(f)α
E(e(b))α =E(b¯)α
Lemma 4.1.

Let eExp,αAt. It holds that E(e)α=(e)α().

Guarded Choice Axiomsq(𝖦𝟣)e+bee(𝖦𝟤)e+bfb;e+bf(𝖦𝟥)e+bff+b¯e(𝖦𝟦)(e+bf)+cge+bc(f+cg)Distributivity Axioms(𝖣𝟣)ers(f+bg)(ersf)+b(ersg)(𝖣𝟤)ers(ftug)er1(fstsug)(𝖣𝟥)b;(ersf)b;(b;ersb;f)Sequencing Axioms(𝖲𝟣)1;eee;1(𝖲𝟤)(e;f);ge;(f;g)(𝖲𝟥)0;e0(𝖲𝟦)(ersf);ge;grsf;g(𝖲𝟧)(e+bf);ge;g+bf;g(𝖲𝟨)v;ev(𝖲𝟩)b;cbcLoop Axioms(𝖫𝟣)e(b)e;e(b)+b1(𝖫𝟤)e(frs 1)+cgc;e(b)c;((sr;f;(e)(b))+b1)Scaling Axioms(𝖢𝟣)11(𝖢𝟤)0;e0Weighted Choice Axioms(𝖶𝟣)erse(r+s);e(𝖶𝟤)ersffsre(𝖶𝟥)ers(ftug)(erstf)1sug(𝖶𝟦)erusf(u;e)rsfFixpoint Rule (𝖥𝟣)ge;g+bfαAtE(e)α=0ge(b);f
Figure 2: The axiomatization of wGKAT bisimulation equivalence. In these statements we let e,f,gExp,b,cBExp,vOut,αAt,pAct,r,s,t,uS. 1 and 0 weights refer to the multiplicative and additive identity in the chosen semiring.

Axiom Summary.

We define Exp×Exp as the smallest congruence satisfying the axioms in Figure 2. Axioms 𝖦𝟣-𝖦𝟦 are inherited from GKAT [25] and describe guarded choice. Axioms 𝖣𝟣 and 𝖣𝟤 state that weighted choice distributes over guarded choice and another weighted choice, respectively. 𝖣𝟥 describes the interaction of tests and weighted choice.

Axioms 𝖲𝟣-𝖲𝟩 characterize sequential composition. 𝖲𝟦 is perhaps the most interesting; it states that composition right distributes over weighted choice just like guarded choice (𝖲𝟧). Since we equate the programs with respect to bisimilarity, which is a branching-time notion of equivalence, the symmetric rules of left distributivity are not sound. 𝖲𝟣 and 𝖲𝟤 state that wGKAT expressions have the structure of a monoid with identity 1, and with vOut and 0 being absorbent elements when composed on the left (𝖲𝟨, 𝖲𝟥).

𝖢𝟣-𝖢𝟤 are about scaling. Scaling by the multiplicative identity does nothing, it is the same as skip. Scaling by 0 annihilates any following expressions as it multiplies the weights by the multiplicative annihilator of the semiring. Though note that it is not the same as abort (0), since scaling by 0 assigns weight 0 to , while 0 assigns weight 1 to . In this way both expressions annihilate any following expressions, but are not the same.

𝖶𝟣-𝖶𝟦 describe weighted branching. Identical branches can be combined, 𝖶𝟣. The order of branches doesn’t matter, 𝖶𝟤. A repeated branching can be re-nested by re-weighting, 𝖶𝟥. Finally, weights can be pushed through the branching into the following expression, 𝖶𝟦.

Remark 4.1.

We have made a choice to present some of our axioms using the syntactic sugar . The axiomatization could be equivalently expressed without it. For example, if we were to express 𝖢𝟣 without the syntactic sugar it would state (110 0);11. Stated explicitly, this axiom offers a way to remove weighted choices from expressions. Note that it is not derivable from other axioms of weighted choice as it is the only axiom with a weighted choice on the left-hand side but not on the right. The use of improves the readability and usability of the axioms. This is because it provides a compact representation of weighted choices with branches scaled by 0 (which are irrelevant for the behavior).

Finally we discuss the loop axioms. 𝖥𝟣 is the fixpoint rule. It states that fixpoints for productive loops are unique. We capture the notion of productivity of expressions, using an auxiliary operator E. 𝖫𝟣 is standard loop unrolling. A loop body is executed no times or one or more depending on the test, so it is the same as making a guarded choice between skipping or executing the loop body one or more times. 𝖫𝟤 allows unrolling and flattening the first set of iterations of a weighted loop if one of the branches is non-productive. The idea is that the loop can execute the nonproductive branch any number of times, but eventually must take the productive branch, after which it reenters the loop. Since a program action has now been taken, the boolean test c could now fail. Hence when the loop body is re-entered it is of the original form. Intuitively the loop has been unrolled up to the first time it executes the productive branch and this nonproductive unrolled portion has been flattened into one scaling followed by the productive program action and then the original loop.

Corollary 4.1 (Soundness).

For all e,fExpefef

4.1 Derivable facts

Some other useful identities are derivable from the axioms.

Lemma 4.2.

For all b,cBExp,e,f,g,hExp,r,s,t,u𝕊
𝖣𝖥𝟣 t;(ersf)etrtsf 𝖣𝖥𝟪 b;(e+cf)b;e+cb;f 𝖣𝖥𝟤 e+b(f+cg)(e+bf)+b+cg 𝖣𝖥𝟫 b;(e+cf)b;(b;e+cf) 𝖣𝖥𝟥 e+b0b;e 𝖣𝖥𝟣𝟢 r;s(rs) 𝖣𝖥𝟦 b;(e+bf)b;e 𝖣𝖥𝟣𝟣 r;(e+bf)r;e+br;f 𝖣𝖥𝟧 (e+bf)rsg(ersg)+b(frsg) 𝖣𝖥𝟣𝟤 grs0r;g 𝖣𝖥𝟨 (e+bf)rs(g+bh)(ersg)+b(frsh) 𝖣𝖥𝟣𝟥 b;(ersf)b;(b;ersf) 𝖣𝖥𝟩 e+1fe 𝖣𝖥𝟣𝟦 gst(eru0)gstre

With the axioms and derived facts in hand, we now revisit our original examples. In the ski rental problem the relevant property is the minimum total cost that could be paid over these sequential days. An appropriate choice of semiring to weight over is the tropical semiring, as it allows us to reason about the cheapest branch of computation using sum to produce branches and minimum to compare branches.

Example 4.1 (Ski Rental).

We now prove that the optimal cost is buying skis if the trip is longer than n days and renting skis otherwise. Recall the encoding was (11yv)n;v where n is the number days of the trip, y the cost of skis, and v terminates the process.

We first prove by induction on n the lemma (11yv)n(1nyv). The base case where n=1 is trivial. Suppose it is true for n=k.

(11yv)k+1 (11yv)k;(11yv) (Definition of en)
(1kyv);(11yv) (Induction hypothesis)
(1;(11yv)kyv;(11yv)) (S4)
((11yv)kyv) (S1, S6)
(vyk(vy1 1)) (W2)
((vykyv)0k1 1) (W3)
(((y+ky);v)0k1 1) (W1)
((y;v)0k1 1) (y+ky=y)
(vyk1 1) (W4)
(1k1yv) (W2)

We now use this fact to simplify the expression of the ski rental problem:

(11yv)n;v (1nyv);v
(1;vnyv;v) (S4)
(vnyv) (S1, S6)
(n+y);v (W1)

This is termination with weight equal to the minimum of n and y.

Example 4.2 (Coin Game).

Recall the encoding is ((111(1;$⃝)).5.5(0;$⃝))(1), where $⃝ is the outcome of winning a dollar. We are interested in expected value, so we choose the extended non-negative rational semiring because this can capture both the probabilities and the values of outcomes. We choose rationals rather than the reals to avoid having to compare infinite precision numbers. We now simplify the encoding:

((111(1;$⃝)).5.5(0;$⃝))(1)
((111(1;$⃝)).5.5(0;0))(1) (C2)
((111(1;$⃝)).50 0)(1) (W4)
(.5(111(1;$⃝)))(1) (2.1)
(.5(111$⃝))(1) (C1, S1)
(1.5.5$⃝)(1) (DF1)
($⃝.5.5 1)(1) (W2)
($⃝.5.5 1+10)(1) (DF7)
1;(((.5.5);$⃝;(($⃝.5.5 1)+10)(1))+11) (L2)
(.5.5);$⃝;($⃝.5.5 1+10)(1) (S1, DF7)
(.5.5);$⃝ (S6)
(2.5);$⃝
1;$⃝

Hence, the player expects to win one dollar in this game.

5 Completeness

It is natural to ask if the set of axioms presented in Section 4 is complete, i.e., whether bisimilarity of any pair of wGKAT expressions can be established solely through the means of axiomatic manipulation. As we will see later on, the problem of completeness essentially relies on representing wGKAT automata syntactically as certain systems of equations and uniquely solving them. This is similar to proofs of completeness one might encounter in the literature concerning process algebra and Kleene Algebra.

Unfortunately, similarly to GKAT [25] and its probabilistic exension [21], this poses a few technical challenges. Firstly, unlike Kleene Algebra, we do not have a perfect correspondence between the operational model (wGKAT automata) and the expressivity of the syntax. Namely, there exist wGKAT automata that cannot be described by a wGKAT expression. This simply stems from the fact that our syntax is able to only describe programs with well-structured control flow using while loops and if-then-else statements, which is strictly less expressive than using arbitrary non-local flow involving constructs like goto expressions in an uninterpreted setting. Secondly, classic proofs of completeness of Kleene Algebra strictly rely on the left distributivity of sequential composition over branching, which is unsound under bisimulation semantics. This is crucial, as it allows for reduction of the problem of solving an arbitrary system of equations to the unary case that can be handled through the inference rule similar to F1 of our system.

In the presence of these problems, we circumvent those issues by extending our inference system with a powerful axiom schema generalizing F1 to arbitrary systems of equations (hence avoiding the issue of left distributivity) that states that each such system has at most one solution (thus solving the problem of insufficient expressivity of our syntax). We will follow the GKAT terminology and refer to this axiom schema as the Uniqueness axiom (UA) [25], but the general idea is standard in process algebra and was explored by Bergstra under the name Recursive Specification Principle (RSP)  [2].

To obtain the completeness result, we will rely on the following roadmap:

  1. 1.

    First, we show that every wGKAT expression possesses a certain normal form that ties it to its operational semantics.

  2. 2.

    Then, we define systems of equations akin to the normal form the step above and define what it means to solve them.

  3. 3.

    Relying on the above two steps, we prove the correspondence between solutions to systems of equations and wGKAT automata homomorphisms.

  4. 4.

    We establish the soundness of the Uniqueness Axiom. As a consequence of the correspondence from the step above, we show that two expressions being related by some bisimulation can be seen as them being solutions to the same system of equations. This combined with the use of UA guarantees completeness.

5.1 Fundamental Theorem

In order to prove completeness we will use an intermediate result which states that each expression can be simplified to a normal form, obtained from the operational semantics of the expression. Following the terminology from the Kleene Algebra community we call this the fundamental theorem [20].

Definition 5.1 ([21]).

Given ΦAt and an indexed collection {eα}αΦ where αΦ,eαExp we define a generalized guarded sum inductively as

Definition 5.2.

Given a non-empty finite index set I and indexed collections {ri}iI and {ei}iI such that eiExp and ri𝕊 for all iI we define a sum expression inductively:

iIriei=ejrj1(iI{j}riei)

Both ˜5.1 and ˜5.2 are well defined up to the order they are unrolled. See the full version of the paper [13, Appendix D] for details.

Theorem 5.1 (Fundamental Theorem).

For every eExp it holds that

where exp defines a function 2+Out+Act×ExpExp given by

exp()=0exp()=1exp(v)=vexp((p,f))=p;f(vOut,pAct,fExp)

5.2 Solutions to Systems of Equations

System of equations.

We are now ready to characterize systems of equations and their solutions. We first introduce a three-sorted grammar to mimic the way that atoms index weighted choices in the fundamental theorem.

Note that the above is well defined only if we take a congruence containing our axioms of both guarded and weighted choice, as the generalized version of guarded choice is defined up to skew-associativity and skew-commutativity. That is, an arbitrary order may be picked when selecting an element of Exp(X), but after substituting wGKAT expressions for indeterminates xX it won’t matter which order was selected. See Appendix D in the full version of the paper [13] for details.

Definition 5.3 ([21]).

A system of equations is a pair (X,τ:XExp(X)) consisting of a finite set X of indeterminates and a function τ. If for all xX,αAt in each τ(x) the gx subterms satisfy E(g)α=0, the system of equations is called Salomaa.

We now define the system of equations associated with a given wGKAT automaton.

Definition 5.4.

Let (X,β) be a wGKAT automaton. A system of equations associated with (X,β) is a Salomaa system (X,τ), with τ:XExp(X) defined by

where sys:2+Out+Act×ExpWExp(X) is given by

sys()=0sys()=1sys(v)=vsys(p,x)=px
Example 5.1.

The τ (up to ) associated with the automaton from ˜3.1 is

x1 (043(p1x2))+α(v11((p2x2)52(p3x3))+β0)
x2 1150 0+α(1150 0+β0)
x3 1150 0+α(1150 0+β0)
Definition 5.5 ([21]).

Given a function h:XExp that assigns a value to each indeterminate in X we derive a wGKAT expression h#(e) for each eExp(X) inductively:

h#(f) =f (3)
h#(e+bf) =h#(e)+bh#(f) (4)
h#(w1rsw2) =h#(w1)rsh#(w2) (5)
h#(gx) =g;h(x) (6)

We now characterize a solution to the Salomaa system of equations.

Definition 5.6 ([21]).

Let RExp×Exp be a congruence. A solution up to R of a system (X,τ) is a map h:XExp such that for all xX that (h(x),h#(τ(x)))R

Example 5.2.

A solution up to of ˜5.1 would satisfy

h(x1) (043p1;h(x2))+α(v11(p2;h(x2)52p3;h(x3))+β0)
h(x2) 1150 0+α(1150 0+β0)
h(x3) 1150 0+α(1150 0+β0)

So in this case we can select

h(x2)=h(x3) =15
h(x1) =(043(p1;15))+α(v11((p2;15)52(p3;15))+β0)

We now can show the connection between solutions to the Salomaa system of equations and automaton homomorphisms using the equivalence classes of states.

Theorem 5.2.

Let (X,β) be a finite wGKAT automaton. The map h:XExp is a solution up to of the system associated with (X,β) if and only if []h is a wGKAT automaton homomorphism from (X,β) to (Exp/,¯). Where ¯ is the unique transition function on Exp/ which makes the quotient map []:ExpExp/ a wGKAT automaton homomorphism from (Exp,) to (Exp/,¯).

5.3 Bisimilarity implies Provable Equivalence

Having characterized systems of equations and their solutions we now present the uniqueness axiom and establish completeness. Let ˙Exp×Exp be the least congruence that contains , and satisfies the following axiom:

(X,τ) is a Salomaa systemf,g:XExp are solutions of (X,τ) up to ˙f(x)˙g(x)for all xX (UA)

We establish the soundness of the axiom in the same way as before.

Theorem 5.3 (Soundess of ˙).

For all e,fExp,e˙fef

Finally, we can prove completeness using the uniqueness axiom.

Theorem 5.4 (Completeness).

For all e,fExp,efe˙f

6 Decidability and Complexity

In practice, one often cares about a mechanistic way to check program equivalence. We show that bisimulation equivalence for wGKAT expressions is indeed decidable, and we offer an efficient procedure to decide it. This sets our language apart from other weighted KAT variants, in particular KAWT, which does not offer a decision procedure for equivalence and is likely not decidable due to using trace equivalence. The key insight is that bisimulation equivalence lets us appeal to known theory of monoid-weighted transition systems and achieve a decision procedure which, remarkably, is polynomial time.

Similar to ProbGKAT [21], we rely on a coalgebraic generalization [3] of classic partition refinement [12, 17] to minimize the automaton under bisimilarity which essentially computes the largest bisimulation. Coalgebraic partition refinement offers a procedure to minimize any coalgebra that fits a grammar of supported functors and polynomial constructors [3]. As mentioned before, wGKAT automata can be viewed as coalgebras. So in order to establish the decidability of bisimulation equivalence for wGKAT automata we show how to express the equivalent coalgebra in the grammar which can be decided by coalgebraic partition refinement. However, in order to determine a bound on the runtime of this procedure we must bound some of the internal operations of the coalgebraic partition refinement algorithm.

To bound the runtime of the coalgebraic partition refinement algorithm we encode our coalgebra in a format with a uniform label set, and then bound the comparison of labels, the init step, and the update step [3]. The init step essentially takes the set of labels on edges from a state and computes the total weight of those edges. The update step basically uses a state’s labels into a set of states S, and the weight of the same state’s edges into another set of states B and computes the weight of edges into S and C/S, as well as computing transitions into blocks of related states [3, 4]. Once we bound these operations we can leverage a complexity result [3, Theorem 3.4] of coalgebraic partition refinement to achieve the desired runtime bound. The details of both of these arguments can be found in the full version of the paper [13, Appendix E].

Corollary 6.1 (Decidability).

If e,fExp, n=#e+#f, and At is fixed, then wGKAT equivalence of e and f is decidable in time O(n3log2(n))

Remark 6.1.

The astute reader will know that the equivalence of rational power series in the tropical semiring is undecidable [16] and might reasonably doubt the decidability of equivalence of wGKAT expressions. This does not pose an issue for wGKAT. Our notion of equivalence is one of bisimilarity, and hence single step equivalence, not trace equivalence. Due to this, deciding equivalence of wGKAT terms over the tropical semiring reduces to deciding equivalence of terms over the additive monoid of the tropical semiring, not the tropical semiring itself. For this reason equivalence of wGKAT automata can be decided without deciding equivalence of rational power series. For this reason equivalence with respect to bisimilarity of wGKAT expressions is decidable even over the tropical semiring.

7 Related Work

Our work comes in a long line of work on Kleene Algebra with Tests (KAT) [15]. This is an algebraic framework for reasoning about programs based on Kleene Algebra, the algebra of regular expressions. The original model was one with the axioms of Kleene Algebra combined with a boolean algebra of tests, giving control flow to a algebraic model. A restriction of this language to the deterministic fragment led to GKAT which allows for decision of equivalence in near linear time [25]. Following this, a deterministic probabilistic language, ProbGKAT, was developed which was also efficiently decidable [21]. Our work is directly inspired by ProbGKAT, although it is orthogonal as an extension of GKAT with semiring weightings. ProbGKAT extended GKAT with convex sums in order to capture probability, in contrast to the general weighted sums we introduce in this paper which do not enforce convexity [21]. As a result the semantics and axiomatizations differ considerably in form but also in terms of the techniques needed to prove results. We took inspiration for our arguments from the general theory of effectful process algebras [23].

Both idempotent and non-idempotent semirings have been examined and used as models for computation [14, 5]. While our work is directly inspired by [15], the work on various non-idempotent -semirings was invaluable to our characterization of semirings appropriate for weighting over. In particular we considered both iteration semirings [6] and inductive -semirings [7]. The work on classifying -semirings is quite thorough and may offer useful classes for researchers working on weighted computation. Semirings in general are well studied and we refer to this theory at various points for our arguments [8].

We would be remiss to not mention the work on Kleene Algebra with Weights and Tests (KAWT) [24]. This is an extension of KAT with weights. It works by weighting the nondeterministic branches of computation in KAT and summing weights. The syntax is quite similar to our own. KAWT is based on a relational semantics which assigns weights to guarded strings in contrast to our coalgebra-based semantics. The syntax of KAWT introduces another class of expression to KAT, the weightings. This class behaves like the Boolean tests in KAT, allowing for both identities, addition and multiplication. These terms are then subterms of programs. For a semiring to be used as the weights in a KAWT it must be idempotent and complete. This allows for a definition of iteration, while keeping each KAT a KAWT. An idempotent semiring is one in which s𝕊,s+s=s and a complete semiring is one in which there is an infinitary sum operator I for any index set I, and the sum obeys some natural notions of sums and multiplication.

Two key differences between wGKAT and KAWT languages are decidability and the admissible class of semirings. In particular no decidability results exist for KAWT [24] and idempotent and complete semirings are considered. We require the semiring be positive, Conway and refinement. All complete semirings are positive [8, 22.28], and all complete -semirings are Conway semirings [5, Theorem 3.4]. So roughly speaking, we impose the new restriction of being a refinement monoid, but in exchange we drop the requirement of idempotence and loosen the requirement of completeness. We find that this trade includes several new useful semirings, like the natural numbers with infinity under addition and multiplication, or even the non-negative extended reals under addition and multiplication, while ruling out only pathological examples.

Finally our work on the wGKAT automaton leverages the existing work on the general theory of coalgebra [19, 11, 18, 9] and in particular monoid-weighted transition systems [10]. We found the property of refinement in monoids to particularly useful and the existing literature to be quite thorough [26, 10]. These ideas of mutual refinements are relevant to the semantics of weighted programming. Of course we leverage an existing algorithm for our decision procedure for bisimulation equivalence [3, 27, 4].

8 Conclusion

We presented wGKAT, a weighted language inspired by Kleene Algebra with Tests, equipped with sequential composition, weighted branching over a large class of semirings, conditionals, Boolean tests, primitive actions, and guarded loops. We proposed an operational semantics and gave a sound and complete axiomatization of bisimilarity. Finally, we showed that bisimulation equivalence of wGKAT is efficiently decidable in O(n3log2(n)) time.

One extension of this work would be to axiomatize the coarser notion of trace equivalence, which brings in new axioms. For example, left distributivity over guarded and weighted choice would seem to be sound under trace equivalence, given some conditions on the weights involved. The undecidability of equivalence of power series in the tropical semiring poses issues for a decision procedure for trace equivalence. However characterizing a decision procedure based on properties of the semiring would be an interesting result.

A practical direction for research would be to take these ideas of weightings and apply them to NetKAT, a variant of KAT for verifying network properties. This would allow for examination of quantitative properties which may be of interest to network operators.

Another direction for future research is to prove completeness without the semiring being refinement and positive. These conditions were needed for a bisimulation to exist, which is what made the completeness theorem possible. If it were possible to prove completeness without laying hands on a bisimulation, then behavioral equivalence could still be established without these properties. While we are only aware of pathological examples of semirings which fail to be refinement, allowing for non-positive semirings would include many familiar semirings. Finally, tackling the question of completeness without the uniqueness axiom which remains open for GKAT, ProbGKAT, and now wGKAT.

References

  • [1] Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. Weighted Programming, 2022. doi:10.48550/arXiv.2202.07577.
  • [2] Jan A. Bergstra and Jan Willem Klop. Verification of an alternating bit protocol by means of process algebra. In Wolfgang Bibel and Klaus P. Jantke, editors, Mathematical Methods of Specification and Synthesis of Software Systems ’85, Proceedings of the International Spring School, Wendisch-Rietz, GDR, April 22-26, 1985, volume 215 of Lecture Notes in Computer Science, pages 9–23, Berlin, Heidelberg, 1985. Springer. doi:10.1007/3-540-16444-8_1.
  • [3] Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic Partition Refinement and Weighted Tree Automata. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods – The Next 30 Years, pages 280–297, Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-30942-8_18.
  • [4] Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement, 2017. doi:10.48550/arXiv.1705.08362.
  • [5] M Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer-Verlag, 2009. doi:10.1007/978-3-642-01492-5.
  • [6] Zoltán Ésik. Iteration Semirings. In Masami Ito and Masafumi Toyama, editors, Developments in Language Theory, pages 1–20, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. doi:10.1007/978-3-540-85780-8_1.
  • [7] Zoltán Ésik and Werner Kuich. Inductive star-semirings. Theor. Comput. Sci., 324(1):3–33, 2004. Words, Languages and Combinatorics. doi:10.1016/j.tcs.2004.03.050.
  • [8] Jonathan S Golan. Semirings and their Applications. Springer Science & Business Media, 2013. doi:10.1007/978-94-015-9333-5.
  • [9] H Peter Gumm. Copower functors. Theoretical Computer Science, 410(12-13):1129–1142, 2009. doi:10.1016/j.tcs.2008.09.057.
  • [10] H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science, 44(1):185–204, 2001. CMCS 2001, Coalgebraic Methods in Computer Science (a Satellite Event of ETAPS 2001). doi:10.1016/S1571-0661(04)80908-3.
  • [11] H. Peter Gumm and Tobias Schröder. Coalgebras Of Bounded Type. Math. Struct. Comput. Sci., 12(5):565–578, 2002. doi:10.1017/S0960129501003590.
  • [12] Paris C. Kanellakis and Scott A. Smolka. CCS Expressions, Finite State Processes, and THree Problems of Equivalence. In Robert L. Probert, Nancy A. Lynch, and Nicola Santoro, editors, Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 17-19, 1983, PODC ’83, pages 228–240, New York, NY, USA, 1983. ACM. doi:10.1145/800221.806724.
  • [13] Spencer Van Koevering, Wojciech Różowski, and Alexandra Silva. Weighted GKAT: Completeness and Complexity, 2025. arXiv:2504.20385.
  • [14] Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 110(2):366–390, 1994. doi:10.1006/inco.1994.1037.
  • [15] Dexter Kozen. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19(3):427–443, May 1997. doi:10.1145/256167.256195.
  • [16] Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In W. Kuich, editor, Automata, Languages and Programming, pages 101–112, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. doi:10.1007/3-540-55719-9_67.
  • [17] Robert Paige and Robert E. Tarjan. Three Partition Refinement Algorithms. SIAM Journal on Computing, 16(6):973–989, 1987. doi:10.1137/0216062.
  • [18] H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. Electronic Notes in Theoretical Computer Science, 33:111–131, 2000. CMCS’2000, Coalgebraic Methods in Computer Science. doi:10.1016/S1571-0661(05)80346-9.
  • [19] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
  • [20] Jan J. M. M. Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theor. Comput. Sci., 308(1-3):1–53, 2003. doi:10.1016/S0304-3975(02)00895-2.
  • [21] Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity, 2023. doi:10.48550/arXiv.2305.01755.
  • [22] Arto Salomaa. Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM, 13(1):158–169, January 1966. doi:10.1145/321312.321326.
  • [23] Todd Junior Wayne Schmid. Coalgebraic Completeness Theorems for Effectful Process Algebras. PhD thesis, UCL (University College London), 2024.
  • [24] Igor Sedlár. Kleene Algebra With Tests for Weighted Programs. 2023 IEEE 53rd International Symposium on Multiple-Valued Logic (ISMVL), pages 111–116, 2023. doi:10.48550/arXiv.2303.00322.
  • [25] Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proceedings of the ACM on Programming Languages, 4(POPL):1–28, December 2019. doi:10.1145/3371129.
  • [26] Friedrich Wehrung. Refinement Monoids, Equidecomposability Types, and Boolean Inverse Semigroups, volume 2188 of Lecture Notes in Mathematics. Springer International Publishing, Cham, 1st edition 2017 edition, 2017. doi:10.1007/978-3-319-61599-8.
  • [27] Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science, 16, 2020. doi:10.23638/LMCS-16(1:8)2020.