Projects per year
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.
Original language  English 

Title of host publication  Formal Modeling and Analysis of Timed Systems 
Subtitle of host publication  13th International Conference, FORMATS 2015, Madrid, Spain, September 24, 2015, Proceedings 
Editors  Sriram Sankaranarayanan, Enrico Vicario 
Publisher  Springer 
Pages  240255 
Volume  9268 
ISBN (Electronic)  9783319229751 
ISBN (Print)  9783319229744 
DOIs  
Publication status  Published  22 Aug 2015 
Event  13th International Conference, FORMATS 2015  Spain, Madrid September , Spain Duration: 2 Sept 2015 → 4 Sept 2015 
Publication series
Name  Lecture Notes in Computer Science 

ISSN (Print)  03029743 
Conference
Conference  13th International Conference, FORMATS 2015 

Country/Territory  Spain 
City  Madrid September 
Period  2/09/15 → 4/09/15 
Fingerprint
Dive into the research topics of 'Verification and control of partially observable probabilistic realtime systems'. Together they form a unique fingerprint.Projects
 1 Finished

Automated GameTheoretic Verification of Security Systems
Engineering & Physical Science Research Council
4/11/13 → 31/10/14
Project: Research Councils