Advances in Symbolic Probabilistic Model Checking with PRISM

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Abstract

For modeling and reasoning about complex systems, symbolic methods provide a prominent way to tackle the state explosion problem. It is well known that for symbolic approaches based on binary decision diagrams (BDD), the ordering of BDD variables plays a crucial role for compact representations and efficient computations. We have extended the popular probabilistic model checker PRISM with support for automatic variable reordering in its multi-terminal-BDD-based engines and report on benchmark results. Our extensions additionally allow the user to manually control the variable ordering at a finer-grained level. Furthermore, we present our implementation of the symbolic computation of quantiles and support for multi-reward-bounded properties, automata specifications and accepting end component computations for Streett conditions.

Details

OriginalspracheEnglisch
TitelTools and Algorithms for the Construction and Analysis of Systems
Redakteure/-innenMarsha Chechik, Jean-François Raskin
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten349-366
Seitenumfang18
ISBN (Print)978-3-662-49673-2
PublikationsstatusVeröffentlicht - 2016
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 9636
ISSN0302-9743

Konferenz

Titel22nd International Conference of Tools and Algorithms for the Construction and Analysis of Systems
KurztitelTACAS 2016
Veranstaltungsnummer
Dauer2 - 8 April 2016
BekanntheitsgradInternationale Veranstaltung
Ort
StadtEindhoven
LandNiederlande

Externe IDs

Scopus 84964037871
ORCID /0000-0002-5321-9343/work/142236726
ORCID /0000-0003-1724-2586/work/165453594

Schlagworte

Schlagwörter

  • Advances in Symbolic Probabilistic Model Checking with PRISM

Bibliotheksschlagworte