On Incorrectness Logic and Kleene Algebra with Top and Tests
summary
Kleene Algebra with Tests (KAT) cannot express incorrectness triples because it lacks an explicit codomain operation; adding a single top element yields TopKAT, which encodes codomains and makes incorrectness triples and all incorrectness-logic rules equationally provable. A small extra construct for abnormal termination (fail / epsilon) models errors and lets TopKAT subsume incorrectness logic with errors. Relational TopKATs do not add expressiveness beyond relational KAT, and TopKAT equality remains decidable and PSPACE-complete.
AI-written summary · about