Three-valued abstraction for probabilistic systems
From MaRDI portal
Publication:444484
DOI10.1016/j.jlap.2012.03.007zbMath1277.68219OpenAlexW1998422337WikidataQ57801178 ScholiaQ57801178MaRDI QIDQ444484
Verena Wolf, Joost-Pieter Katoen, Martin Leucker, Daniel Klink
Publication date: 14 August 2012
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2012.03.007
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
A counter abstraction technique for verifying properties of probabilistic swarm systems, On Abstraction of Probabilistic Systems, Combining decomposition and reduction for state space analysis of a self-stabilizing system, Efficient computation of the bounds of continuous time imprecise Markov chains, Abstract model repair for probabilistic systems, Bounding inferences for large-scale continuous-time Markov chains: a new approach based on lumping and imprecise Markov chains, Probabilistic model checking of biological systems with uncertain kinetic rates
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A logic for reasoning about time and reliability
- Interval-valued finite Markov chains
- Deciding bisimilarity and similarity for probabilistic processes.
- Comparative branching-time semantics for Markov chains
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- On finite-state approximants for probabilistic computation tree logic
- Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL
- The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Processes
- A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes
- Abstraction for Stochastic Systems by Erlang’s Method of Stages
- Partial Order Reduction for Markov Decision Processes: A Survey
- Delayed Nondeterminism in Continuous-Time Markov Decision Processes
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
- Sliding Window Abstraction for Infinite Markov Chains
- Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Symbolic model checking for probabilistic processes
- Validation of Stochastic Systems
- Magnifying-Lens Abstraction for Markov Decision Processes
- Model-Checking ω-Regular Properties of Interval Markov Chains
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Model-checking continuous-time Markov chains
- Symmetry Reduction for Probabilistic Model Checking
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Model Checking Software
- Tools and Algorithms for the Construction and Analysis of Systems
