TY - JOUR
T1 - 2D dependency pairs for proving operational termination of CTRSs
AU - Lucas, Salvador
AU - Meseguer, José
N1 - Funding Information:
Research partially supported by NSF grant CNS 13-19109. Salvador Lucas’ research was developed during a sabbatical year at the CS Dept. of the UIUC and was also partially supported by Spanish MECD grant PRX12/00214, MINECO project TIN2010-21062-C02-02, and GV grant BEST/2014/026 and project PROMETEO/2011/052.
Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - The notion of operational termination captures nonterminating computations due to subsidiary processes that are necessary to issue a single ‘main’ step but which often remain ‘hidden’ when the main computation sequence is observed. This highlights two dimensions of nontermination: one for the infinite sequencing of computation steps, and the other that concerns the proof of some single steps. For conditional term rewriting systems (CTRSs), we introduce a new dependency pair framework which exploits the bidimensional nature of conditional rewriting (rewriting steps + satisfaction of the conditions as reachability problems) to obtain a powerful and more expressive framework for proving operational termination of CTRSs.
AB - The notion of operational termination captures nonterminating computations due to subsidiary processes that are necessary to issue a single ‘main’ step but which often remain ‘hidden’ when the main computation sequence is observed. This highlights two dimensions of nontermination: one for the infinite sequencing of computation steps, and the other that concerns the proof of some single steps. For conditional term rewriting systems (CTRSs), we introduce a new dependency pair framework which exploits the bidimensional nature of conditional rewriting (rewriting steps + satisfaction of the conditions as reachability problems) to obtain a powerful and more expressive framework for proving operational termination of CTRSs.
KW - Conditional term rewriting
KW - Dependency pairs
KW - Operational termination
KW - Program analysis
UR - http://www.scopus.com/inward/record.url?scp=84911972406&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84911972406&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-12904-4_11
DO - 10.1007/978-3-319-12904-4_11
M3 - Article
AN - SCOPUS:84911972406
VL - 8663
SP - 195
EP - 212
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SN - 0302-9743
ER -