Multi-Objective Model Checking of Markov Decision Processes

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...

Full description

Bibliographic Details
Main Authors: Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2008-11-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/990/pdf