Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

DOI10.1007/978-3-540-70583-3_13zbMath1155.68427OpenAlexW1502518842MaRDI QIDQ3519498

Tomáš Brázdil, Vojtěch Forejt, Antonín Kučera

Publication date: 19 August 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-70583-3_13

Mathematics Subject Classification ID

Synthesis problems (93B50) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (9)

The satisfiability problem for a quantitative fragment of PCTL ⋮ Model Checking Probabilistic Systems ⋮ Satisfiability of quantitative probabilistic CTL: rise to the challenge ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives ⋮ Quantitative Multi-objective Verification for Probabilistic Systems ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Stochastic game logic

Cites Work

• A logic for reasoning about time and reliability
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
• Branching-Time Model-Checking of Probabilistic Pushdown Automata
• STACS 2004
• Markov Decision Processes with Multiple Objectives
• Multi-objective Model Checking of Markov Decision Processes
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives