Pith. sign in

REVIEW 5 minor 54 references

On Propositional Program Equivalence (extended abstract)

T0 review · 0 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read GKAT checks uninterpreted program equivalence in nearly linear time

desk verdict A clear, honest survey of GKAT that breaks no new ground but is a solid entry point; worth a referee's time if the venue wants expository work. read the letter →

arxiv 2507.07480 v1 pith:UTNWRSFL submitted 2025-07-10 cs.PL

Tobias Kappé This is my paper · ORCID
classification cs.PL
keywords propositionalequivalenceguardedKleenealgebrawithtestsGKATdeterministicautomataonstringsprogramaxiomatizationbisimilaritycontrol-flowverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

General program equivalence is undecidable, so the paper adopts a weaker but still useful notion: two programs are propositionally equivalent when their executions coincide no matter how primitive statements and tests are interpreted. The paper argues that this notion is not merely decidable but practically feasible, and that Guarded Kleene Algebra with Tests (GKAT) is the right framework to make it so. The central worked example is the equivalence of two in-order binary-tree traversal programs, one with three loops and one with a single loop. The survey then lays out the automata-theoretic, axiomatic, and coalgebraic tools behind GKAT, and identifies open problems about completeness and expressivity.

What carries the argument

The load-bearing objects are deterministic automata on guarded strings, where a guarded string is a word alternating complete truth assignments to primitive tests with primitive actions, and a deterministic automaton has at most one transition per atom and at most one accepted atom per state. GKAT expressions convert to such automata in linear size, since no determinization step is needed, and language equivalence of these automata is checkable in nearly linear time via the Hopcroft-Karp union-find algorithm. The other central device is the unique-fixed-point rule for loops, guarded by a productivity side condition $E(e) \equiv 0$ that forces the loop body to perform an action before it can terminate; adding this rule as an infinitary scheme axiomatizes loop equivalence. For bisimilarity, the corresponding machinery is the transition system of Figure 6 and skip-free GKAT, axiomatized using techniques adapted from 1-free regular expressions.

What would settle it

Exhibit two GKAT expressions that are equivalent according to the guarded-language semantics but cannot be proved equivalent by the finite axioms of Figure 4 together with the generalized unique-fixed-point rule; the paper leaves this completeness question open, so finding such a pair (or proving none exists) would settle the axiomatization's adequacy.

Watch

Extended reading notes

Core claim

The survey's central point is that propositional program equivalence, equality of behavior for all interpretations of the primitive actions and tests, becomes decidable in nearly linear time when restricted to the deterministic fragment of Kleene Algebra with Tests, and that this fragment (GKAT) is expressive enough to encode standard deterministic control flow. Concretely, the two encodings of the in-order tree traversal from Figure 1 are equivalent: $e \cdot (b\cdot f)^* \cdot \bar{b} \cdot (c\cdot g\cdot (b\cdot f)^*\cdot \bar{b})^* \cdot \bar{c}$ equals $e \cdot ((b+c)\cdot (b\cdot f + \bar{b}\cdot g))^* \cdot \overline{b+c}$, regardless of what $e,f,g,b,c$ stand for. The paper explains this by embedding programs into GKAT, converting expressions to deterministic automata on guarded strings without an exponential determinization step, and checking language equivalence with a union-find based algorithm. Alongside the decision procedure, the survey reports an axiomatization that is complete only if an infinitary unique-fixed-point rule is admitted, and summarizes evidence, including an infinite hierarchy of deterministic automata, that a finite extension of GKAT cannot express all deterministic behaviors.

Load-bearing premise

The load-bearing premise is that two programs have the same guarded language exactly when they behave identically under every functional interpretation of the primitive actions, so that checking automata on guarded strings truly decides the intended equivalence.

Editorial extensions

