Synthesizing efficient systems in probabilistic environments

DOI10.1007/s00236-015-0237-yzbMath1344.68171OpenAlexW837466048MaRDI QIDQ300419

F. Blanchet-Sadri, M. Dambrine

Publication date: 28 June 2016

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/20450025/acta_inf_synth.pdf

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Uses Software

• PRISM
• MCQueue

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Performance analysis of probabilistic timed automata using digital clocks
• N-process mutual exclusion with bounded waiting by 4. log//2N-valued shared variable
• Symbolic model checking: \(10^{20}\) states and beyond
• Synthesizing robust systems
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Using probabilistic model checking for dynamic power management
• On Sequential Decisions and Markov Chains
• Synthesizing Efficient Controllers
• Quantitative Multi-objective Verification for Probabilistic Systems
• Temporal Verification of Reactive Systems: Response
• Pure Stationary Optimal Strategies in Markov Decision Processes
• Better Quality in Synthesis through Quantitative Objectives
• Graph-Based Algorithms for Boolean Function Manipulation
• Markov Chains
• Symbolic model checking for probabilistic processes
• Markov Decision Processes with Multiple Objectives
• Multi-objective Model Checking of Markov Decision Processes