Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

被引：4
|
作者：
Kassing, Jan-Christoph [1 ]
Giesl, Juergen [1 ]
机构：
[1] Rhein Westfal TH Aachen, LuFG Informat 2, Aachen, Germany
来源：
AUTOMATED DEDUCTION, CADE 29 | 2023年 / 14132卷
关键词：
COMPLEXITY; BYTECODE;
D O I：
10.1007/978-3-031-38499-8_20
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost termination of probabilistic TRSs. To evaluate its power, we implemented the new framework in our tool AProVE.
引用
收藏
页码：344 / 364
页数：21
相关论文
共 50 条
  • [1] A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
    Kassing, Jan-Christoph
    Dollase, Stefan
    Giesl, Jurgen
    FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2024, 2024, 14659 : 62 - 80
  • [2] From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
    Kassing, Jan-Christoph
    Frohn, Florian
    Giesl, Jurgen
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PT II, FOSSACS 2024, 2024, 14575 : 206 - 228
  • [3] Proving positive almost-sure termination
    Bournez, O
    Garnier, F
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2005, 3467 : 323 - 337
  • [4] Proving Almost-Sure Termination by Omega-Regular Decomposition
    Chen, Jianhui
    He, Fei
    PROCEEDINGS OF THE 41ST ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '20), 2020, : 869 - 882
  • [5] Termination of innermost context-sensitive rewriting using dependency pairs
    Alarcon, Beatriz
    Lucas, Salvador
    FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 73 - +
  • [6] New Approaches for Almost-Sure Termination of Probabilistic Programs
    Huang, Mingzhang
    Fu, Hongfei
    Chatterjee, Krishnendu
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018, 2018, 11275 : 181 - 201
  • [7] Dependency pairs for proving termination properties of conditional term rewriting systems
    Lucas, Salvador
    Meseguer, Jose
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2017, 86 (01) : 236 - 268
  • [8] Modular Verification for Almost-Sure Termination of Probabilistic Programs
    Huang, Mingzhang
    Fu, Hongfei
    Chatterjee, Krishnendu
    Goharshady, Amir Kafshdar
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (OOPSLA):
  • [9] Termination of term rewriting using dependency pairs
    Arts, T
    Giesl, J
    THEORETICAL COMPUTER SCIENCE, 2000, 236 (1-2) : 133 - 178
  • [10] Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs
    Uchiyama, Keita
    Sakai, Masahiko
    Sakabe, Toshiki
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2010, E93D (05) : 953 - 962
12345