If this is right

  • If the GKAT framework is right, verifying equivalence of uninterpreted control-flow programs, such as loop fusions, condition swaps, and restructuring like the two tree-walk variants, becomes feasible for practical-sized code in nearly linear time, not just theoretically decidable.
  • The encoding of standard if/while programs into GKAT means algebraic laws can certify compiler-style transformations without considering what the primitive operations do, so equivalence checking can be built into compilers as a lightweight pre-verification step.
  • The infinite expressivity hierarchy implies that no finite extension of GKAT with deterministic composition operators captures all deterministic guarded-string behaviors, so faithfully modelling every control-flow restructuring requires either non-local control flow or a richer semantic notion.
  • The bisimilarity axiomatization of skip-free GKAT, proved via bisimulation collapse, suggests that process-algebraic reasoning can support equivalence checking where language equivalence is too coarse, for instance distinguishing immediate failure from an infinite loop.
  • A complete finite axiomatization of GKAT equivalence would follow from a characterization of which deterministic automata on guarded strings are solvable in GKAT; the paper identifies this characterization as the key open step.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The automata-theoretic machinery could be adapted to check equivalences between code fragments in a compiler intermediate representation, treating primitive operations as uninterpreted functions for a fast pre-check before full verification.
  • The expressivity hierarchy generalizes the classic structured-programming debate: a language with only if/while is a genuinely restricted fragment of all deterministic finite-state behaviors, so the paper's results sharpen the sense in which 'goto considered harmful' is a propositional claim.
  • If a complete finite axiomatization for GKAT is found, it could yield a proof-theoretic analogue of the Hopcroft-Karp equivalence check: a rewrite system that decides equivalence quickly without ever building automata.
  • The skip-free bisimilarity results hint that the probabilistic extension of GKAT, mentioned as a further development, may inherit similar completeness theorems, giving compositional reasoning for probabilistic programs under the same guarded-style discipline.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. This extended abstract surveys propositional program equivalence through KAT and GKAT. It motivates the topic with the equivalence of two in-order tree traversal programs and states the algebraic law underlying it. It then reviews KAT syntax, relational and guarded-string semantics, the PSPACE-completeness of KAT equivalence, and KAT's axiomatization; introduces GKAT's deterministic automata and nearly linear equivalence checking; discusses fixed-point axiomatizations, expressivity limitations, bisimilarity, and connections with Milner's conjecture; and closes with open problems. The paper contains no new theorems and instead organizes existing results, with the stated goal of serving as a starting point for further study.

Significance. The motivating equivalence is valid, and the paper gives a compact and generally accurate entry point to an active research area. It is honest about what is known versus open, explicitly flagging, for example, the open completeness problem for the finitary fixed-point rule and the lack of a characterization of solvable automata. The claimed complexity and decidability facts are consistent with the cited literature. Because the paper is expository and relies almost entirely on prior work, its value lies in synthesis and accessibility rather than in new technical results.

minor comments (5)
  1. [Sections 2.1, 2.2, 3.1] Negation bars are missing throughout the rendering. Most importantly, the KAT encodings in Section 2.1 should be b·e + bar(b)·f for conditionals and (b·e)*·bar(b) for while loops, and the encodings of the programs in Figures 1a and 1b need the corresponding overbars. In Section 3.1, the clause for E(e(b)) should be E(e(b)) = bar(b), not b, and E(e +_b f) should be b·E(e) + bar(b)·E(f). As printed, E(e(b)) = b is false and would make the unique-fixed-point rule unsound in some cases. Please ensure all negation overbars are present in the final version.
  2. [Section 2.2] The predicate for a primitive test t is written as tau(t) subseteq T; this should be tau(t) subseteq S, since it describes the set of states where t holds.
  3. [Section 3.3] The displayed definition of bisimulation is one-directional; as written it defines a simulation, not a bisimulation. The statement that determinism makes the back condition unnecessary is not generally true: for example, the relation relating 0 to p satisfies the forward-only condition, yet 0 and p are not bisimilar. If the intended notion is a symmetric bisimulation, please state that explicitly; otherwise add the converse transfer clause.
  4. [Section 3.1] There is a small typo in the prose: 'while b to e' should be 'while b do e'.
  5. [Section 2.2] The sentence 'checking language equivalence in KAT is pspace-complete' is imprecise. PSPACE-completeness is for the equivalence problem of KAT expressions; language equivalence of finite automata on guarded strings is much easier. Please reword to avoid confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the motivating equivalence is a genuine example and the cited results are peer-reviewed external theorems.

full rationale

