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 (ω-regular or LTL) properties φi, and probabilities ri ∈ [0,1], i=1,...,k, we ask whether there exists a strategy σ for the cont...
Main Authors: | Etessami, K, Kwiatkowska, M, Vardi, M, Yannakakis, M |
---|---|
Format: | Journal article |
Language: | English |
Published: |
2008
|
Similar Items
-
Compositional probabilistic verification through multi-objective model checking
by: Kwiatkowska, M, et al.
Published: (2013) -
Multi-objective robust strategy synthesis for Interval Markov decision processes
by: Hahn, E, et al.
Published: (2017) -
Specification revision for Markov decision processes with optimal trade-off
by: Lahijanian, M, et al.
Published: (2016) -
Markov Decision Processes with Multiple Long-run Average Objectives
by: Brázdil, T, et al.
Published: (2011) -
Quantitative model-checking of controlled discrete-time Markov processes
by: Tkachev, I, et al.
Published: (2016)