PRISM: Probabilistic symbolic model checker
From MaRDI portal
Recommendations
Cited in
(82)- An elementary proof that Herman's ring is \(\Theta (N^{2})\)
- PRISM
- On the use of MTBDDs for performability analysis and verification of stochastic systems.
- Models of transcription factor binding: sensitivity of activation functions to model assumptions
- Performance limits and trade-offs in entropy-driven biochemical computers
- Modeling fimbriae mediated parasite-host interactions
- Model checking and abstraction to the aid of parameterized systems (a survey)
- Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions
- Reconciling real and stochastic time: the need for probabilistic refinement
- Enhancing probabilistic model checking with ontologies
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Modular verification of protocol equivalence in the presence of randomness
- \textsf{PrIC3}: property directed reachability for MDPs
- Preface to the special issue on probabilistic model checking
- Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
- Natural strategic ability
- Symbolic model checking for probabilistic timed automata
- Limited by sensing -- a minimal stochastic model of the lag-phase during diauxic growth
- Model checking expected time and expected reward formulae with random time bounds
- Optimal cost almost-sure reachability in POMDPs
- Probabilistic guarded commands mechanized in HOL
- What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives
- Nearly optimal verifiable data streaming
- Deciding probabilistic automata weak bisimulation: theory and practice
- Weak probabilistic anonymity
- Simulation of generalised semi-Markov processes based on graph transformation systems
- PEPA queues: capturing customer behaviour in queueing networks
- Exogenous probabilistic computation tree logic
- A Tutorial on Interactive Markov Chains
- ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM
- Comparative analysis of statistical model checking tools
- Verification of context-dependent channel-based service models
- Evaluating a probabilistic model checker for modeling and analyzing retrial queueing systems
- Command-based importance sampling for statistical model checking
- Binary decision diagrams
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- Maximizing the conditional expected reward for reaching the goal
- Fast debugging of PRISM models
- Temporalization of Probabilistic Propositional Logic
- Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus
- Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
- Quantitative analysis under fairness constraints
- Space-efficient scheduling of stochastically generated tasks
- Probabilistic symbolic model checking with PRISM: A hybrid approach
- Modeling tripartite entanglement in quantum protocols using evolving entangled hypergraphs
- Probabilistic model checking of the PDGF signaling pathway
- Multi-valued verification of strategic ability
- A probabilistic higher-order fixpoint logic
- Scenario-based verification of uncertain MDPs
- A GPGPU-based simulator for Prism: statistical verification of results of PMC
- The big-O problem
- The theory of traces for systems with nondeterminism, probability, and termination
- Of cores: a partial-exploration framework for Markov decision processes
- Evaluating complex MAC protocols for sensor networks with APMC
- Probabilistic model checking on HPC systems for the performance analysis of mobile networks
- Probabilistic approximations of ODEs based bio-pathway dynamics
- Lazy probabilistic model checking without determinisation
- Model Checking-Based Genetic Programming with an Application to Mutual Exclusion
- Measuring the confinement of probabilistic systems
- Of cores: a partial-exploration framework for Markov decision processes
- Formal modelling and verification of probabilistic resource bounded agents
- SySCoRe: Synthesis via Stochastic Coupling Relations
- Wordgen : a Timed word Generation Tool
- PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
- A probabilistic extension of UML-B
- A probabilistic logic for verifying continuous-time Markov chains
- Ontology-mediated probabilistic model checking
- A possible worlds semantics for trustworthy non-deterministic computations
- Making model checking feasible for GOAL
- Safe autonomy under perception uncertainty using chance-constrained temporal logic
- Model-based testing of probabilistic systems
- SySCcoRe 2.0: toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications
- Checking trustworthiness of probabilistic computations in a typed natural deduction system
- Using fixed memory blocks in GPUs to accelerate SpMV multiplication in probabilistic model checkers
- PAC statistical model checking of mean payoff in discrete- and continuous-time MDP
- Cancellative convex semilattices
- Probabilistic model checking of biological systems with uncertain kinetic rates
- Formal techniques for performance analysis: blending SAN and PEPA
- Formal probabilistic analysis of detection properties in wireless sensor networks
- Using probabilistic Kleene algebra pKA for protocol verification
- Analysing distributed internet worm attacks using continuous state-space approximation of process algebra models
- Mixing logics and rewards for the component-oriented specification of performance measures
This page was built for publication: PRISM: Probabilistic symbolic model checker
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4738778)
