一句话：提出 GKAT，利用其（余）代数理论，使未解释命令式程序的等式推理达到近乎线性时间。
GKAT 是通过对 KAT 的并（+）与迭代（*）施加谓词守卫限制而得到的变体。本文建立 GKAT 的（余）代数理论，并将其用于命令式程序的推理。与等式理论为 PSPACE 完全的 KAT 不同，作者证明 GKAT 的等式理论可在（几乎）线性时间内判定，并给出完整的 Kleene 定理，证明 Salomaa 式 Kleene 代数公理的对应版本具有完备性。该结果为未解释程序的验证提供了高效的代数基础。
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
@article{paperbot535,
title = {Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time},
author = {Steffen Smolka and Nate Foster and Justin Hsu and Tobias Kappé and Dexter Kozen and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371129}
}