MRMC
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Approximate model checking of stochastic hybrid systems
- Three-valued abstraction for probabilistic systems
- Multiphase until formulas over Markov reward models: an algebraic approach
- Efficient CSL model checking using stratification
- Probabilistic model checking for energy-utility analysis
- Minimal counterexamples for linear-time probabilistic verification
- A framework for verification of software with time and probabilities
- Efficient approximation of optimal control for continuous-time Markov games
- Smoothed model checking for uncertain continuous-time Markov chains
- Lumpability for uncertain continuous-time Markov chains
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
- LTL model checking of time-inhomogeneous Markov chains
- Formal methods for biochemical signalling pathways
- Cost preserving bisimulations for probabilistic automata
- Towards light-weight probabilistic model checking
- Three-Valued Abstraction for Continuous-Time Markov Chains
- Observing continuous-time MDPs by 1-clock timed automata
- Abstraction of Probabilistic Systems
- Computing cumulative rewards using fast adaptive uniformization
- Formal dependability modeling and analysis: a survey
- Quantitative abstractions for collective adaptive systems
- Decidability of approximate Skolem problem and applications to logical verification of dynamical properties of Markov chains
- PRINSYS
- Automata-based CSL model checking
- Counterexample generation for discrete-time Markov models: an introductory survey
- CSL model checking algorithms for QBDs
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Mean-field limits beyond ordinary differential equations
- Mixing logics and rewards for the component-oriented specification of performance measures
- Model checking mobile stochastic logic
- Hierarchical counterexamples for discrete-time Markov chains
- A Tutorial on Interactive Markov Chains
- Performance model checking scenario-aware dataflow
- Formalisms for specifying Markovian population models
- Distributed synthesis in continuous time
- Formal system verification. State-of the-art and future trends
- Energy-utility analysis for resilient systems using probabilistic model checking
- Solving systems of bilinear equations for transition rate reconstruction
- Galileo
- GreatSPN
- SIGREF
- PRISM
- Bio-PEPA
- JTorX
- GreatSPN 1.7
- BISIMULATOR
- M-TREE
- LiQuor
- SMART_
- ProbDiVinE
- PASS
- CEGAR
- CADP
- COMICS
- REACH
- SPNP
- ULM
- DiPro
- PARAM
- Casaal
- Ymer
- Pinapa
- MoMo
- SCOOT
- TVT
- ArgoUML
- PEPA
- STOCKS
- DIFtree
- MARCIE
- MC2
- SABRE
- HASL
- Rapture
- Concurrency Workbench
- StochDynTools
- ADABU
- Storm
- CARMA
- Figaro
- Mec 5
- DCVALID
- PALOMA
- INFAMY
- VERSA
- Aligator.jl
- JScience
- Markov Models
- mCRL
- PLASMA-lab
- PROPhESY
- iscasMc
- AMT
- ASDeX
- POWER-TRUCTOR
- A progress measure for explicit-state probabilistic model-checkers
- Performability assessment by model checking of Markov reward models
- Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions
- Model Based Importance Analysis for Minimal Cut Sets
This page was built for software: MRMC