• PRISM

  • Referenced in 376 articles [sw01186]
  • probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, Markov decision processes ... performed through model checking such systems against specifications written in the probabilistic temporal logics PCTL ... tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs ... PRISM has been successfully used to analyse probabilistic termination, performance, and quality of service properties...
  • PAT

  • Referenced in 29 articles [sw13258]
  • simulator. Most importantly, PAT implements various model checking techniques catering for different properties such ... with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization...
  • APMC

  • Referenced in 25 articles [sw11483]
  • Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification ... probabilistic systems. However, the representation of the transition matrix may be expensive for very large ... induce a prohibitive cost for the model checking algorithm. In this paper, we propose ... satisfied with high confidence by a probabilistic system. Our randomized algorithm requires only a succinct...
  • MRMC

  • Referenced in 66 articles [sw04129]
  • verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward...
  • PVeStA

  • Referenced in 15 articles [sw08423]
  • tool. Statistical model checking is an attractive formal analysis method for probabilistic systems such ... probabilistic in nature. This paper is about drastically increasing the scalability of statistical model checking ... tool [10]. PVeStA supports statistical model checking of probabilistic real-time systems specified as either ... probabilistic rewrite theories in Maude. Furthermore, the properties that it can model check...
  • Ymer

  • Referenced in 14 articles [sw09468]
  • probabilistic transient properties of stochastic discrete event systems. Ymer implements both statistical and numerical model ... checking techniques. We focus on two features of Ymer ... distributed acceptance sampling and statistical model checking of nested probabilistic statements...
  • VESTA

  • Referenced in 22 articles [sw08425]
  • statistical analysis of probabilistic systems. It supports statistical model-checking [6, 7] and statistical evaluation ... model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check ... property specified in probabilistic computation tree logic (PCTL) [3] or continuous stochastic logic ... satisfied by a stochastic model. Furthermore, VESTA supports the statistical computation of expected values...
  • DiPro

  • Referenced in 4 articles [sw09744]
  • Generation. The computation of counterexamples for probabilistic model checking has been an area of active ... allows for the computation and representation of probabilistic counterexamples. We present an open source tool ... used with the PRISM and MRMC probabilistic model checkers. It allows for the computation...
  • Markov Models

  • Referenced in 4 articles [sw28576]
  • application of these models we formalize probabilistic model checking of pCTL formulas, analysis of IPv4...
  • LiQuor

  • Referenced in 18 articles [sw04136]
  • Probmela programs, which are terms of a probabilistic guarded command language with an operational semantics ... properties by means of automata-based model checking algorithms...
  • ExplicitPRISMSymm

  • Referenced in 2 articles [sw13369]
  • technique for explicit models in PRISM. Probabilistic model checking of concurrent system involves exhaustive search ... probabilistic models, which are easy to build and perform reasonably well at property checking ... represented probabilistic models. We report that explicitly represented models perform well at property checking...
  • GPU-PRISM

  • Referenced in 2 articles [sw19543]
  • based on parallel algorithms for probabilistic model checking which are tuned for GPUs. In particular...
  • ProMoca

  • Referenced in 1 article [sw18548]
  • temporal logic. Thirdly, we adapt a probabilistic model checking algorithm to automatically analyze compliance...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • probabilistic analysis of complex systems. Smart can combine different formalisms in the same modeling study ... techniques, as well as symbolic CTL model-checking algorithms, are available. For the study...
  • INFAMY

  • Referenced in 5 articles [sw21177]
  • INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties...
  • PSMaude

  • Referenced in 3 articles [sw10125]
  • features. To allow their probabilistic simulation and statistical model checking by means of pseudo-random ... this paper, we propose an expressive probabilistic strategy language that allows the user to define ... probabilistic rewrite theories. We have implemented PSMaude, a tool that extends Maude with a probabilistic ... simulator and a statistical model checker for our language. We illustrate the convenience of being...
  • PRISM-games

  • Referenced in 11 articles [sw12934]
  • tool is based on the probabilistic model checker PRISM, benefiting from its existing user interface ... simulator, whilst adding novel model checking algorithms for stochastic games, as well as functionality...
  • gbs

  • Referenced in 17 articles [sw06078]
  • analyze data from GBS models. This package contains probabilistic and reliability indicators and random number ... package in order to check the suitability of the GBS models. In this article...
  • conPAS

  • Referenced in 1 article [sw10953]
  • from Buchi games and qualitative probabilistic LTL model checking, it generates a control strategy...
  • Antichains

  • Referenced in 24 articles [sw20208]
  • propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata ... algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show ... that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard...