What Triggers a Behavior?

We introduce and study {\em trigger querying}.  Given a model M and a
temporal behavior \varphi, trigger querying is the problem of finding
the set of scenarios that trigger \varphi in M. That is, if a
computation of M has a prefix that follows the scenario, then its
suffix satisfies \varphi. Trigger querying enables one to find, for
example, given a program with a function f, the scenarios that lead to
calling f with some parameter value, or to find, given a hardware
design with signal \err, the scenarios after which the signal \err
aught to be eventually raised.

We formalize trigger querying using the temporal operator \triggers
(triggers), which is the most useful operator in modern industrial
specification languages.  A regular expression r triggers an LTL
formula \varphi in a system M, denoted M \models r \triggers \varphi,
if for every computation \pi of M and index i \geq 0, if the prefix of
\pi up to position i is a word in the language of r, then the suffix
of \pi from position i satisfies \varphi.  The solution to the trigger
query M \models ? \triggers \varphi is the maximal regular expression
that triggers \varphi in M.  Trigger querying is useful for studying
systems, and it significantly extends the practicality of traditional
query checking [Chan00]. Indeed, in traditional query checking,
solutions are restricted to propositional assertions about states of
the systems, whereas in our setting the solutions are temporal
scenarios.


We show that the solution to a trigger query M \models ? \triggers
\varphi is regular, and can be computed in polynomial space.
Unfortunately, the polynomial-space complexity is in the size
of M. Consequently, we also study {\em partial trigger querying},
which returns a (non empty) subset of the solution, and is more
feasible. Other extensions we study are {\em observable trigger
querying}, where the partial solution has to refer only to a subset of
the atomic propositions, {\em constrained trigger querying}, where in
addition to M and \varphi, the user provides a regular constraint c
and the solution is the set of scenarios respecting c that trigger
\varphi in M, and {\em relevant trigger querying}, which excludes
vacuous triggers --- scenarios that are not induced by a prefix of a
computation of M.  Trigger querying can be viewed as the problem of
finding sufficient conditions for a behavior \varphi in M. We also
consider the dual problem, of finding necessary conditions to \varphi,
and show that it can be solved in space complexity that is only
logarithmic in M.