Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/39502
Title: Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
Authors: Cook, Byron
Khlaaf, Heidy
Piterman, Nir
First Published: 18-May-2017
Publisher: Association for Computing Machinery (ACM)
Citation: Journal of the ACM, 2017, 64(2), Article No. 15
Abstract: Temporal logic is a formal system for specifying and reasoning about propositions qualified in terms of time. It offers a unified approach to program verification as it applies to both sequential and parallel programs and provides a uniform framework for describing a system at any level of abstraction. Thus a number of automated systems have been proposed to exclusively reason about either Computation-Tree Logic (CTL) or Linear Temporal Logic (LTL) in the infinite-state setting. Unfortunately, these logics have significantly reduced expressiveness as they restrict the interplay between temporal operators and path quantifiers, thus disallowing the expression of many practical properties, for example “along some future an event occurs infinitely often”. Contrarily, CTL∗, a superset of both CTL and LTL, can facilitate the interplay between path-based and state-based reasoning. CTL∗ thus exclusively allows for the expressiveness of properties involving existential system stabilization and “possibility” properties. Until now, there have not existed automated systems that allow for the verification of such expressive CTL∗ properties over infinite-state systems. This paper proposes a method capable of such a task, thus introducing the first known fully automated tool for symbolically proving CTL∗ properties of (infinite-state) integer programs. The method uses an internal encoding that admits reasoning about the subtle interplay between the nesting of temporal operators and path quantifiers that occurs within CTL∗ proofs. A program transformation is first employed that trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We then synthesize and quantify preconditions over the transformed program that represent program states that satisfy a CTL∗ formula. This paper demonstrates the viability of our approach in practice, thus leading to a new class of fullyautomated tools capable of proving crucial properties that no tool could previously prove. Additionally, we consider the linear-past extension to CTL∗ for infinite-state systems in which the past is linear and each moment in time has a unique past. We discuss the practice of this extension and how it is further supported through the use of history variables. We have implemented our approach and report our benchmarks carried out on case studies ranging from smaller programs to demonstrate the expressiveness of CTL∗ specifications, to larger code bases drawn from device drivers and various industrial examples
DOI Link: 10.1145/3060257
ISSN: 1535-9921
Links: http://dl.acm.org/citation.cfm?id=3060257
http://hdl.handle.net/2381/39502
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © 2017, Association for Computing Machinery (ACM). Deposited with reference to the publisher’s open access archiving policy.
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
jacm-ctlstar.pdfPost-review (final submitted author manuscript)643.75 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.