Robust Satisfaction
===================

In order to check whether an open system satisfies a desired property,
we need to check the behavior of the system with respect to an
arbitrary environment.  In the most general setting, the environment
is another open system. Given an open system M and a property \psi, we
say that M robustly satisfies \psi iff for every open system M', which
serves as an environment to M, the composition M||M' satisfies \psi.
The problem of robust model checking is then to decide, given M and
\psi, whether M robustly satisfies \psi.  In this paper we study the
robust-model-checking problem.  We consider systems modeled by
nondeterministic Moore machines, and properties specified by branching
temporal logic (for linear temporal logic, robust satisfaction
coincides with usual satisfaction).  We show that the complexity of
the problem is EXPTIME-complete for CTL and the \mu-calculus, and is
2EXPTIME-complete for CTL*.  We partition branching temporal logic
formulas into three classes: universal, existential, and mixed
formulas. We show that each class has different sensitivity to the
robustness requirement. In particular, unless the formula is mixed,
robust model checking can ignore nondeterministic environments.  In
addition, we show that the problem of classifying a CTL formula into
these classes is EXPTIME-complete.