U-check: Model Checking and Parameter Synthesis under Uncertainty

Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Novel applications of formal modelling such as systems biology have highlighted the need to extend formal analysis techniques to domains with pervasive parametric uncertainty. Consequently, machine learning methods for parameter synthesis and uncertainty quantification are playing an increasingly significant role in quantitative formal modelling. In this paper, we introduce a toolbox for parameter synthesis and model checking in uncertain systems based on Gaussian Process emulation and optimisation. The toolbox implements in a user friendly way the techniques described in a series of recent papers at QEST and other primary venues, and it interfaces easily with widely used modelling languages such as PRISM and Bio-PEPA. We describe in detail the architecture and use of the software, demonstrating its application on a case study.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication12th International Conference, QEST 2015, Madrid, Spain, September 1-3, 2015, Proceedings
PublisherSpringer International Publishing
Number of pages16
ISBN (Electronic)978-3-319-22264-6
ISBN (Print)978-3-319-22263-9
Publication statusPublished - 2015

Publication series

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


Dive into the research topics of 'U-check: Model Checking and Parameter Synthesis under Uncertainty'. Together they form a unique fingerprint.

Cite this