Logic in Computer Science (LICS 2004)

Paper: Proving Termination Assertions in Dynamic Logics (at LICS 2004)

Authors: Daniel Leivant

Abstract

Total correctness assertions (TCAs) have long been considered a natural formalization of successful program termination. However, research dating back to the 1980s suggests that validity of TCAs is a notion of limited interest; we corroborate this by proving compactness and Herbrand properties for the valid TCAs, defining in passing a new sound, complete, and syntax-directed deductive system for TCAs. It follows that proving TCAs whose truth depends on underlying inductive data-types is impossible in logics of programs that are sound for all structures, such as Dynamic Logic based on Segerberg's PDL, even when augmented with powerful first-order theories like Peano Arithmetic. Harel's Convergence Rule bypasses this difficulty, but is methodologically and conceptually problematic, in addition to being unsound for general validity. We propose instead to bind variables to inductive data via DL's box operator, leading to an alternative formalization of termination assertions, which we dub Inductive TCA (ITCA). We observe that a TCA is provable in Harel's DL exactly when the corresponding ITCA is provable in Segerberg's DL, thereby showing that the Convergence Rule is not foundationally or practically necessary. We also show that validity of ITCAs is directly reducible to validity of partial correctness assertions, confirming the foundational importance of the latter.

BibTeX

  @InProceedings{Leivant-ProvingTerminationA,
    author = 	 {Daniel Leivant},
    title = 	 {Proving Termination Assertions in Dynamic Logics},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {89--98},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }