Verification and control of partially observable probabilistic real-time systems

Gethin Norman, David Parker, Xueyi Zou

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

5 Citations (Scopus)

Abstract

We propose automated techniques for the verification and control of probabilistic real-time 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 dense-time behaviour and a grid-based 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 languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems
Subtitle of host publication13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings
EditorsSriram Sankaranarayanan, Enrico Vicario
PublisherSpringer
Pages240-255
Volume9268
ISBN (Electronic)978-3319229751
ISBN (Print)978-3319229744
DOIs
Publication statusPublished - 22 Aug 2015
Event13th International Conference, FORMATS 2015 - Spain, Madrid September , Spain
Duration: 2 Sept 20154 Sept 2015

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743

Conference

Conference13th International Conference, FORMATS 2015
Country/TerritorySpain
City Madrid September
Period2/09/154/09/15

Fingerprint

Dive into the research topics of 'Verification and control of partially observable probabilistic real-time systems'. Together they form a unique fingerprint.

Cite this