This paper is a survey/position extended abstract, not a derivation of new results from fitted parameters or normalized data. The central motivating claim is that the two in-order traversal programs in Figure 1 are propositionally equivalent, encoded in Section 2.1 as e·(b·f)*·¬b·(c·g·(b·f)*·¬b)*·¬c versus e·((b+c)·(b·f + ¬b·g))*·¬(b+c). This identity is not used as a fitted input: the encodings are standard KAT encodings of control flow, and the claimed equivalence is a genuine guarded-language identity that can be verified directly from the fusion semantics. No parameter is estimated, no quantity is predicted from a subset of data, and no result is defined in terms of its own conclusion. The paper's load-bearing metatheoretic claims—guarded-language semantics coincides with relational semantics for KAT and GKAT, deterministic automata conversion is linear, the decision procedure is nearly linear, and the infinitary axiom scheme is complete—are cited to peer-reviewed prior publications ([34], [4], [49], [46]). Several of these are co-authored by the present author, but self-citation is not circular when the cited works contain independent proofs and are not invoked as unverified premises. The survey also honestly flags open problems, including completeness of the finite axiomatization and the characterization of solvable automata, which further indicates that no closed self-supporting chain is being used to force conclusions. There is no ansatz smuggled in via citation and no known result renamed as organization. The only deficiencies are presentation-level typos and the absence of new technical content, neither of which constitutes circularity.

Assumptions & free parameters 0 free parameters · 8 assumptions · 0 invented entities

The paper introduces no free parameters or invented entities. It relies on standard mathematical background (Boolean algebra, Kleene algebra) and on the axioms and semantics of KAT and GKAT as established in the cited literature. The key domain assumptions are the completeness of guarded-language semantics and the functional interpretation of primitive actions, both taken from prior published work.

assumptions (8)
  • standard math Classical Boolean algebra laws for tests, including idempotence, commutativity, distributivity, and complement.
    Used throughout Section 2 to reason about tests; standard background cited from [3].
  • standard math Kleene algebra axioms for regular expressions, including monoid laws, distributivity, star unfolding, and fixed-point induction.
    Defines the equational theory of regular expressions, used in Section 2.3; standard from [9, 27].
  • domain assumption KAT axioms (Figure 3), combining Boolean algebra and Kleene algebra with tests.
    The main object of study in Section 2; soundness and completeness are cited from [34].
  • domain assumption GKAT syntax and axioms (Figure 4), including the encodings of if-then-else and while loops as first-class constructs.
    GKAT is the focus of Section 3; axioms from [49].
  • domain assumption Unique fixed-point rule for loops with productivity side condition E(e) ≡ 0.
    Used in Section 3.1 to reason about loops; from [49].
  • domain assumption Least fixed-point rule for program inclusion, e.g., if e · g +b f ≦ g then e(b) · f ≦ g.
    Alternative axiomatization of inclusion in Section 3.1; from [49].
  • domain assumption Functional interpretation of primitive actions for GKAT, so that each expression denotes a partial function.
    Assumed in Section 3 to specialize KAT semantics to deterministic programs; from [4].
  • domain assumption Completeness of guarded-language semantics for relational semantics over all interpretations: JeK = Jf K iff JeKI = Jf KI for all I.
    Taken as a background theorem from [34]; underpins the automata-based decision procedure described in Section 2.2.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On Propositional Program Equivalence (extended abstract)." pith.science (2026). https://pith.science/paper/UTNWRSFL

@misc{pith2026250707480,
  author       = {Pith},
  title        = {Pith review of: On Propositional Program Equivalence (extended abstract)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UTNWRSFL}},
  note         = {Machine review of arXiv:2507.07480}
}
abstract

General program equivalence is undecidable. However, if we abstract away the semantics of statements, then this problem becomes not just decidable, but practically feasible. For instance, a program of the form "if $b$ then $e$ else $f$" should be equivalent to "if not $b$ then $f$ else $e$" - no matter what $b$, $e$ and $f$ are. This kind of equivalence is known as propositional equivalence. In this extended abstract, we discuss recent developments in propositional program equivalence from the perspective of (Guarded) Kleene Algebra with Tests, or (G)KAT.

Figures

Figures reproduced from arXiv: 2507.07480 by the authors.

