Fast Verified SCCs for Probabilistic Model Checking

Arnd Hartmanns, Bram Kohlen, Peter Lammich

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

19 Downloads (Pure)

Abstract

High-performance probabilistic model checkers like the Modest Toolset’s mcsta follow the topological ordering of an MDP’s strongly connected components (SCCs) to speed up the numerical analysis. They use hand-coded and -optimised implementations of SCC-finding algorithms. Verified SCC-finding implementations so far were orders of magnitudes slower than their unverified counterparts. In this paper, we show how to use a refinement approach with the Isabelle theorem prover to formally verify an imperative SCC-finding implementation that can be swapped in for mcsta ’s current unverified one. It uses the same state space representation as mcsta, avoiding costly conversions of the representation. We evaluate the verified implementation’s performance using an extensive benchmark, and show that its use does not significantly influence mcsta ’s overall performance. Our work exemplifies a practical approach to incrementally increase the trustworthiness of existing model checking software by replacing unverified components with verified versions of comparable performance.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part I
EditorsÉtienne André, Jun Sun
PublisherSpringer Nature
Pages181-202
Number of pages22
ISBN (Electronic)978-3-031-45329-8
ISBN (Print)978-3-031-45328-1
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
PublisherSpringer
Volume14215
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

  • 2023 OA procedure

Fingerprint

Dive into the research topics of 'Fast Verified SCCs for Probabilistic Model Checking'. Together they form a unique fingerprint.

Cite this