Compositional probabilistic verification through multi-objective model checking
DOI10.1016/J.IC.2013.10.001zbMATH Open1277.68138OpenAlexW2104298332MaRDI QIDQ386007FDOQ386007
Authors: Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu 
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
Recommendations
- Assume-guarantee verification for probabilistic systems
- Quantitative multi-objective verification for probabilistic systems
- Learning-based compositional verification for synchronous probabilistic systems
- Automated verification and strategy synthesis for probabilistic systems
- Leveraging weighted automata in compositional reasoning about concurrent probabilistic systems
probabilistic automatacompositional verificationprobabilistic verificationassume-guarantee reasoning
Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
- Interactive Markov chains. And the quest for quantified quality
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Model checking of probabilistic and nondeterministic systems
- Title not available (Why is that?)
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- Quantitative multi-objective verification for probabilistic systems
- Multi-objective Model Checking of Markov Decision Processes
- Performance analysis of probabilistic timed automata using digital clocks
- Markov decision processes and regular events
- Tentative steps toward a development method for interfering programs
- Title not available (Why is that?)
- Multi-Objective Model Checking of Markov Decision Processes
- Pareto curves for probabilistic model checking
- Fast randomized consensus using shared memory
- Title not available (Why is that?)
- Assume-guarantee verification for probabilistic systems
- Quantitative analysis under fairness constraints
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Theoretical Aspects of Computing - ICTAC 2004
Cited In (20)
- Trade-off analysis meets probabilistic model checking
- Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
- Assume-guarantee verification for probabilistic systems
- Model checking probabilistic systems
- Statistically sound verification and optimization for complex systems
- Compositional strategy synthesis for stochastic games with multiple objectives
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Quantitative verification and strategy synthesis for stochastic games
- Compositional analysis of probabilistic timed graph transformation systems
- Quantitative multi-objective verification for probabilistic systems
- Compositional abstraction-based synthesis for networks of stochastic switched systems
- Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach
- Verification of compliance for multilevel models in individual trace semantics
- Learning-based compositional verification for synchronous probabilistic systems
- Automated verification and strategy synthesis for probabilistic systems
- Compositional probabilistic model checking with string diagrams of MDPs
- Learning assumptions for compositional verification of timed automata
- A compositional approach to parity games
- Multi-agent verification and control with probabilistic model checking
- Probabilistic verification of hierarchical leader election protocol in dynamic systems
Uses Software
This page was built for publication: Compositional probabilistic verification through multi-objective model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q386007)
