Augmenting branching temporal logics with existential quantification over atomic propositions

Abstract

In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal logic formula that specifies this behavior. One of the ways to overcome the expressiveness limitation of temporal logics is to augment them with quantification over atomic propositions. In this paper we consider the extension of branching temporal logics with existential quantification over atomic propositions. Once we add existential quantification to a branching temporal logic, it becomes sensitive to unwinding. That is, unwinding a structure into an infinite tree does not preserve the set of formulas it satisfies. Accordingly, we distinguish between two semantics, two practices as specification languages, and two versions of the model-checking problem for such a logic. One semantics refers to the structure that models the program, and the second semantics refers to the infinite computation tree that the program induces. We examine the complexity of the model-checking problem in the two semantics for the logics CTL and CTL* augmented with existential quantification over atomic propositions. Following the cheerless results that we get, we examine also the program complexity of model checking; i.e., the complexity of this problem in terms of the program, assuming the formula is fixed. We show that while fixing the formula dramatically reduces model-checking complexity in the tree semantics, its influence on the structure semantics is poor.