Quantitative/Probabilistic Modelling, Verification and Synthesis
Professor Marta Kwiatkowska is happy to supervise projects in the area of quantitative/probabilistic modelling, verification and synthesis, particularly those relating to the PRISM model checker. PRISM is an open source formal verification tool for analysis of probabilistic systems. PRISM has an extensive website which includes software for download, tutorial, manual, publications and many case studies. Students' own proposals in the broad area of theory, algorithms and implementation techniques for software verification/synthesis will also be considered.
Below are some concrete project proposals:
- Modelling trust in human-robot interaction. When human users interact with autonomous robots, appropriate notions of computational trust are needed to ensure that their interactions are safe and effective: too little trust can lead to user disengagement, and too much trust may cause damage. Trust management systems have been introduced for autonomous agents on the Internet, but need to be adapted to the setting of mobile robots, taking into account intermittent connectivity and uncertainty on sensor readings. Recently, a logic and model checking algorithm were formulated for reasoning about trust (http://qav.comlab.ox.ac.uk/bibitem.php?key=HK170, see also https://www.hayfestival.com/p-12297-marta-kwiatkowska.aspx?skinid=16. This project aims to develop an implementation of a simplified model checking algorithm. The project will suit a student interested in theory and/or software implementation.
- Autonomous urban driving. This project is concerned with synthesising strategies for autonomous driving directly from requirements expressed in temporal logic, so that they are correct by construction. Probability is used to quantify information about hazards, such as accidents hotspots. Inspired by the DARPA Urban Challenge, a method for synthesising strategies (controllers) from multi-objective requirements was developed and validated on map data for villages in Oxfordshire ( http://www.prismmodelchecker.org/bibitem.php?key=CKSW13 ). The idea is to develop the techniques further, to allow high-level navigation based on waypoints, and to develop strategies for avoiding threats, such as road blockage, at runtime. In the longer term, the goal is to validate the methods on realistic scenarios in collaboration with the Mobile Robotics Group. The project will suit a student interested in theory or software implementation. For more information about the project see http://www.veriware.org/autonomous.php
- Controller synthesis for robot coordination. Autonomous robots have numerous applications in scenarios such as warehouse management, planetary exploration, or search and rescue. In view of environmental uncertainty, such scenarios are modelled using Markov decision processes. The goals (e.g. the goods should be delivered to location A while avoiding the hazardous location B) can be conveniently specified using temporal logic, from which correct-by-construction controllers (strategies) can be generated. This project aims to develop a PRISM model of a system of robots for a particular scenario so that safety and effectiveness of their cooperation is guaranteed. Techniques based on machine learning, and specifically real-time dynamic programming ( http://www.prismmodelchecker.org/papers/atva14.pdf ), will be utilised to generate controllers directly from temporal logic goals. This project will suit a student interested in machine learning and software implementation.
- Modelling and verification of DNA programs. DNA molecules can be used to perform complex logical computation. DNA computation differs from conventional digital computation and is sometimes referred to as ‘computing with soup’http://www.economist.com/node/21548488 . Correct design of DNA devices is error-prone and the task is supported by tools such as the DNA Strand Displacement (DSD) programming language and simulator (http://research.microsoft.com/en-us/projects/dna/default.aspx) developed at Microsoft. The DSD tool enables the probabilistic model checking of DNA circuits and has been used to identify a flaw in a DNA transducer gate (see http://qav.comlab.ox.ac.uk/bibitem.php?key=LPC+12). The aim of this project is to model and analyse DNA implementation of logic inference proposed in “Autonomous Resolution Based on DNA Strand Displacement”, DNA Computing and Molecular Programming, LNCS 6937, 2011. The project will suit a student interested in modelling DNA programs using DSD and/or PRISM. For more information about the DNA computing project see http://www.veriware.org/dna.php.
A Molecular Recorder (with Luca Cardelli). Recent technological developments allow massive parallel reading (sequencing) and writing (synthesis) of heterogeneous pools of DNA strands. We are no longer limited to simple circuits built out of a small number of different strands, nor to reading out a few bits of output by fluorescence. While these