Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games

Tobias Meggendorfer, Maximilian Weininger

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

Abstract

We present version 2.0 of the Partial Exploration Tool (Pet), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, Pet2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that Pet2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.

Original languageEnglish
Title of host publicationComputer Aided Verification - 36th International Conference, CAV 2024, Proceedings
EditorsArie Gurfinkel, Vijay Ganesh
PublisherSpringer Science and Business Media Deutschland GmbH
Pages359-372
Number of pages14
ISBN (Print)9783031656323
DOIs
StatePublished - 2024
Externally publishedYes
Event36th International Conference on Computer Aided Verification, CAV 2024 - Montreal, Canada
Duration: 24 Jul 202427 Jul 2024

Publication series

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

Conference

Conference36th International Conference on Computer Aided Verification, CAV 2024
Country/TerritoryCanada
CityMontreal
Period24/07/2427/07/24

Keywords

  • Model checker
  • Partial exploration
  • Probabilistic verification
  • Stochastic games

Fingerprint

Dive into the research topics of 'Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games'. Together they form a unique fingerprint.

Cite this