The Verification of Probabilistic Systems Under Memoryless Partial-Information Policies is Hard
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
Several models of probabilistic systems comprise both probabilistic and nondeterministic choice. In such models, the resolution of nondeterministic choices is mediated by the concept of policies sometimes called adversaries. A policy is a criterion for choosing among nondeterministic alternatives on the basis of the past sequence of states of the system. By fixing the resolution of nondeterministic choice, a policy reduces the system to an ordinary stochastic system, thus making it possible to reason about the probability of events of interest. A partial information policy is a policy that can observe only a portion of the system state, and that must base its choices on finite sequences of such partial observations. We argue that in order to obtain accurate estimates of the worst-case performance of a probabilistic system, it would often be desirable to consider partial-information policies. However, we show that even when considering memoryless partial-information policies, the problem of deciding whether the system can stay forever with positive probability in a given subset of states becomes NP-complete. As a consequence, many verification problems that can be solved in polynomial time under perfect-information policies, such as the model-checking of pCTL or the computation of the worst-case long-run average outcome of tasks, become NP-hard under memoryless partial-information policies. On the positive side, we show that the worst-case long-run average outcome of tasks under memoryless partial-information policies can be computed by solving a nonlinear programming problem, opening the way to the use of numerical approximation algorithms.
- Statistics and Probability