Kleene algebra with domain

被引：105
作者：
Desharnais, Jules [1 ]
Moeller, Bernhard
Struth, Georg
机构：
[1] Univ Laval, Dept Informat & Genie Logiciel, Quebec City, PQ G1K 7P4, Canada
[2] Univ Augsburg, Inst Informat, D-86135 Augsburg, Germany
[3] Univ Bundeswehr Munchen, Munich, Germany
来源：
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC | 2006年 / 7卷 / 04期
关键词：
theory; verification; idempotent semiring; Kleene algebra; domain; codomain; image and preimage operation; equational reasoning; state transition systems; program development and analysis;
D O I：
10.1145/1183278.1183285
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We propose Kleene algebra with domain (KAD), an extension of Kleene algebra by simple equational axioms for a domain and a codomain operation. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of programs and state transition systems. We develop the basic calculus, present the most interesting models and discuss some related theories. We demonstrate applicability by two examples: algebraic reconstructions of Noethericity and propositional Hoare logic based on equational reasoning.
引用
收藏
页码：798 / 833
页数：36
相关论文
共 39 条
[21]   A COMPLETENESS THEOREM FOR KLEENE ALGEBRAS AND THE ALGEBRA OF REGULAR EVENTS [J].
KOZEN, D .
INFORMATION AND COMPUTATION, 1994, 110 (02) :366-390
[22]  
Kozen D, 1997, LECT NOTES COMPUT SC, V1258, P244
[23]   Kleene algebra with tests [J].
Kozen, D .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (03) :427-443
[24]  
Kozen D, 1979, RC7864 IBM
[25]  
Kozen D., 1994, LOGIC INFORM FLOW, P78
[26]  
KOZEN D, 2001, T COMPUT LOGIC, V1, P60
[27]  
Kuich W., 1997, HDB FORMAL LANGUAGES, V1, P609, DOI [DOI 10.1007/978-3-642-59136-5_9, DOI 10.1007/978-3-642-59136-59]
[28]  
Loeckx Jacques, 1987, FDN PROGRAM VERIFICA, V2nd
[29]   Algebras of modal operators and partial correctness [J].
Möller, B ;
Struth, G .
THEORETICAL COMPUTER SCIENCE, 2006, 351 (02) :221-239
[30]  
MOLLER B, 2005, 20056 U AUGSB
1234