
PRISM
 Referenced in 376 articles
[sw01186]
 probabilistic systems. PRISM supports three probabilistic models: discretetime 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 realtime 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 modelchecking [6, 7] and statistical evaluation ... modelchecking VESTA uses a sequence of interrelated statistical hypothesis testing to check ... property speciﬁed in probabilistic computation tree logic (PCTL) [3] or continuous stochastic logic ... satisﬁed 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 automatabased 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...

GPUPRISM
 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 modelchecking algorithms, are available. For the study...

INFAMY
 Referenced in 5 articles
[sw21177]
 INFAMY, a model checker for arbitrarily structured infinitestate 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 pseudorandom ... 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...

PRISMgames
 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...