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 条
  • [1] Kleene algebra with domain
    Desharnais, Jules
    Moeller, Bernhard
    Struth, Georg
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2006, 7 (04) : 798 - 833
  • [2] On the complexity of reasoning in Kleene algebra
    Kozen, D
    INFORMATION AND COMPUTATION, 2002, 179 (02) : 152 - 162
  • [3] On the complexity of reasoning in Kleene algebra
    Kozen, D
    12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 195 - 202
  • [4] On the expressive power of Kleene algebra with domain
    Struth, Georg
    INFORMATION PROCESSING LETTERS, 2016, 116 (04) : 284 - 288
  • [5] Kleene Algebra of Weighted Programs with Domain
    Sedlar, Igor
    DYNAMIC LOGIC. NEW TRENDS AND APPLICATIONS, DALI 2023, 2024, 14401 : 52 - 67
  • [6] On the Complexity of Reasoning in Kleene Algebra with Commutativity Conditions
    Kuznetsov, Stepan L.
    THEORETICAL ASPECTS OF COMPUTING, ICTAC 2023, 2023, 14446 : 83 - 99
  • [7] How the location of * influences complexity in Kleene algebra with tests
    Hardin, C
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3452 : 224 - 239
  • [8] Implicational Kleene algebra with domain and the substructural logic of partial correctness
    Sedlar, Igor
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2024, 34 (07) : 645 - 660
  • [9] Kleene Algebra with Hypotheses
    Doumane, Amina
    Kuperberg, Denis
    Pous, Damien
    Pradic, Pierre
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2019, 2019, 11425 : 207 - 223
  • [10] Synchronous Kleene algebra
    Prisacariu, Cristian
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2010, 79 (07): : 608 - 635