Model checking of probabilistic and nondeterministic systems
From MaRDI portal
Publication:2956706
DOI10.1007/3-540-60692-0_70zbMath1354.68167OpenAlexW4377077122MaRDI QIDQ2956706
Publication date: 19 January 2017
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-60692-0_70
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items
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 ⋮ Model checking QCTL plus on quantum Markov chains ⋮ Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ A General Framework for Probabilistic Characterizing Formulae ⋮ Temporal logics for the specification of performance and reliability ⋮ Quantitative solution of omega-regular games ⋮ Symbolic model checking for probabilistic timed automata ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Model Checking Probabilistic Systems ⋮ Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system ⋮ Automatic verification of concurrent stochastic systems ⋮ Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods ⋮ Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Quantitative verification and strategy synthesis for stochastic games ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ Means-end relations and a measure of efficacy ⋮ Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Metrics for labelled Markov processes ⋮ Symbolic model checking for probabilistic processes ⋮ A Tutorial on Interactive Markov Chains ⋮ On Abstraction of Probabilistic Systems ⋮ Parametric probabilistic transition systems for system design and analysis ⋮ Compositional probabilistic verification through multi-objective model checking ⋮ Safety verification for probabilistic hybrid systems ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ Approximating labelled Markov processes ⋮ Model checking differentially private properties ⋮ Statistical model checking of stochastic component-based systems ⋮ Multiphase until formulas over Markov reward models: an algebraic approach ⋮ On the use of MTBDDs for performability analysis and verification of stochastic systems. ⋮ Symbolic control for stochastic systems via finite parity games ⋮ Probabilistic may/must testing: retaining probabilities by restricted schedulers ⋮ Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} ⋮ Probabilistic CEGAR ⋮ Formal modelling and verification of probabilistic resource bounded agents ⋮ Minimization of probabilistic models of programs ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Reachability in recursive Markov decision processes ⋮ Cognitive Reasoning and Trust in Human-Robot Interactions ⋮ Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study ⋮ Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes ⋮ Exact quantitative probabilistic model checking through rational search ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations ⋮ Deciding bisimilarity and similarity for probabilistic processes. ⋮ Quantitative Multi-objective Verification for Probabilistic Systems ⋮ The complexity of synchronizing Markov decision processes ⋮ Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata ⋮ Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives ⋮ Automatic verification of competitive stochastic systems ⋮ Preface to the special issue on probabilistic model checking ⋮ Model checking for probabilistic timed automata ⋮ Probabilistic verification and approximation ⋮ Game-Based Probabilistic Predicate Abstraction in PRISM ⋮ Model Checking Quantitative Linear Time Logic ⋮ Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking ⋮ Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ Deciding probabilistic bisimilarity over infinite-state probabilistic systems ⋮ Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ The well-designed logical robot: learning and experience from observations to the Situation Calculus ⋮ Quantifying opacity ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Stochastic game logic ⋮ On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems ⋮ Unnamed Item ⋮ Model checking mobile stochastic logic ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Computation tree measurement language (CTML) ⋮ Conditional Probabilities over Probabilistic and Nondeterministic Systems ⋮ Model-Checking ω-Regular Properties of Interval Markov Chains ⋮ Probabilistic mobile ambients ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ Bisimulations Meet PCTL Equivalences for Probabilistic Automata ⋮ Efficient Decomposition Algorithm for Stationary Analysis of Complex Stochastic Petri Net Models ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations ⋮ Branching bisimulation congruence for probabilistic systems ⋮ Quantitative Analysis under Fairness Constraints ⋮ Can we build it: formal synthesis of control strategies for cooperative driver assistance systems ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Measuring and Synthesizing Systems in Probabilistic Environments ⋮ Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes ⋮ Model checking discounted temporal properties ⋮ On probabilistic timed automata. ⋮ Weak Probabilistic Anonymity ⋮ On the verification of qualitative properties of probabilistic processes under fairness constraints. ⋮ Automatic verification of real-time systems with discrete probability distributions. ⋮ Probabilistic Temporal Logics
