PRINCESS

Overview

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.

Participants (at Birmingham):

Publications

14 publications:
  • [EP21] Alexandros Evangelidis and David Parker. Quantitative Verification of Kalman Filters. Formal Aspects of Computing, 33(4-5), pages 669-693, Springer. February 2021. [pdf] [bib] [Builds a framework for quantitative verification of Kalman filters on top of PRISM. ]
  • [LFPH19] Bruno Lacerda, Fatma Faruq, David Parker and Nick Hawes. Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots. International Journal of Robotics Research, 38(9), pages 1098–1123. 2019. [pdf] [bib] [Presents a framework for mobile service robot with formal performance guarantees, with an implementation built on PRISM.]
  • [KNP19] Marta Kwiatkowska, Gethin Norman and David Parker. Verification and Control of Turn-Based Probabilistic Real-Time Games. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday), volume 11760 of LNCS, pages 379-396, Springer. November 2019. [pdf] [bib] [Proposes techniques for verifying probabilistic real-time games building on methods implemented in PRISM-games.]
  • [EP19] Alexandros Evangelidis and David Parker. Quantitative Verification of Numerical Stability for Kalman Filters. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 425-441, Springer. October 2019. [pdf] [bib] [Builds a framework for verifying Kalman filters on top of PRISM.]
  • [KNPS19] Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games. In Proc. 23rd International Symposium on Formal Methods (FM'19), volume 11800 of LNCS, pages 298-315, Springer. October 2019. [pdf] [bib] [Develops verification methods for stochastic games using Nash equilibria, implemented in PRISM-games.]
  • [NP19] Chris Novakovic and David Parker. Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems. In Proc. 24th European Symposium on Research in Computer Security (ESORICS'19), volume 11735 of LNCS, pages 319-337, Springer. September 2019. [pdf] [bib] [Develops techniques to identify side-channel attacks in probabilistic systems, building on PRISM-pomdps.]
  • [PFF+19] Avi Pfeffer, Curt Wu, Gerald Fry, Kenny Lu, Steve Marotta, Mike Reposa, Yuan Shi, T. K. Satish Kumar, Craig A. Knoblock, David Parker, Irfan Muhammad and Chris Novakovic. Software Adaptation for an Unmanned Undersea Vehicle. IEEE Software, 36(2), pages 91-96, IEEE. March 2019. [pdf] [bib] [Summarises the PRINCESS project, which develops methods for adapting an optimising software at runtime, including mission verification using extensions of PRISM.]
  • [FLHP18] Fatma Faruq, Bruno Lacerda, Nick Hawes and David Parker. Simultaneous Task Allocation and Planning Under Uncertainty. In Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'18), IEEE. October 2018. [pdf] [bib] [Proposes techniques for verified multi-robot task allocation and planning, implemented as an extension of PRISM.]
  • [EPB18] Alexandros Evangelidis, David Parker and Rami Bahsoon. Performance Modelling and Verification of Cloud-based Auto-Scaling Policies. Future Generation Computer Systems, 87, pages 629-638, Elsevier. October 2018. [pdf] [bib] [Presents an approach for producing formal performance guarantees for cloud-based auto-scaling policies using PRISM.]
  • [KNP17b] Marta Kwiatkowska, Gethin Norman and David Parker. Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In Models, Algorithms, Logics and Tools, volume 10460 of LNCS, pages 289-309, Springer. August 2017. [pdf] [bib] [Proposes novel symbolic techniques for verifi cation and optimal strategy synthesis for priced probabilistic timed automata ]
  • [BKLPW17] 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), volume 10426 of LNCS, pages 160-180, Springer. July 2017. [pdf] [bib] [Proposes "interval iteration" techniques for deriving more accurate bounds on the results of probabilistic model checking, and implements them in PRISM.]
  • [KNP17] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking: Advances and Applications. In R. Drechsler (editor), Formal System Verification, pages 73-121, Springer. June 2017. [pdf] [bib] [Provides an introduction to probabilistic model checking, including coverage of some recent advances in the field and a wide variety of examples and applications.]
  • [LPH17] 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), pages 504-512, AAAI Press. June 2017. [pdf] [bib] [Proposes techniques for generating mobile robot controllers with probabilistic time-bounded guarantees using multi-objective probabilistic model checking and an extension of PRISM.]
  • [NPZ17] Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, 53(3), pages 354-402, Springer. April 2017. [pdf] [bib] [Presents techniques and a tool for verification and strategy synthesis in partially observable probabilistic models with both discrete and dense models of time.]