Search

• < Previous
• 1
• Next >

---

Multi-Objective Model Checking of Markov Decision Processes

Kousha Etessami ; Marta Kwiatkowska ; Moshe Y. Vardi ; Mihalis Yannakakis.

We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (\omega -regular or LTL) properties \varphi\_i, and probabilities r\_i \epsilon [0,1], i=1,...,k, we ask whether there exists a&nbsp;[&hellip;]

---

Permissive Controller Synthesis for Probabilistic Systems

Klaus Drager ; Vojtech Forejt ; Marta Kwiatkowska ; David Parker ; Mateusz Ujma.

We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty&nbsp;[&hellip;]

---