2D dependency pairs for proving operational termination of CTRSs

Salvador Lucas; José Meseguer

doi:10.1007/978-3-319-12904-4_11

2D dependency pairs for proving operational termination of CTRSs

Research output: Contribution to journal › Article

Abstract

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.

Original language	English (US)
Pages (from-to)	195-212
Number of pages	18
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8663
DOIs	https://doi.org/10.1007/978-3-319-12904-4_11
State	Published - Jan 1 2014

Fingerprint

Keywords

Conditional term rewriting
Dependency pairs
Operational termination
Program analysis

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Cite this

Lucas, S., & Meseguer, J. (2014). 2D dependency pairs for proving operational termination of CTRSs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8663, 195-212. https://doi.org/10.1007/978-3-319-12904-4_11

@article{dde2f380dc0f49b0ba684ef06a3fe68e,

title = "2D dependency pairs for proving operational termination of CTRSs",

abstract = "The notion of operational termination captures nonterminating computations due to subsidiary processes that are necessary to issue a single {\textquoteleft}main{\textquoteright} step but which often remain {\textquoteleft}hidden{\textquoteright} 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.",

keywords = "Conditional term rewriting, Dependency pairs, Operational termination, Program analysis",

author = "Salvador Lucas and Jos{\'e} Meseguer",

year = "2014",

month = jan

day = "1",

doi = "10.1007/978-3-319-12904-4_11",

language = "English (US)",

volume = "8663",

pages = "195--212",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - 2D dependency pairs for proving operational termination of CTRSs

AU - Lucas, Salvador

AU - Meseguer, José

PY - 2014/1/1

Y1 - 2014/1/1

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 -

Access to Document

10.1007/978-3-319-12904-4_11