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 条
  • [31] Kleene Algebra Modulo Theories
    Greenberg, Michael
    Beckett, Ryan
    Campbell, Eric
    PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22), 2022, : 594 - 608
  • [32] TOWARDS KLEENE ALGEBRA WITH RECURSION
    LEISS, H
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 242 - 256
  • [33] An axiomatization of arrays for Kleene algebra with tests
    Aboul-Hosn, Kamal
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2006, 4136 : 63 - 77
  • [34] Completeness and Incompleteness in Nominal Kleene Algebra
    Kozen, Dexter
    Mamouras, Konstantinos
    Silva, Alexandra
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2015), 2015, 9348 : 51 - 66
  • [35] On Hoare logic, Kleene algebra, and types
    Kozen, D
    IN THE SCOPE OF LOGIC: METHODOLOGY & PHILOSOPHY OF SCIENCE, 2002, 315 : 119 - 133
  • [36] A Quest for Kleene Algebra in 2 Dimensions
    Stefanescu, Gheorghe
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2015), 2015, 9348 : 3 - 26
  • [37] Concurrent Kleene Algebra and its Foundations
    Hoare, Tony
    Moeller, Bernhard
    Struth, Georg
    Wehrman, Ian
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2011, 80 (06): : 266 - 296
  • [38] Modal Kleene algebra and partial correctness
    Möller, B
    Struth, G
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 379 - 393
  • [39] A coalgebraic approach to Kleene algebra with tests
    Chen, HB
    Pucella, R
    THEORETICAL COMPUTER SCIENCE, 2004, 327 (1-2) : 23 - 44
  • [40] Investigating discrete controllability with Kleene algebra
    Bherer, H
    Desharnais, J
    Frappier, M
    St-Denis, R
    RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, 2003, 3051 : 74 - 85