What Triggers a Behavior?

We introduce and study trigger querying. Given a model M and a temporal behavior vartheta, trigger querying is the problem of finding the set of scenarios that trigger vartheta in M. That is, if a computation of M has a prefix that follows the scenario, then its suffix satisfies vartheta. 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 ought to be eventually raised. We formalize trigger querying using the temporal operator mapsto (triggers), which is the most useful operator in modern industrial specification languages. A regular expression r triggers an LTL formula vartheta in a system M, denoted M {text{M | = r }} mapsto vartheta, if for every computation pi of M and index i geqslant 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 vartheta. The solution to the trigger query {text{M | = ?}} mapsto vartheta is the maximal regular expression that triggers vartheta in M. Trigger querying is useful for studying systems, and it significantly extends the practicality of traditional query checking [6]. 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 {text{M | = ?}} mapsto vartheta is regular, and can be computed in polynomial space. Unfortunately, the polynomial-space complexity is in the size of M. Consequently, we also study partial trigger querying, which returns a (non empty) subset of the solution, and is more feasible. Other extensions we study are observable trigger querying, where the partial solution has to refer only to a subset of the atomic propositions, constrained trigger querying, where in addition - to M and vartheta, the user provides a regular constraint c and the solution is the set of scenarios respecting c that trigger vartheta in M, and 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 vartheta in M. We also consider the dual problem, of finding necessary conditions to vartheta, and show that it can be solved in space complexity that is only logarithmic in M.