PASS

PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. Models are specified in a variant of the PRISM language. PASS computes the probability of reaching a set of goal states specified by the user. PASS has two sisters, PARAM and INFAMY, that accept virtually the same language, but have different strengths.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 8 articles )

Showing results 1 to 8 of 8.
Sorted by year (citations)

  1. Křetínský, Jan; Meggendorfer, Tobias: Of cores: a partial-exploration framework for Markov decision processes (2020)
  2. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  3. Wang, Shuling; Zhan, Naijun; Zhang, Lijun: A compositional modelling and verification framework for stochastic hybrid systems (2017)
  4. Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: On abstraction of probabilistic systems (2014)
  5. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  6. Barbuti, Roberto; Levi, Francesca; Milazzo, Paolo; Scatena, Guido: Probabilistic model checking of biological systems with uncertain kinetic rates (2012)
  7. Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn; Zhang, Lijun: PASS: abstraction refinement for infinite probabilistic models (2010) ioport
  8. Kattenbelt, Mark; Kwiatkowska, Marta; Norman, Gethin; Parker, David: A game-based abstraction-refinement framework for Markov decision processes (2010)


Further publications can be found at: http://depend.cs.uni-sb.de/tools/pass/publications/