Kleene Algebra with Domain (KAD)

Title: Kleene Algebra with Domain (KAD)

Research Question: How can we extend Kleene Algebra (KAT) to better model and analyze state transition systems?

Methodology: The researchers proposed Kleene Algebra with Domain (KAD), an extension of KAT with two additional axioms for a domain and a codomain operation. This allows for a more expressive language for specifying and analyzing state transition systems.

Results: The authors developed the basic calculus of KAD, discussed related theories, and presented models. They demonstrated the applicability of KAD by reconstructing Noetherianity and well-foundedness, and by reconstructing propositional Hoare logic.

Implications: KAD significantly extends the expressiveness of KAT, making it more suitable for modeling and analyzing state transition systems. This can lead to more accurate and efficient verification of software systems.

Link to Article: https://arxiv.org/abs/0310054v1 Authors: arXiv ID: 0310054v1