Model checking of probabilistic and nondeterministic systems
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata
- scientific article; zbMATH DE number 1400096 (Why is no real title available?)
- Conditional Probabilities over Probabilistic and Nondeterministic Systems
- Model Checking Quantitative Linear Time Logic
- Multiphase until formulas over Markov reward models: an algebraic approach
- Trade-off analysis meets probabilistic model checking
- Branching bisimulation congruence for probabilistic systems
- Probabilistic model checking for energy-utility analysis
- Model checking stochastic automata
- Foundations of Software Science and Computational Structures
- Constraint-based debugging in probabilistic model checking
- Pardinus: a temporal relational model finder
- Parametric probabilistic transition systems for system design and analysis
- Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
- Combined model checking for temporal, probabilistic, and real-time logics
- Verification and control for probabilistic hybrid automata with finite bisimulations
- Deciding what is good-for-MDPs
- The finite satisfiability problem for PCTL is undecidable
- Towards light-weight probabilistic model checking
- Reachability in recursive Markov decision processes
- A probabilistic model for the interaction of an agent with a network environment
- What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives
- Qualitative Logics and Equivalences for Probabilistic Systems
- Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
- The well-designed logical robot: learning and experience from observations to the Situation Calculus
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- A survey on temporal logics for specifying and verifying real-time systems
- Measuring progress of probabilistic LTL model checking
- The complexity of synchronizing Markov decision processes
- Verifying a class of nondeterministic discrete event systems in a generalized temporal logic
- Probabilistic may/must testing: retaining probabilities by restricted schedulers
- On Abstraction of Probabilistic Systems
- Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
- Model checking failure-prone open systems using probabilistic automata
- Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models
- Symbolic model checking for probabilistic processes
- Metrics for labelled Markov processes
- Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes
- On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems
- Means-end relations and a measure of efficacy
- Stochastic game logic
- A temporal logic for proving properties of topologically general executions
- Quantitative analysis under fairness constraints
- Counterexamples in Probabilistic Model Checking
- Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
- Bisimulations meet PCTL equivalences for probabilistic automata
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
- Model checking probabilistic systems
- Approximating labelled Markov processes
- Group-by-group probabilistic bisimilarities and their logical characterizations
- Model checking mobile stochastic logic
- State explosion in almost-sure probabilistic reachability
- Statistical model checking of stochastic component-based systems
- PMaude: rewrite-based specification language for probabilistic object systems
- Partial order reduction for probabilistic branching time
- Quantitative analysis with the probabilistic model checker PRISM
- Preface to the special issue on probabilistic model checking
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
- Model checking discounted temporal properties
- A Tutorial on Interactive Markov Chains
- Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system
- Validation of Stochastic Systems
- A logic for reasoning about time and reliability
- Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
- Game-Based Probabilistic Predicate Abstraction in PRISM
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Model checking with probabilistic tabled logic programming
- Probabilistic mobile ambients
- Model checking QCTL plus on quantum Markov chains
- The satisfiability problem for a quantitative fragment of PCTL
- Model-Checking ω-Regular Properties of Interval Markov Chains
- Games, Time, and Probability: Graph Models for System Design and Analysis
- Cognitive reasoning and trust in human-robot interactions
- The finite satisfiability problem for PCTL is undecidable
- Performance analysis of probabilistic timed automata using digital clocks
- Measuring and synthesizing systems in probabilistic environments
- Energy-utility analysis for resilient systems using probabilistic model checking
- Automatic verification of concurrent stochastic systems
- Probabilistic verification and approximation
- Deciding probabilistic bisimilarity over infinite-state probabilistic systems
- Automatic verification of real-time systems with discrete probability distributions.
- Temporal logics for the specification of performance and reliability
- Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
- Probabilistic temporal logics via the modal mu-calculus
- CEGAR for compositional analysis of qualitative properties in Markov decision processes
- Quantitative verification and strategy synthesis for stochastic games
- Compositional probabilistic verification through multi-objective model checking
- Separable GPL: decidable model checking with more non-determinism
- Model checking linear-time properties of probabilistic systems
- Distribution, approximation and probabilistic model checking
- On probabilistic timed automata.
- On-the-fly model checking for extended action-based probabilistic operators
- On the verification of qualitative properties of probabilistic processes under fairness constraints.
- Formal modelling and verification of probabilistic resource bounded agents
- Quantitative solution of omega-regular games
- Quantifying opacity
- Euclidean model checking: a scalable method for verifying quantitative properties in probabilistic systems
- On the use of MTBDDs for performability analysis and verification of stochastic systems.
- Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
This page was built for publication: Model checking of probabilistic and nondeterministic systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2956706)