[NPZ15]
Gethin Norman, David Parker and Xueyi Zou.
Verification and Control of Partially Observable Probabilistic RealTime Systems.
In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of LNCS, pages 240255, Springer.
September 2015.
[pdf]
[bib]
[Develops techniques for verification and controller synthesis on a partially observable variant of probabilistic timed automata, implemented in an extension of PRISM.]

Notes:
An extended version of this paper, with proofs, is available at http://arxiv.org/abs/1506.06419.
Accompanying files and source code can be found here.
The original publication is available at www.springerlink.com.

Abstract.
We propose automated techniques for the verification and control of
probabilistic realtime systems that are only partially observable.
To formally model such systems, we define an extension of probabilistic timed automata
in which local states are partially visible to an observer or controller.
We give a probabilistic temporal logic that can express a range of quantitative properties of these models,
relating to the probability of an event's occurrence or the expected value of a reward measure.
We then propose techniques to either verify that such a property holds
or to synthesise a controller for the model which makes it true.
Our approach is based on an integer discretisation of the model's densetime behaviour
and a gridbased abstraction of the uncountable belief space induced by partial observability.
The latter is necessarily approximate since the underlying problem is undecidable,
however we show how both lower and upper bounds on numerical results can be generated.
We illustrate the effectiveness of the approach by implementing it in the PRISM model checker
and applying it to several case studies, from the domains of computer security and task scheduling.
