On the expressive power of Kleene algebra with domain

DOI10.1016/J.IPL.2015.11.007MaRDI QIDQ903368zbMATH OpenOpenAlexFDO

Authors Georg Struth

Publication date 5 January 2016

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.07246

zbMATH Keywords

Hoare logicsemiringsprogram correctnessexpressive powerKleene algebras

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semirings (16Y60)

Abstract: It is shown that antidomain semirings are more expressive than test semirings and that Kleene algebras with domain are more expressive than Kleene algebras with tests. It is also shown that Kleene algebras with domain are expressive for propositional Hoare logic whereas Kleene algebras with tests are not.

Recommendations

• On the complexity of Kleene algebra with domain
• Kleene algebra with domain
• Free Kleene algebras with domain
• On Kleene algebras
• On the complexity of reasoning in Kleene algebra
• scientific article; zbMATH DE number 408802
• Kleene algebras with implication
• Kleene algebra with hypotheses
• On the expressive power of \textsc{Klaim}-based calculi
• On the expressive power of \textsc{Klaim}-based calculi

Cites work

• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• Algebras of modal operators and partial correctness
• Domain Axioms for a Family of Near-Semirings
• Internal axioms for domain semirings
• Kleene algebra with domain
• On Hoare logic and Kleene algebra with tests

Cited in

(4)

• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Kleene algebra with domain
• On the complexity of reasoning in Kleene algebra
• On the complexity of Kleene algebra with domain

This page was built for publication: On the expressive power of Kleene algebra with domain

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q903368)