Scenario Approach for Parametric Markov Models

Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue*, Lijun Zhang

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Downloads (Pure)

Abstract

In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability and the reward values of the parametric model, we exploit the scenario approach to synthesize a relatively simple polynomial approximation. The approximation is probably approximately correct (PAC), meaning that with high confidence, the approximating function is close to the actual function with an allowable error. With the PAC approximations, one can check properties of the parametric Markov models. We show that the scenario approach can also be used to check PRCTL properties directly – without synthesizing the polynomial at first hand. We have implemented our algorithm in a prototype tool and conducted thorough experiments. The experimental results demonstrate that our tool is able to compute polynomials for more benchmarks than state-of-the-art tools such as PRISM and Storm, confirming the efficacy of our PAC-based synthesis.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
EditorsÉtienne André, Jun Sun
PublisherSpringer
Pages158-180
Number of pages23
ISBN (Print)9783031453281
DOIs
Publication statusPublished - 22 Oct 2023
Event21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore
Duration: 24 Oct 202327 Oct 2023
Conference number: 21

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14215 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Abbreviated titleATVA 2023
Country/TerritorySingapore
CitySingapore
Period24/10/2327/10/23

Keywords

  • 2024 OA procedure

Fingerprint

Dive into the research topics of 'Scenario Approach for Parametric Markov Models'. Together they form a unique fingerprint.

Cite this