On the Complexity of Kleene Algebra with Domain

被引:2
|
作者
Sedlar, Igor [1 ]
机构
[1] Czech Acad Sci, Inst Comp Sci, Prague, Czech Republic
关键词
Complexity; Kleene algebra; Kleene algebra with domain; Propositional dynamic logic; Test algebra; COMPLETENESS; AXIOMS;
D O I
10.1007/978-3-031-28083-2_13
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We prove that the equational theory of Kleene algebra with domain is EXPTIME-complete. Our proof makes essential use of Hollenberg's equational axiomatization of program equations valid in relational test algebra. We also show that the equational theory of Kleene algebra with domain coincides with the equational theory of *-continuous Kleene algebra with domain.
引用
收藏
页码:208 / 223
页数:16
相关论文
共 50 条
  • [41] Weak Kleene algebra and computation trees
    Cohen, Ernie
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2006, 4136 : 1 - 1
  • [42] A Kleene Algebra of Tagged System Actors
    Dey, Soumyajit
    Sarkar, Dipankar
    Basu, Anupam
    IEEE EMBEDDED SYSTEMS LETTERS, 2011, 3 (01) : 28 - 31
  • [43] Position Automata for Kleene Algebra with Tests
    Silva, Alexandra
    SCIENTIFIC ANNALS OF COMPUTER SCIENCE, 2012, 22 (02) : 367 - 394
  • [44] Automatic proof generation in Kleene algebra
    Worthington, James
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, 2008, 4988 : 382 - 396
  • [45] Completeness and Incompleteness of Synchronous Kleene Algebra
    Wagemaker, Jana
    Bonsangue, Marcello
    Kappe, Tobias
    Rot, Jurriaan
    Silva, Alexandra
    MATHEMATICS OF PROGRAM CONSTRUCTION, 2019, 11825 : 385 - 413
  • [46] Kleene algebra with tests: Completeness and decidability
    Kozen, D
    Smith, F
    COMPUTER SCIENCE LOGIC, 1997, 1258 : 244 - 259
  • [47] A framework for Kleene algebra with an embedded structure
    Furusawa, Hitoshi
    RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, 2006, 3929 : 96 - 107
  • [48] Completeness and incompleteness in nominal Kleene algebra
    Kozen, Dexter
    Mamouras, Konstantinos
    Silva, Alexandra
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2017, 91 : 17 - 32
  • [49] On hoare logic and Kleene algebra with tests
    Cornell Univ, Ithaca, United States
    Proc Symp Logic Comput Sci, (167-172):
  • [50] Image segmentation based on Kleene algebra
    Hata, Y
    Ishikawa, M
    Kamiura, N
    1998 28TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC - PROCEEDINGS, 1998, : 155 - 160