Augmenting Branching Temporal Logics with
Existential Quantification over Atomic Propositions
---------------------------------------------------
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.