The Verification of Probabilistic Systems Under Memoryless Partial-Information Policies is Hard
Luca de Alfaro · Defense Technical Information Center (DTIC) · 1999
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.