{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:41Z","timestamp":1776482081786,"version":"3.51.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,11,12]],"date-time":"2008-11-12T00:00:00Z","timestamp":1226448000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study and provide efficient algorithms for multi-objective model checking\nproblems for Markov Decision Processes (MDPs). Given an MDP, M, and given\nmultiple linear-time (\\omega -regular or LTL) properties \\varphi\\_i, and\nprobabilities r\\_i \\epsilon [0,1], i=1,...,k, we ask whether there exists a\nstrategy \\sigma for the controller such that, for all i, the probability that a\ntrajectory of M controlled by \\sigma satisfies \\varphi\\_i is at least r\\_i. We\nprovide an algorithm that decides whether there exists such a strategy and if\nso produces it, and which runs in time polynomial in the size of the MDP. Such\na strategy may require the use of both randomization and memory. We also\nconsider more general multi-objective \\omega -regular queries, which we\nmotivate with an application to assume-guarantee compositional reasoning for\nprobabilistic systems.\n  Note that there can be trade-offs between different properties: satisfying\nproperty \\varphi\\_1 with high probability may necessitate satisfying \\varphi\\_2\nwith low probability. Viewing this as a multi-objective optimization problem,\nwe want information about the \"trade-off curve\" or Pareto curve for maximizing\nthe probabilities of different properties. We show that one can compute an\napproximate Pareto curve with respect to a set of \\omega -regular properties in\ntime polynomial in the size of the MDP.\n  Our quantitative upper bounds use LP methods. We also study qualitative\nmulti-objective model checking problems, and we show that these can be analysed\nby purely graph-theoretic methods, even though the strategies may still require\nboth randomization and memory.<\/jats:p>","DOI":"10.2168\/lmcs-4(4:8)2008","type":"journal-article","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T10:25:15Z","timestamp":1231496715000},"source":"Crossref","is-referenced-by-count":65,"title":["Multi-Objective Model Checking of Markov Decision Processes"],"prefix":"10.46298","volume":"Volume 4, Issue 4","author":[{"given":"Kousha","family":"Etessami","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Mihalis","family":"Yannakakis","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,11,12]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/990\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/990\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:48Z","timestamp":1681243248000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/990"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,12]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(4:8)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0810.5728","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0810.5728","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-06200-6_24","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,12]]},"article-number":"990"}}