On the Complexity of Kleene Algebra with Domain

被引：2
|
作者：
Sedlar, Igor [1 ]
机构：
[1] Czech Acad Sci, Inst Comp Sci, Prague, Czech Republic
来源：
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, RAMICS 2023 | 2023年 / 13896卷
关键词：
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 条
  • [21] Foundations of Concurrent Kleene Algebra
    Hoare, C. A. R.
    Moeller, Bernhard
    Struth, Georg
    Wehrman, Ian
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2009, 5827 : 166 - +
  • [22] Concurrent Kleene Algebra with Tests
    Jipsen, Peter
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014), 2014, 8428 : 37 - 48
  • [23] Kleene Algebra and Bytecode Verification
    Kot, Lucja
    Kozen, Dexter
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 141 (01) : 221 - 236
  • [24] Developments in concurrent Kleene algebra
    Hoare, Tony
    van Staden, Stephan
    Moeller, Bernhard
    Struth, Georg
    Zhu, Huibiao
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2016, 85 (04) : 617 - 636
  • [25] Developments in Concurrent Kleene Algebra
    Hoare, Tony
    van Staden, Stephan
    Moeller, Bernhard
    Struth, Georg
    Zhu, Huibiao
    Villard, Jules
    Hearn, Peter O.
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014), 2014, 8428 : 1 - 18
  • [26] Kleene Algebra of Partial Predicates
    Kornilowicz, Artur
    Ivanov, Ievgen
    Nikitchenko, Mykola
    FORMALIZED MATHEMATICS, 2018, 26 (01): : 11 - 20
  • [27] Monodic tree kleene algebra
    Takai, Toshinori
    Furusawa, Hitoshi
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2006, 4136 : 402 - 416
  • [28] Proof theory for Kleene algebra
    Hardin, C
    LICS 2005: 20TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE - PROCEEDINGS, 2005, : 290 - 299
  • [29] Probabilistic Concurrent Kleene Algebra
    McIver, Annabelle
    Rabehaja, Tahiry
    Struth, Georg
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (117): : 97 - 115
  • [30] 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
12345