Symbolic model checking for probabilistic processes

DOI10.1007/3-540-63165-8_199zbMath1401.68180OpenAlexW1806449990MaRDI QIDQ4571974

No author found.

Publication date: 4 July 2018

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63165-8_199

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

Synthesizing efficient systems in probabilistic environments, Model Checking Probabilistic Systems, Model Checking Linear-Time Properties of Probabilistic Systems, Metrics for labelled Markov processes, Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains, Approximating labelled Markov processes, Symbolic verification and strategy synthesis for turn-based stochastic games, Minimization of probabilistic models of programs, Three-valued abstraction for probabilistic systems, Deciding bisimilarity and similarity for probabilistic processes., Preface to the special issue on probabilistic model checking, Bayesian statistical model checking with application to Stateflow/Simulink verification, Towards classifying propositional probabilistic logics, Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement, Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey, Approximate Verification of the Symbolic Dynamics of Markov Chains, Temporalization of Probabilistic Propositional Logic, Compositional Model Checking of product-form CTMCs, System design of stochastic models using robustness of temporal properties

Cites Work

• A probabilistic PDL
• Verification of multiprocess probabilistic protocols
• Bisimulation through probabilistic testing
• Symbolic model checking: \(10^{20}\) states and beyond
• Iteration theories of synchronization trees
• A logic for reasoning about time and reliability
• Generating BDDs for symbolic model checking in CCS
• Model checking of probabilistic and nondeterministic systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• The complexity of probabilistic verification
• Termination of Probabilistic Concurrent Program
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item