Figure 1
Figure 1. Two algorithms for an in-order walk of a binary tree. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. An example automaton on guarded strings Executions of a program are recorded in so-called guarded strings [34], which are plain words that alternate between actions and atoms. The latter record the truth value of each test at that point in the program. More formally, the set of atoms At is 2 T , and α ∈ At is the atom signifying that all tests in α are true, whereas the primitive tests outside α are false. A guarded… view at source ↗
Figure 3
Figure 3. The axioms of KAT. Here, ≡ is the smallest congruence on KAT that satisfies the laws above for all e, f, g ∈ Exp and b, c, d ∈ BExp. We also write e ≦ f as a shorthand for e + f ≡ f; this makes ≦ a partial order (up to ≡). 2.3 Axiomatization Besides using the decision procedure sketched above to find out whether two KAT terms are equivalent, we can also reason about them equationally. The rel￾evant axioms (in [PITH… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Some axioms of GKAT [49]. Here, ≡ is the smallest congruence on GExp generated by the laws above, for all e, f, g ∈ GExp and b, c ∈ BExp. 3.1 Axiomatization Because GKAT specializes KAT, a natural question is whether the same type of results can be achieved. Previously…
Figure 5
Figure 5. Figure 5: A deterministic automaton on guarded strings without a solution [46]. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: Operational semantics of GKAT terms [46]. Here, [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: Transition rules for regular expressions. All of these are quantified over [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

54 extracted references · 39 canonical work pages

  1. [49]

    In: POPL

    Smolka, S., Foster, N., Hsu, J., Kappé, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In: POPL. pp. 61:1–61:28 (2020).https://doi.org/10.1145/3371129

    doi:10.1145/3371129 2020

  2. [1]

    Azevedo de Amorim, A., Zhang, C., Gaboardi, M.: Kleene algebra with com- mutativity conditions is undecidable. In: CSL. pp. 36:1–36:25 (2025). https: //doi.org/10.4230/LIPICS.CSL.2025.36

    doi:10.4230/lipics.csl.2025.36 2025

  3. [2]

    Journal of Logic and Computation p

    Benevides, M., Gomes, L., Lopes, B.: Towards determinism in PDL: relations and proof theory. Journal of Logic and Computation p. exae022 (2024)

    work page 2024

  4. [3]

    McGraw-Hill (1970)

    Birkhoff, G., Bartee, T.C.: Modern applied algebra. McGraw-Hill (1970)

    work page 1970

  5. [4]

    In: POPL

    ten Cate, B., Kappé, T.: Algebras for deterministic computation are inherently incomplete. In: POPL. pp. 25:1–25:27 (2025).https://doi.org/10.1145/3704861

    work page doi:10.1145/3704861 2025

  6. [5]

    Chen, H., Pucella, R.: A coalgebraic approach to Kleene algebra with tests. Theor. Comput. Sci.327(1-2), 23–44 (2004).https://doi.org/10.1016/j.tcs.2004.07. 020

    work page doi:10.1016/j.tcs.2004.07 2004

  7. [6]

    Cifuentes, C.: Reverse compilation techniques. Ph.D. thesis, Queensland University of Technology (1994)

    work page 1994

  8. [7]

    Cohen, E.: Hypotheses in Kleene algebra. Tech. rep., Bellcore (1994)

    work page 1994

Show all 54 references
  1. [8]

    Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Tech. Rep. TR96-1598, Cornell University (1996)

    1996

  2. [9]

    Chapman and Hall, Ltd., London (1971)

    Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London (1971)

    1971

  3. [10]

    In: CALCO

    Dahlqvist, F., Schmid, T.: How to write a coequation ((co)algebraic pearls). In: CALCO. pp. 13:1–13:25 (2021).https://doi.org/10.4230/LIPICS.CALCO.2021. 13

    2021 doi

  4. [11]

    ACM Trans

    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log.7(4), 798–833 (2006).https://doi.org/10.1145/1183278.1183285

    2006

  5. [12]

    ACM 11(3), 147–148 (1968).https://doi.org/10.1145/362929.362947

    Dijkstra,E.W.:Letterstotheeditor:gotostatementconsideredharmful.Commun. ACM 11(3), 147–148 (1968).https://doi.org/10.1145/362929.362947

    1968

  6. [13]

    Dijkstra, E.W.: On a somewhat disappointing correspondence (May 1987),http: //www.cs.utexas.edu/users/EWD/ewd10xx/EWD1009.PDF, circulated privately

    1987

  7. [14]

    In: FoSSaCS

    Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: FoSSaCS. pp. 207–223 (2019). https://doi.org/10.1007/ 978-3-030-17127-8_12

    2019

  8. [15]

    Goldblatt, R.: A comonadic account of behavioural covarieties of coalgebras. Math. Struct. Comput. Sci. 15(2), 243–269 (2005). https://doi.org/10.1017/ S096012950400458X

    2005

  9. [16]

    In: FoSSaCS

    Gomes, L., Baillot, P., Gaboardi, M.: BiGKAT: An algebraic framework for re- lational verification of probabilistic programs. In: FoSSaCS. pp. 243–264 (2025). https://doi.org/10.1007/978-3-031-90897-2_12

    2025 doi

  10. [17]

    In: LICS

    Grabmayer, C.: Milner’s proof system for regular expressions modulo bisimilarity is complete. In: LICS. pp. 34:1–34:13. ACM (2022).https://doi.org/10.1145/ 3531130.3532430, full version athttps://arxiv.org/abs/2209.12188

    2022

  11. [18]

    In: LICS

    Grabmayer, C., Fokkink, W.J.: A complete proof system for 1-free regular expres- sions modulo bisimilarity. In: LICS. pp. 465–478. ACM (2020).https://doi.org/ 10.1145/3373718.3394744

    2020

  12. [19]

    Hardin, C.: The Horn theory of relational Kleene algebra. Ph.D. thesis, Cornell University (2005)

    2005

  13. [20]

    Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Tech. Rep. TR71-114, Cornell University (1971)

    1971

  14. [21]

    In: Algebra, Meaning, and Computation, Essays Dedicated to Joseph On Propositional Program Equivalence (extended abstract) 15 A

    Jacobs, B.: A bialgebraic review of deterministic automata, regular expressions and languages. In: Algebra, Meaning, and Computation, Essays Dedicated to Joseph On Propositional Program Equivalence (extended abstract) 15 A. Goguen on the Occasion of His 65th Birthday. pp. 375–...

    2006 doi

  15. [22]

    In: FoSSaCS

    Kappé, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: From hypotheses to completeness. In: FoSSaCS. pp. 381–400 (2020). https://doi.org/10.1007/978-3-030-45231-5_20

    2020 doi

  16. [23]

    In: FoSSaCS

    Kappé, T., Schmid, T.: A general completeness theorem for skip-free star algebras. In: FoSSaCS. pp. 265–286 (2025). https://doi.org/10.1007/ 978-3-031-90897-2_13

    2025

  17. [24]

    In: ESOP

    Kappé, T., Schmid, T., Silva, A.: A complete inference system for skip-free guarded Kleene algebra with tests. In: ESOP. pp. 309–336 (2023).https://doi.org/10. 1007/978-3-031-30044-8_12, updated proofs found athttps://arxiv.org/abs/ 2301.11301

    2023 arXiv

  18. [25]

    Kappé, T.: An elementary proof of the FMP for Kleene algebra (2024),https: //arxiv.org/abs/2212.10931, to appear inFundamenta Informaticae

    2024

  19. [26]

    Addison-Wesley (1997)

    Knuth, D.E.: The art of computer programming, Volume I: Fundamental Algo- rithms, 3rd Edition. Addison-Wesley (1997)

    1997

  20. [27]

    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366–390 (1994). https://doi.org/10.1006/inco. 1994.1037

    1994

  21. [28]

    In: TACAS

    Kozen, D.: Kleene algebra with tests and commutativity conditions. In: TACAS. pp. 14–33 (1996).https://doi.org/10.1007/3-540-61042-1_35

    1996 doi

  22. [29]

    ACM Trans

    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.19(3), 427–443 (1997). https://doi.org/10.1145/256167.256195

    1997

  23. [30]

    In: STACS

    Kozen, D.: Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In: STACS. pp. 27–38 (2001). https://doi.org/10.1007/ 3-540-44693-1_3

    2001

  24. [31]

    Matematica Contem- poranea 24, 117–139 (2003)

    Kozen, D.: Automata on guarded strings and applications. Matematica Contem- poranea 24, 117–139 (2003)

    2003

  25. [32]

    In: ICALP

    Kozen, D., Mamouras, K.: Kleene algebra with equations. In: ICALP. pp. 280–292 (2014). https://doi.org/10.1007/978-3-662-43951-7_24

    2014 doi

  26. [33]

    Kozen, D., Patron, M.C.: Certification of compiler optimizations using Kleene algebra with tests. In: CL. pp. 568–582 (2000). https://doi.org/10.1007/ 3-540-44957-4_38

    2000

  27. [34]

    Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: CSL. pp. 244–259 (1996).https://doi.org/10.1007/3-540-63172-0_43

    1996 doi

  28. [35]

    Kozen, D., Tseng, W.D.: The Böhm-Jacopini theorem is false, propositionally. In: MPC. pp. 177–192 (2008).https://doi.org/10.1007/978-3-540-70594-9_11

    2008 doi

  29. [36]

    In: ICALP

    Krob, D.: A complete system of B-rational identities. In: ICALP. pp. 60–73 (1990). https://doi.org/10.1007/BFb0032022

    1990 doi

  30. [37]

    In: ICTAC

    Kuznetsov, S.L.: On the complexity of reasoning in Kleene algebra with com- mutativity conditions. In: ICTAC. pp. 83–99 (2023).https://doi.org/10.1007/ 978-3-031-47963-2_7

    2023

  31. [38]

    IRE Trans

    McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electronic Computers9(1), 39–47 (1960).https://doi.org/10.1109/ TEC.1960.5221603

    1960

  32. [39]

    Milner, R.: A complete inference system for a class of regular behaviours. J. Com- put. Syst. Sci.28(3), 439–466 (1984).https://doi.org/10.1016/0022-0000(84) 90023-0

    1984 doi

  33. [40]

    In: POPL

    Pous, D.: Symbolic algorithms for language equivalence and Kleene algebra with tests. In: POPL. pp. 357–368 (2015).https://doi.org/10.1145/2676726. 2677007 16 T. Kappé

    2015 doi

  34. [41]

    Pous, D., Rot, J., Wagemaker, J.: On tools for completeness of Kleene algebra with hypotheses. Log. Methods Comput. Sci.20(2) (2024). https://doi.org/10. 46298/LMCS-20(2:8)2024

    2024

  35. [42]

    Pous, D., Wagemaker, J.: Completeness theorems for Kleene algebra with tests and top. Log. Methods Comput. Sci.20(3) (2024). https://doi.org/10.46298/ LMCS-20(3:27)2024

    2024

  36. [43]

    In: IJCAR

    Rooduijn, J., Kozen, D., Silva, A.: A cyclic proof system for guarded Kleene algebra with tests. In: IJCAR. pp. 257–275 (2024).https://doi.org/10.1007/ 978-3-031-63501-4_14

    2024

  37. [44]

    In: ICALP (07 2023)

    Różowski, W., Kappé, T., Kozen, D., Schmid, T., Silva, A.: Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In: ICALP (07 2023). https://doi.org/10.4230/LIPIcs.ICALP.2023.136

    2023 doi

  38. [45]

    Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966).https://doi.org/10.1145/321312.321326

    1966

  39. [46]

    In: ICALP

    Schmid, T., Kappé, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. In: ICALP. pp. 142:1–142:14 (2021). https://doi.org/10.4230/LIPICS.ICALP.2021.142

    2021 doi

  40. [47]

    In: MFPS

    Schmid, T., Rot, J., Silva, A.: On star expressions and coalgebraic completeness theorems. In: MFPS. pp. 242–259 (2021).https://doi.org/10.4204/EPTCS.351. 15

    2021 doi

  41. [48]

    Sedlár, I.: Kleene algebra with dynamic tests: Completeness and complexity (2023), https://arxiv.org/abs/2311.06937

    2023 arXiv

  42. [50]

    Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215–225 (1975).https://doi.org/10.1145/321879.321884

    1975

  43. [51]

    Thompson, K.: Regular expression search algorithm. Commun. ACM11(6), 419– 422 (1968). https://doi.org/10.1145/363347.363387

    1968

  44. [52]

    Van Koevering, S., Rozowski, W., Silva, A.: Weighted GKAT: completeness and complexity (2025), https://arxiv.org/abs/2504.20385, to appear at ICALP 2025

    2025 arXiv

  45. [53]

    Watson, B.W.: A taxonomy of finite automata construction algorithms. Tech. rep., Technische Universiteit Eindhoven (1993), https://research.tue.nl/files/ 2482472/9313452

    1993

  46. [54]

    In: POPL

    Zhang, C., Kappé, T., Narváez, D.E., Naus, N.: CF-GKAT: Efficient validation of control-flow transformations. In: POPL. pp. 21:1–21:27 (2025).https://doi.org/ 10.1145/3704857

    2025 doi

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.