Memoryful Branching-Time Logic
Traditional branching-time logics such as CTL* are
memoryless: once a path in the computation tree is quantified at a
given node, the computation that led to that node is forgotten. Recent
work in planning suggests that CTL* cannot easily express
temporal goals that refer to whole computations. Such goals
require memoryful quantification of paths. With such a memoryful
quantification, $E\psi$ holds at a node $s$ of a computation tree if
there is a path $\pi$ starting at the root of the tree and going
through $s$ such that $\pi$ satisfies the linear-time formula $\psi$.
We define the memoryful branching-time logic mCTL*
and study its expressive power and algorithmic properties.
We show that mCTL* is as expressive, but exponentially more
succinct, than CTL*, and that the ability of mCTL* to refer
to the present is essential for this equivalence. From the algorithmic
point of view, while the satisfiability problem for mCTL* is
2EXPTIME-complete --- not harder than that of CTL*, its
model-checking problem is EXPSPACE-complete --- exponentially harder
than that of CTL*. The upper bounds are obtained by extending the
automata-theoretic approach to handle memoryful quantification, and
are much more efficient than these obtained by translating mCTL* to
branching logics with past. The EXPSPACE lower bound for the
model-checking problem applies already to formulas of restricted form
(in particular, to $AGE\psi$, which is useful for specifying
possibility properties), and implies that reasoning about a memoryful
branching-time logic is harder than reasoning about the linear-time
logic of its path formulas.