Towards Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems

Heidy Khlaaf

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. In this talk, I will cover the logics CTL, LTL, Fair-CTL and CTL*, and a number of automated systems that have been proposed to exclusively reason about either CTL or 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 a many practical properties. I will thus introduce the the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs, and discuss the implications and usage of CTL* over infinite-state systems.

Talks and Publications: