Amir Pnueli: A Compositional Approach to Verification (both Deductive and Algorithmic) of CTL* Properties

Abstract: One of the well-known advantages of the temporal logic CTL is that its finite-state algorithmic verification (model checking) can be executed in a modular (compositional fashion). That is, the task of verifying a complex CTL formula f can be broken into several subtasks, each dealing with a sub-formula of f, associated with a single temporal operator. This explains the polynomial complexity of CTL model checking.

In contrast, algorithmic verification of the more expressive LTL temporal logic, known to be PSAPCE complete, has traditionally been carried out as a monolithic task, based on the construction of tableau for the full LTL formula or translating it into an automaton.

In this work, we consider the maximally expressive temporal logic CTL*, which contains both CTL and LTL as fragments. We show that verification of any CTL* formula f can be done in a compositional way, treating separately each sub-formula of f. The compositional approach is based on two reduction principles which, respectively, get rid of each temporal operator and each path quantifier, one at a time.

Based on these reduction principles, we present first a relatively complete deductive verification system for CTL*, and then briefly discuss their application for a compositional model-checking approach for arbitrary CTL* formulas over fair reactive finite-state systems. The model-checking algorithm has been implemented on the Weizmann Institute's TLV verification system.

This is a joint work with Yonit Kesten and Elad Shahar.