Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10332698 | Journal of Computer and System Sciences | 2016 | 34 Pages |
Abstract
We consider partially observable Markov decision processes (POMDPs) with Ï-regular conditions specified as parity objectives. The class of Ï-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Krishnendu Chatterjee, Martin ChmelÃk, Mathieu Tracol,