Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
From MaRDI portal
Recommendations
Cites work
- A logic for reasoning about time and reliability
- Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes
- Approximate Abstractions of Stochastic Hybrid Systems
- Approximate model checking of stochastic hybrid systems
- Approximating labelled Markov processes
- Approximating Markov Processes by Averaging
- Approximations of Stochastic Hybrid Systems
- Bisimulation for labelled Markov processes
- Bisimulation metrics for continuous Markov decision processes
- Bisimulation through probabilistic testing
- Characterization and computation of infinite-horizon specifications over Markov processes
- Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
- Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system
- Error bounds for rolling horizon policies in discrete-time Markov control processes
- Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
- Foundations of Software Science and Computational Structures
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 1754609 (Why is no real title available?)
- scientific article; zbMATH DE number 1864592 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Hybrid Systems: Computation and Control
- Labelled Markov processes.
- Labelled Markov processes: stronger and faster approximations
- Markov chains and stochastic stability
- Metrics for labelled Markov processes
- Model checking of probabilistic and nondeterministic systems
- On approximation metrics for linear temporal model-checking of stochastic systems
- On finite-state approximants for probabilistic computation tree logic
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Robust PCTL model checking
- Stochastic optimal control. The discrete time case
- Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions
- Taking it to the limit: approximate reasoning for Markov processes
Cited in
(11)- Domain theory, testing and simulation for labelled Markov processes
- Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Probabilistic Marking Estimation in Labeled Petri Nets
- Robust PCTL model checking
- On the relationship between bisimulation and trace equivalence in an approximate probabilistic context
- Hyperfinite Approximations to Labeled Markov Transition Systems
- Characterization and computation of infinite-horizon specifications over Markov processes
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Finite Approximation of LMPs for Exact Verification of Reachability Properties
- A spectrum of approximate probabilistic bisimulations
This page was built for publication: Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5418954)
