  We present a technique for automatically extracting mutual exclusion
invariants from temporal planning instances. It first identifies a set of
invariant templates by inspecting the lifted representation of the domain and
then checks these templates against properties that assure invariance. Our
technique builds on other approaches to invariant synthesis presented in the
literature, but departs from their limited focus on instantaneous actions by
addressing temporal domains. To deal with time, we formulate invariance
conditions that account for the entire structure of the actions and the
possible concurrent interactions between them. As a result, we construct a
significantly more comprehensive technique than previous methods, which is able
to find not only invariants for temporal domains, but also a broader set of
invariants for non-temporal domains. The experimental results reported in this
paper provide evidence that identifying a broader set of invariants results in
the generation of fewer multi-valued state variables with larger domains. We
show that, in turn, this reduction in the number of variables reflects
positively on the performance of a number of temporal planners that use a
variable/value representation by significantly reducing their running time.
