
PRISM
 Referenced in 442 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 36 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 28 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 71 articles
[sw04129]
 verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward...

PVeStA
 Referenced in 18 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 17 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 25 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...

PRISMgames
 Referenced in 20 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...

probblackreach
 Referenced in 2 articles
[sw34625]
 probblackreach: Probabilistic blackbox reachability checking (extended version). Model checking has a long ... combination of testing, model inference and model checking. The technique requires systems to be fully ... checking technique for stochastic systems that allows both, nondeterministic and probabilistic behaviour ... involves model inference, testing and probabilistic modelchecking. Here, we consider reachability checking...

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

gbs
 Referenced in 25 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...

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

Antichains
 Referenced in 33 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...