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 条

[1]

AARTS CJ, 1992, THESIS EINDHOVEN U T

[2]

Abrial J.-R., 1996, The B-Book

[3]

[Anonymous], 1980, Modal Logic: An Introduction, DOI DOI 10.1017/CBO9780511621192

[4]

APT K. R, 1997, VERIFICATION SEQUENT

[5]

BIRKHOFF G, 1984, C PUBLICATIONS AM MA, V25

[6]

Bull R., 1984, HDB PHILOS LOGIC, VII, P1, DOI DOI 10.1007/978-94-009-6259-0_1

[7]

Cohen E, 2000, LECT NOTES COMPUT SC, V1837, P45

[8]

COHEN E, 1993, TMARH023814 BELLC

[9]

CONWAY JH, 1971, REGULAR ALGEBRA FINI

[10] The variety of Kleene algebras with conversion is not finitely based [J].

Crvenkovic, S ;

Dolinka, I ;

Ésik, Z .

THEORETICAL COMPUTER SCIENCE, 2000, 230 (1-2) :235-245

← 1 2 3 4 →