The Verification of Probabilistic Systems Under Memoryless Partial-Information Policies is Hard
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1999
- Accession Number
- ADA461516
Entities
People
- Luca De Alfaro
Organizations
- University of California, Berkeley