Canonical finite models of Kleene algebra with tests

DOI10.1016/j.jlamp.2015.11.001zbMath1407.68321OpenAlexW2213295336WikidataQ114851591 ScholiaQ114851591MaRDI QIDQ299196

Takeo Uramoto

Publication date: 22 June 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.11.001

zbMATH Keywords

regular languagecompleteness theoremprogram optimizationcanonical finite modelKleene algebra with testssyntactic semiring

Mathematics Subject Classification ID

Algebraic theory of languages and automata (68Q70) Decidability of theories and sets of sentences (03B25)

Uses Software

• KAT-ML
• NetKAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A coalgebraic approach to Kleene algebra with tests
• Dynamic algebras: Examples, constructions, applications
• A completeness theorem for Kleene algebras and the algebra of regular events
• Characterizations of locally testable events
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• KAT + B!
• Kleene Algebra with Equations
• Mathematical Foundations of Computer Science 2004
• On finite monoids having only trivial subgroups
• NetKAT
• A Modified Completeness Theorem of KAT and Decidability of Term Reducibility
• On Hoare logic and Kleene algebra with tests