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 P and a property Q , we say that P robustly satisfies Q iff for every open system PSR , which serves as an environment to P , the composition PUTP R satisfies Q . The problem of robust model checking is then to decide, given P and Q , whether P robustly satisfies Q . 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 V -calculus, and is 2EXPTIME-complete for CTLW . We partition branching temporal logic formulas into three classes: universal, existential, a...

• Type: Conference
• Year: 1999
• Where: CONCUR
• Authors: Orna Kupferman, Moshe Y. Vardi
• Keywords: CONCUR 1999, Distributed And Parallel Computing, Open System, Robust Model Checking, Temporal Logic