Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations

DOI10.1007/978-3-319-06880-0_2zbMath1407.68275OpenAlexW660320WikidataQ112268311 ScholiaQ112268311MaRDI QIDQ5418954

No author found.

Publication date: 2 June 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-06880-0_2

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (4)

Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement ⋮ On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context ⋮ Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Characterization and computation of infinite-horizon specifications over Markov processes
• Metrics for labelled Markov processes
• Approximate model checking of stochastic hybrid systems
• Markov chains and stochastic stability
• Stochastic optimal control. The discrete time case
• Bisimulation through probabilistic testing
• A logic for reasoning about time and reliability
• Approximating labelled Markov processes
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Bisimulation for labelled Markov processes
• On finite-state approximants for probabilistic computation tree logic
• Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes
• Taking It to the Limit: Approximate Reasoning for Markov Processes
• Model checking of probabilistic and nondeterministic systems
• Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions
• Robust PCTL model checking
• Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
• On approximation metrics for linear temporal model-checking of stochastic systems
• Bisimulation Metrics for Continuous Markov Decision Processes
• Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system
• Approximations of Stochastic Hybrid Systems
• Error bounds for rolling horizon policies in discrete-time Markov control processes
• Hybrid Systems: Computation and Control
• Approximate Abstractions of Stochastic Hybrid Systems
• Foundations of Software Science and Computational Structures
• Approximating Markov Processes by Averaging

This page was built for publication: Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations