Weighted GKAT: Completeness and Complexity
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 ProcedureCategory:
Track B: Automata, Logic, Semantics, and Theory of ProgrammingFunding:
Spencer Van Koevering: Partially supported by a Cornell Bowers CIS Deans Excellence Fellowship.Copyright and License:
![[Uncaptioned image]](x1.png)
2012 ACM Subject Classification:
Theory of computation Models of computationEditors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele PuppisSeries and Publisher:

1 Introduction
Weighted programming is a recently introduced paradigm [1] in which computational branches of programs are associated with quantities. For example, the program does with weight and with weight . 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 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.
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.
We identify a class of semirings for which the semantics of weighted loops can be computed when considering bisimulation equivalence (Section 3.2).
- 3.
-
4.
We design a decision procedure for bisimilarity which runs in time if the number of tests is fixed, where 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
do p | ||||||
assert b | ||||||
return v | ||||||
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 of primitive tests, we define BExp, the grammar of tests, to be given by the following:
In the above, and respectively represent false and true, denotes negation, represents disjunction and juxtaposition is conjunction. We will write to denote Boolean equivalence in BExp. Logical entailment defines a preorder given by . The quotient of BExp by the relation , denoted by is in one-to-one correspondence with the Boolean Algebra freely generated by the set . The entailment defines a partial order on . 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 . Intuitively, given two programs and , represents a program that runs with the weight of and with the weight of . 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).
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 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 is a nonempty carrier set equipped with two monoid structures interacting in the suitable way.
-
1.
is a commutative monoid with identity
-
2.
is a monoid with identity element
-
3.
and for all
-
4.
for all in
We will abuse the notation and write multiplication in as juxtaposition; additionally we will write 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 and ) are distinct from false and true tests (respectively denoted by and ).
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 days. Each day they either rent skis for a cost of , or they buy them for a cost of and no longer have the need to rent. We can encode the situation of making this choice on the trip lasting days, via the following wGKAT expression over the tropical semiring:
Here, for positive , we write the -fold sequential composition of the expression .
Essentially, we perform at most choices between paying and immediately terminating upon paying . The immediate termination is represented using a return value .
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:
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 . The inner weighted choice is slightly different, it represents an “and”. Each branch executes with probability . 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 and a fixed semiring , define . Here, refers to the support of a function given by . Elements of the set are functions which we will refer to as weightings on over . We can view these as formal sums over 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 , we can define an analog of Dirac delta specialized to weightings, namely , which maps its argument to the semiring multiplicative identity if it is equal to , and the semiring additive identity otherwise. Given a set , we will write for the total weight of the set under the weighting . Moreover, any function can be uniquely extended to a function , called the linearization of , given by
Crucially, the above satisfies the property that , where is defined by . 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 is the unique -semimodule homomorphism of the type , that allows to factor 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 consisting of a set of states and a transition function 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 , 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 , representing performing a labelled transition to a next state.
To lighten up notation, we will write instead of .
Example 3.1.
Let . We consider a wGKAT automaton , whose pictorial representation is below on the left, while the definition of is below to the right.
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 , whose states are wGKAT expressions. The semantics of an expression , 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 , we define by structural induction on .
Tests, actions, output variables.
Suppose , we let
A test either accepts or aborts with weight depending on whether the given atom entails the truth of the test. An output variable outputs itself with weight and then terminates. An action outputs the atomic program action and then accepts with weight , 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 .
Guarded Choice.
A guarded choice is an if-then-else statement conditioned on . To capture this, we let have the outgoing edges of if and otherwise.
Weighted Choice.
The intuition here is that the automaton executes both arguments and scales their output by the given quantity. We define as the automaton with all outgoing edges of , scaled by , and all outgoing edges of , scaled by . The derivative is:
where these operations are the addition and scalar multiplication of the weightings.
Sequential Composition.
We define the derivative of sequential composition as:
where given and we let be the linearization of , given by:
The intuition here is that if skips, then the behavior of the composition is the behavior of . If aborts or returns a value then the derivative is the behavior of . Finally, if executes an action and transitions to another state, then the behavior is the next step of composed with 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 such that
(1) | ||||
(2) |
We note that the fixpoint rule 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:
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 to re-enter the loop once computation of 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 as .
Lemma 3.1.
For all , is finite. We bound it by where
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 a function is a wGKAT homomorphism if for all and
-
1.
For any
-
2.
For any
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 and be wGKAT automata. A relation is a bisimulation if there exists a transition function such that the projections are wGKAT homomorphisms from to and respectively. We say the elements are bisimilar if there exists a bisimulation R such that .
To be able to build the combined transition structure over 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 is a refinement monoid if implies that there exist such that . A monoid with identity is positive (conical) if for all , .
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.
Tropical
-
2.
Arctic
-
3.
Bottleneck
-
4.
Formal languages
-
5.
Extended naturals
-
6.
Viterbi
-
7.
Boolean
-
8.
Extended non-negative rationals
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 inductively as follows
Lemma 4.1.
Let . It holds that .
Axiom Summary.
We define 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 , and with and 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 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 (), since scaling by assigns weight to ✗, while assigns weight 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 . 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 (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 . 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 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
4.1 Derivable facts
Some other useful identities are derivable from the axioms.
Lemma 4.2.
For all
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 days and renting skis otherwise. Recall the encoding was where is the number days of the trip, the cost of skis, and terminates the process.
We first prove by induction on the lemma . The base case where is trivial. Suppose it is true for .
(Definition of ) | ||||
(Induction hypothesis) | ||||
(S4) | ||||
(S1, S6) | ||||
(W2) | ||||
(W3) | ||||
(W1) | ||||
() | ||||
(W4) | ||||
(W2) |
We now use this fact to simplify the expression of the ski rental problem:
(S4) | ||||
(S1, S6) | ||||
(W1) |
This is termination with weight equal to the minimum of and .
Example 4.2 (Coin Game).
Recall the encoding is , 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:
(C2) | |||
(W4) | |||
(2.1) | |||
(C1, S1) | |||
(DF1) | |||
(W2) | |||
(DF7) | |||
(L2) | |||
(S1, DF7) | |||
(S6) | |||
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.
First, we show that every wGKAT expression possesses a certain normal form that ties it to its operational semantics.
-
2.
Then, we define systems of equations akin to the normal form the step above and define what it means to solve them.
-
3.
Relying on the above two steps, we prove the correspondence between solutions to systems of equations and wGKAT automata homomorphisms.
-
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 and an indexed collection where we define a generalized guarded sum inductively as
Definition 5.2.
Given a non-empty finite index set I and indexed collections and such that and for all we define a sum expression inductively:
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 it holds that
where exp defines a function given by
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 , but after substituting wGKAT expressions for indeterminates 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 consisting of a finite set of indeterminates and a function . If for all in each the gx subterms satisfy , the system of equations is called Salomaa.
We now define the system of equations associated with a given wGKAT automaton.
Definition 5.4.
Let be a wGKAT automaton. A system of equations associated with is a Salomaa system , with defined by
where is given by
Example 5.1.
The (up to ) associated with the automaton from ˜3.1 is
Definition 5.5 ([21]).
Given a function that assigns a value to each indeterminate in we derive a wGKAT expression for each inductively:
(3) | ||||
(4) |
(5) | ||||
(6) |
We now characterize a solution to the Salomaa system of equations.
Definition 5.6 ([21]).
Let be a congruence. A solution up to of a system is a map such that for all that
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 be a finite wGKAT automaton. The map is a solution up to of the system associated with if and only if is a wGKAT automaton homomorphism from to . Where is the unique transition function on which makes the quotient map a wGKAT automaton homomorphism from to .
5.3 Bisimilarity implies Provable Equivalence
Having characterized systems of equations and their solutions we now present the uniqueness axiom and establish completeness. Let be the least congruence that contains , and satisfies the following axiom:
(UA) |
We establish the soundness of the axiom in the same way as before.
Theorem 5.3 (Soundess of ).
For all
Finally, we can prove completeness using the uniqueness axiom.
Theorem 5.4 (Completeness).
For all
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 , and the weight of the same state’s edges into another set of states and computes the weight of edges into and , 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 , , and At is fixed, then wGKAT equivalence of and is decidable in time
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 and a complete semiring is one in which there is an infinitary sum operator for any index set , 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 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.