PRINCESS (Probabilistic Representation of Intent Commitments to Ensure Software Survival)
is a project under the DARPA BRASS (Building Resource Adaptive Software Systems) program. It is led by
Charles River Analytics
and involves partners from the university of Birmingham, Harvard University and the University of Southern California.
The overall aim of the project is to develop adaptive software systems for operation in dynamic and uncertain environments, underpinned by rigorous formal verification methods which ensure the correctness of the adaptation process. The work will involve developing techniques that combine verification with probabilistic modelling and inference, with a particular preference for the use of probabilistic programming languages.
Christel Baier, Joachim Klein, Linda Leuschner, David Parker and Sascha Wunderlich.
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes.
In Proc. 28th International Conference on Computer Aided Verification (CAV'17). To appear.
[Proposes "interval iteration" techniques for deriving more accurate bounds on the results of probabilistic model checking, and implements them in PRISM.]
Bruno Lacerda, David Parker and Nick Hawes.
Multi-objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees.
In Proc. 27th International Conference on Automated Planning and Scheduling (ICAPS'17), AAAI Press. To appear.
[Proposes techniques for generating mobile robot controllers with probabilistic time-bounded guarantees using multi-objective probabilistic model checking and an extension of PRISM.]
Gethin Norman, David Parker and Xueyi Zou.
Verification and Control of Partially Observable Probabilistic Systems.
Real-Time Systems, 53(3), pages 354-402, Springer.
[Presents techniques and a tool for verification and strategy synthesis in partially observable probabilistic models with both discrete and dense models of time.]
Marta Kwiatkowska, Gethin Norman and David Parker.
Probabilistic Model Checking: Advances and Applications.
In R. Drechsler (editor), Formal System Verification, Springer. To appear.
[Provides an introduction to probabilistic model checking, including coverage of some recent advances in the field and a wide variety of examples and applications.]