Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/39502
Full metadata record
DC FieldValueLanguage
dc.contributor.authorCook, Byron-
dc.contributor.authorKhlaaf, Heidy-
dc.contributor.authorPiterman, Nir-
dc.date.accessioned2017-03-20T09:56:18Z-
dc.date.available2017-06-15T01:45:08Z-
dc.date.issued2017-05-18-
dc.identifier.citationJournal of the ACM, 2017, 64(2), Article No. 15en
dc.identifier.issn1535-9921-
dc.identifier.urihttp://dl.acm.org/citation.cfm?id=3060257en
dc.identifier.urihttp://hdl.handle.net/2381/39502-
dc.description.abstractTemporal 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 examplesen
dc.language.isoenen
dc.publisherAssociation for Computing Machinery (ACM)en
dc.rightsCopyright © 2017, Association for Computing Machinery (ACM). Deposited with reference to the publisher’s open access archiving policy.en
dc.subjectModel Checkingen
dc.subjectCTL∗en
dc.titleVerifying Increasingly Expressive Temporal Logics for Infinite-State Systemsen
dc.typeJournal Articleen
dc.identifier.doi10.1145/3060257-
dc.description.statusPeer-revieweden
dc.description.versionPost-printen
dc.type.subtypeArticle-
pubs.organisational-group/Organisationen
pubs.organisational-group/Organisation/COLLEGE OF SCIENCE AND ENGINEERINGen
pubs.organisational-group/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Scienceen
dc.dateaccepted2017-02-14-
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.