Symbolic Model Checking of Weighted PCTL Using Dependency Graphs

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)

Abstract

We present a global and local algorithm for model checking a weighted variant of PCTL with upper-bound weight constraints, on probabilistic weighted Kripke structures where the weights are vectors with non-zero magnitude. Both algorithms under- and over approximate a fixed-point over a symbolic dependency graph, until sufficient evidence to prove or disprove the given formula is found. Fixed-point computations are carried out in the domain of (multidimensional) probabilistic step functions, encoded as interval decision diagrams. The global algorithm works similarly to classic value iteration for PCTL in that it evaluates all nodes of the dependency graph iteratively, while the local algorithm performs a search-like evaluation of the given dependency graph in an attempt to find enough evidence locally to prove/disprove a given formula, without having to evaluate all nodes. Both algorithms are evaluated on several experiments and we show that the local algorithm generally outperforms the global algorithm.
Original languageEnglish
Title of host publicationNASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings
EditorsKristin Yvonne Rozier, Julia M. Badger
Number of pages18
PublisherSpringer
Publication date2019
Pages298-315
ISBN (Print)978-3-030-20651-2
ISBN (Electronic)978-3-030-20652-9
DOIs
Publication statusPublished - 2019
EventNFM19: 11th Annual NASA Formal Methods Symposium: Challenges for Future Exploration - Rice University, Houston, United States
Duration: 7 May 20199 May 2019
Conference number: 11
https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html

Conference

ConferenceNFM19: 11th Annual NASA Formal Methods Symposium
Number11
LocationRice University
CountryUnited States
CityHouston
Period07/05/201909/05/2019
Internet address
SeriesLecture Notes in Computer Science
Volume11460
ISSN0302-9743

Keywords

  • Model Checking
  • Dependency graph
  • probabilistic CTL
  • On-the-fly methods

Fingerprint Dive into the research topics of 'Symbolic Model Checking of Weighted PCTL Using Dependency Graphs'. Together they form a unique fingerprint.

Cite this