Compositional probabilistic verification through multi-objective model checking

DOI10.1016/j.ic.2013.10.001zbMath1277.68138OpenAlexW2104298332MaRDI QIDQ386007

Mohammad Hasan, H. S. Yoon

Publication date: 13 December 2013

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2013.10.001

zbMATH Keywords

probabilistic automatacompositional verificationprobabilistic verificationassume-guarantee reasoning

Mathematics Subject Classification ID

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

Related Items (7)

Model Checking Probabilistic Systems ⋮ Compositional strategy synthesis for stochastic games with multiple objectives ⋮ Quantitative verification and strategy synthesis for stochastic games ⋮ Compositional abstraction-based synthesis for networks of stochastic switched systems ⋮ Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach ⋮ Probabilistic verification of hierarchical leader election protocol in dynamic systems ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey

Uses Software

• PRISM
• ECDAR
• LiQuor

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal methods for eternal networked software systems. 11th international school on formal methods for the design of computer, communication and software systems, SFM 2011, Bertinoro, Italy, June 13--18, 2011. Advanced lectures
• Interactive Markov chains. And the quest for quantified quality
• Performance analysis of probabilistic timed automata using digital clocks
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Model checking of probabilistic and nondeterministic systems
• Quantitative Multi-objective Verification for Probabilistic Systems
• Fast randomized consensus using shared memory
• Assume-Guarantee Verification for Probabilistic Systems
• Multi-Objective Model Checking of Markov Decision Processes
• Quantitative Analysis under Fairness Constraints
• Tentative steps toward a development method for interfering programs
• Markov decision processes and regular events
• Pareto Curves for Probabilistic Model Checking
• Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Theoretical Aspects of Computing - ICTAC 2004
• Multi-objective Model Checking of Markov Decision Processes

This page was built for publication: Compositional probabilistic verification through multi-objective model checking