|
New: Presentations:
When can we ignore stuff?: presentation to NASA AMES, July 2003.
(For the latest of LURCH, see Owen03a)
Hard problems (worst-case intractable) like program
verification exhibit a phase transition shown here:
Note the standard features of the phase transisition:
-
An easy range of problem instances ;
-
A range for
which it is practically impossible to find a solution;
-
and a narrow band, the phase transition, separating
the two regions [Owen00a].
We are working on LURCH, an alternative
to model checking. LURCH is a tool that exploits the hypothetical
easy range , so that models can be verified
quickly without using so much memory, and as a side
benefit makes possible features that greatly simplify
the modeling task.
How is it possible to exploit the easy range? We
do this by using a partial, random search:
- Partial,
because unlike other model checking tools, the whole
space of possible behaviors is not explored;
- Random,
because the choice of which behavior to explore is nondeterministic.
For input models in the easy range, a
random sample of possible behaviors will tell us nearly
everything we could learn from an exhaustive search
(for these models exhaustive search is simply overkill).
And for models in the too hard range, where the partial,
random search is not effective, exhaustive search
is intractable.
Or, as stated by Knuth in more general terms:
No
matter what complicated thing you have, . . . there's a
fairly good chance that random sampling will give insight.
Of course if you start with purely random data
[e.g., the worst-case end of the the too hard range], then
random sampling is going to tell you that it is purely
random data [Knuth01a]
Elsewhere similar ideas about how program structure
determines whether a verification problem falls
into the easy range are expressed in terms of funnels or
small backbones [Menzies01a]. A funnel is a small set of key variables
that largely determine the behavior of the entire
system; if an execution path stumbles into the funnel,
it will nearly always be directed to the same behavior.
Easy range models are easier to verify (and arguably
more testable [Owen00a,Owen00b]) because they contain funnels. In
these models a comparatively small amount of exploration
is likely to quickly find the key variables and
therefore everything its possible to find.
|