--- _id: '8193' abstract: - lang: eng text: 'Multiple-environment Markov decision processes (MEMDPs) are MDPs equipped with not one, but multiple probabilistic transition functions, which represent the various possible unknown environments. While the previous research on MEMDPs focused on theoretical properties for long-run average payoff, we study them with discounted-sum payoff and focus on their practical advantages and applications. MEMDPs can be viewed as a special case of Partially observable and Mixed observability MDPs: the state of the system is perfectly observable, but not the environment. We show that the specific structure of MEMDPs allows for more efficient algorithmic analysis, in particular for faster belief updates. We demonstrate the applicability of MEMDPs in several domains. In particular, we formalize the sequential decision-making approach to contextual recommendation systems as MEMDPs and substantially improve over the previous MDP approach.' acknowledgement: Krishnendu Chatterjee is supported by the Austrian ScienceFund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE),and COST Action GAMENET. Petr Novotn ́y is supported bythe Czech Science Foundation grant No. GJ19-15134Y. article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Deep full_name: Karkhanis, Deep last_name: Karkhanis - first_name: Petr full_name: Novotný, Petr id: 3CC3B868-F248-11E8-B48F-1D18A9856A87 last_name: Novotný - first_name: Amélie full_name: Royer, Amélie id: 3811D890-F248-11E8-B48F-1D18A9856A87 last_name: Royer orcid: 0000-0002-8407-0705 citation: ama: 'Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: Proceedings of the 30th International Conference on Automated Planning and Scheduling. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.' apa: 'Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., & Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In Proceedings of the 30th International Conference on Automated Planning and Scheduling (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence.' chicago: 'Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In Proceedings of the 30th International Conference on Automated Planning and Scheduling, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020.' ieee: 'K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment Markov decision processes: Efficient analysis and applications,” in Proceedings of the 30th International Conference on Automated Planning and Scheduling, Nancy, France, 2020, vol. 30, pp. 48–56.' ista: 'Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. 2020. Multiple-environment Markov decision processes: Efficient analysis and applications. Proceedings of the 30th International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 30, 48–56.' mla: 'Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” Proceedings of the 30th International Conference on Automated Planning and Scheduling, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.' short: K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, A. Royer, in:, Proceedings of the 30th International Conference on Automated Planning and Scheduling, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56. conference: end_date: 2020-10-30 location: Nancy, France name: 'ICAPS: International Conference on Automated Planning and Scheduling' start_date: 2020-10-26 date_created: 2020-08-02T22:00:58Z date_published: 2020-06-01T00:00:00Z date_updated: 2023-09-07T13:16:18Z day: '01' department: - _id: KrCh intvolume: ' 30' language: - iso: eng month: '06' oa_version: None page: 48-56 project: - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: Proceedings of the 30th International Conference on Automated Planning and Scheduling publication_identifier: eissn: - '23340843' issn: - '23340835' publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' related_material: record: - id: '8390' relation: dissertation_contains status: public scopus_import: '1' status: public title: 'Multiple-environment Markov decision processes: Efficient analysis and applications' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 30 year: '2020' ... --- _id: '1407' abstract: - lang: eng text: We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study. article_processing_charge: No arxiv: 1 author: - first_name: Mária full_name: Svoreňová, Mária last_name: Svoreňová - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ivana full_name: Cěrná, Ivana last_name: Cěrná - first_name: Cǎlin full_name: Belta, Cǎlin last_name: Belta citation: ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006' apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006' chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.' ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.' ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.' mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.' short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.' date_created: 2018-12-11T11:51:50Z date_published: 2017-02-01T00:00:00Z date_updated: 2023-09-20T09:43:09Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1016/j.nahs.2016.04.006 ec_funded: 1 external_id: arxiv: - '1410.5387' isi: - '000390637000014' intvolume: ' 23' isi: 1 issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1410.5387 month: '02' oa: 1 oa_version: Preprint page: 230 - 253 project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: 'Nonlinear Analysis: Hybrid Systems' publication_status: published publisher: Elsevier publist_id: '5800' quality_controlled: '1' related_material: record: - id: '1689' relation: earlier_version status: public scopus_import: '1' status: public title: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 23 year: '2017' ... --- _id: '1166' abstract: - lang: eng text: POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Jessica full_name: Davies, Jessica id: 378E0060-F248-11E8-B48F-1D18A9856A87 last_name: Davies citation: ama: 'Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.' apa: 'Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.' chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016:3225–32. AAAI Press, 2016. ieee: K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232. ista: 'Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.' mla: Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp. 3225–32. short: K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232. conference: end_date: 2016-02-17 location: Phoenix, AZ, USA name: 'AAAI: Conference on Artificial Intelligence' start_date: 2016-02-12 date_created: 2018-12-11T11:50:30Z date_published: 2016-12-02T00:00:00Z date_updated: 2023-02-23T12:26:41Z day: '02' department: - _id: KrCh - _id: ToHe ec_funded: 1 intvolume: ' 2016' language: - iso: eng month: '12' oa_version: None page: 3225 - 3232 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence publication_status: published publisher: AAAI Press publist_id: '6191' quality_controlled: '1' related_material: link: - relation: table_of_contents url: https://dl.acm.org/citation.cfm?id=3016355 record: - id: '5443' relation: earlier_version status: public status: public title: A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 2016 year: '2016' ... --- _id: '1477' abstract: - lang: eng text: We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples. arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Mathieu full_name: Tracol, Mathieu id: 3F54FA38-F248-11E8-B48F-1D18A9856A87 last_name: Tracol citation: ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 2016;82(5):878-911. doi:10.1016/j.jcss.2016.02.009 apa: Chatterjee, K., Chmelik, M., & Tracol, M. (2016). What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.02.009 chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences. Elsevier, 2016. https://doi.org/10.1016/j.jcss.2016.02.009. ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with ω-regular objectives,” Journal of Computer and System Sciences, vol. 82, no. 5. Elsevier, pp. 878–911, 2016. ista: Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 82(5), 878–911. mla: Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:10.1016/j.jcss.2016.02.009. short: K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences 82 (2016) 878–911. date_created: 2018-12-11T11:52:15Z date_published: 2016-08-01T00:00:00Z date_updated: 2023-02-23T12:24:38Z day: '01' department: - _id: KrCh doi: 10.1016/j.jcss.2016.02.009 ec_funded: 1 external_id: arxiv: - '1309.2802' intvolume: ' 82' issue: '5' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1309.2802 month: '08' oa: 1 oa_version: Preprint page: 878 - 911 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Journal of Computer and System Sciences publication_status: published publisher: Elsevier publist_id: '5718' quality_controlled: '1' related_material: record: - id: '2295' relation: earlier_version status: public - id: '5400' relation: earlier_version status: public scopus_import: 1 status: public title: What is decidable about partially observable Markov decision processes with ω-regular objectives type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 82 year: '2016' ... --- _id: '1518' abstract: - lang: eng text: The inference of demographic history from genome data is hindered by a lack of efficient computational approaches. In particular, it has proved difficult to exploit the information contained in the distribution of genealogies across the genome. We have previously shown that the generating function (GF) of genealogies can be used to analytically compute likelihoods of demographic models from configurations of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has a simple, recursive form, the size of such likelihood calculations explodes quickly with the number of individuals and applications of this framework have so far been mainly limited to small samples (pairs and triplets) for which the GF can be written by hand. Here we investigate several strategies for exploiting the inherent symmetries of the coalescent. In particular, we show that the GF of genealogies can be decomposed into a set of equivalence classes that allows likelihood calculations from nontrivial samples. Using this strategy, we automated blockwise likelihood calculations for a general set of demographic scenarios in Mathematica. These histories may involve population size changes, continuous migration, discrete divergence, and admixture between multiple populations. To give a concrete example, we calculate the likelihood for a model of isolation with migration (IM), assuming two diploid samples without phase and outgroup information. We demonstrate the new inference scheme with an analysis of two individual butterfly genomes from the sister species Heliconius melpomene rosina and H. cydno. acknowledgement: "We thank Lynsey Bunnefeld for discussions throughout the project and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on an earlier version of this manuscript. This work was supported by funding from the\r\nUnited Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant from the European\r\nResearch Council (250152) (to N.H.B.)." article_processing_charge: No article_type: original author: - first_name: Konrad full_name: Lohse, Konrad last_name: Lohse - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Simon full_name: Martin, Simon last_name: Martin - first_name: Nicholas H full_name: Barton, Nicholas H id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 citation: ama: Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. 2016;202(2):775-786. doi:10.1534/genetics.115.183814 apa: Lohse, K., Chmelik, M., Martin, S., & Barton, N. H. (2016). Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.115.183814 chicago: Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics. Genetics Society of America, 2016. https://doi.org/10.1534/genetics.115.183814. ieee: K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for calculating blockwise likelihoods under the coalescent,” Genetics, vol. 202, no. 2. Genetics Society of America, pp. 775–786, 2016. ista: Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786. mla: Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics, vol. 202, no. 2, Genetics Society of America, 2016, pp. 775–86, doi:10.1534/genetics.115.183814. short: K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786. date_created: 2018-12-11T11:52:29Z date_published: 2016-02-01T00:00:00Z date_updated: 2025-05-28T11:42:48Z day: '01' ddc: - '570' department: - _id: KrCh - _id: NiBa doi: 10.1534/genetics.115.183814 ec_funded: 1 external_id: pmid: - '26715666' file: - access_level: open_access checksum: 41c9b5d72e7fe4624dd22dfe622337d5 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:51Z date_updated: 2020-07-14T12:45:00Z file_id: '5241' file_name: IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf file_size: 957466 relation: main_file file_date_updated: 2020-07-14T12:45:00Z has_accepted_license: '1' intvolume: ' 202' issue: '2' language: - iso: eng month: '02' oa: 1 oa_version: Preprint page: 775 - 786 pmid: 1 project: - _id: 25B07788-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '250152' name: Limits to selection in biology and in evolutionary computation publication: Genetics publication_status: published publisher: Genetics Society of America publist_id: '5658' pubrep_id: '561' quality_controlled: '1' scopus_import: '1' status: public title: Efficient strategies for calculating blockwise likelihoods under the coalescent type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 202 year: '2016' ... --- _id: '1529' abstract: - lang: eng text: 'We consider partially observable Markov decision processes (POMDPs) with a set of target states and an integer cost associated with every transition. The optimization objective we study asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.' acknowledgement: 'We thank Blai Bonet for helping us with RTDP-Bel. The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.' article_processing_charge: No arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. 2016;234:26-48. doi:10.1016/j.artint.2016.01.007 apa: Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2016). Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2016.01.007 chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence. Elsevier, 2016. https://doi.org/10.1016/j.artint.2016.01.007. ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” Artificial Intelligence, vol. 234. Elsevier, pp. 26–48, 2016. ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. 234, 26–48. mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence, vol. 234, Elsevier, 2016, pp. 26–48, doi:10.1016/j.artint.2016.01.007. short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence 234 (2016) 26–48. date_created: 2018-12-11T11:52:33Z date_published: 2016-05-01T00:00:00Z date_updated: 2023-02-23T12:25:49Z day: '01' department: - _id: KrCh doi: 10.1016/j.artint.2016.01.007 ec_funded: 1 external_id: arxiv: - '1411.3880' intvolume: ' 234' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1411.3880 month: '05' oa: 1 oa_version: Preprint page: 26 - 48 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: Artificial Intelligence publication_status: published publisher: Elsevier publist_id: '5642' quality_controlled: '1' related_material: record: - id: '1820' relation: earlier_version status: public - id: '5425' relation: earlier_version status: public scopus_import: 1 status: public title: Optimal cost almost-sure reachability in POMDPs type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 234 year: '2016' ... --- _id: '1324' abstract: - lang: eng text: 'DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. DEC-POMDPs have been studied with finite-horizon and infinite-horizon discounted-sum objectives, and there exist solvers both for exact and approximate solutions. In this work we consider Goal-DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the RTDP-Bel approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. Copyright ' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: 'Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs. In: Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling. Vol 2016-January. AAAI Press; 2016:88-96.' apa: 'Chatterjee, K., & Chmelik, M. (2016). Indefinite-horizon reachability in Goal-DEC-POMDPs. In Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling (Vol. 2016–January, pp. 88–96). London, United Kingdom: AAAI Press.' chicago: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” In Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, 2016–January:88–96. AAAI Press, 2016. ieee: K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,” in Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, London, United Kingdom, 2016, vol. 2016–January, pp. 88–96. ista: 'Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs. Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 2016–January, 88–96.' mla: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, vol. 2016–January, AAAI Press, 2016, pp. 88–96. short: K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, AAAI Press, 2016, pp. 88–96. conference: end_date: 2016-06-17 location: London, United Kingdom name: 'ICAPS: International Conference on Automated Planning and Scheduling' start_date: 2016-06-12 date_created: 2018-12-11T11:51:22Z date_published: 2016-01-01T00:00:00Z date_updated: 2021-01-12T06:49:53Z day: '01' department: - _id: KrCh ec_funded: 1 language: - iso: eng main_file_link: - url: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999 month: '01' oa_version: None page: 88 - 96 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling publication_status: published publisher: AAAI Press publist_id: '5946' quality_controlled: '1' scopus_import: 1 status: public title: Indefinite-horizon reachability in Goal-DEC-POMDPs type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 2016-January year: '2016' ... --- _id: '1327' abstract: - lang: eng text: 'We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard constraint. The energy levels may increase and decrease with transitions, and the hard constraint requires that the energy level must remain positive in all steps till the target is reached. First, we present a novel algorithm for solving POMDPs with energy levels, developing on existing POMDP solvers and using RTDP as its main method. Our second contribution is related to policy representation. For larger POMDP instances the policies computed by existing solvers are too large to be understandable. We present an automated procedure based on machine learning techniques that automatically extracts important decisions of the policy allowing us to compute succinct human readable policies. Finally, we show experimentally that our algorithm performs well and computes succinct policies on a number of POMDP instances from the literature that were naturally enhanced with energy levels. ' author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Anchit full_name: Gupta, Anchit last_name: Gupta - first_name: Petr full_name: Novotny, Petr id: 3CC3B868-F248-11E8-B48F-1D18A9856A87 last_name: Novotny citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest path with energy constraints in POMDPs. In: Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016). Stochastic shortest path with energy constraints in POMDPs. In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (pp. 1465–1466). Singapore: ACM.' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, 1465–66. ACM, 2016. ieee: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic shortest path with energy constraints in POMDPs,” in Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, Singapore, 2016, pp. 1465–1466. ista: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic shortest path with energy constraints in POMDPs. Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents & Multiagent Systems, 1465–1466.' mla: Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–66. short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466. conference: end_date: 2016-05-13 location: Singapore name: 'AAMAS: Autonomous Agents & Multiagent Systems' start_date: 2016-05-09 date_created: 2018-12-11T11:51:23Z date_published: 2016-01-01T00:00:00Z date_updated: 2021-01-12T06:49:54Z day: '01' department: - _id: KrCh ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1602.07565 month: '01' oa: 1 oa_version: Preprint page: 1465 - 1466 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems publication_status: published publisher: ACM publist_id: '5942' quality_controlled: '1' scopus_import: 1 status: public title: Stochastic shortest path with energy constraints in POMDPs type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '1397' abstract: - lang: eng text: 'We study partially observable Markov decision processes (POMDPs) with objectives used in verification and artificial intelligence. The qualitative analysis problem given a POMDP and an objective asks whether there is a strategy (policy) to ensure that the objective is satisfied almost surely (with probability 1), resp. with positive probability (with probability greater than 0). For POMDPs with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the payoff of an infinite path is the long-run average of the rewards, we consider two types of path constraints: (i) a quantitative limit-average constraint defines the set of paths where the payoff is at least a given threshold L1 = 1. Our main results for qualitative limit-average constraint under almost-sure winning are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative limit-average constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We present a prototype implementation of our EXPTIME algorithm. For POMDPs with w-regular conditions specified as parity objectives, while the qualitative analysis problems are known to be undecidable even for very special case of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. Based on our theoretical algorithms we also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of well-known POMDP examples for robotics applications. For POMDPs with a set of target states and an integer cost associated with every transition, we study the optimization objective that asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely. We show that for general integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double and exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms that extend existing algorithms for POMDPs with finite-horizon objectives. We show experimentally that it performs well in many examples of interest. We study more deeply the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a strategy to ensure that the target set is reached almost surely. While in general the problem EXPTIME-complete, in many practical cases strategies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. We first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. In this work we consider Goal DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. In the end we present a short summary of a few other results related to verification of MDPs and POMDPs.' alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: Chmelik M. Algorithms for partially observable markov decision processes. 2016. apa: Chmelik, M. (2016). Algorithms for partially observable markov decision processes. Institute of Science and Technology Austria. chicago: Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.” Institute of Science and Technology Austria, 2016. ieee: M. Chmelik, “Algorithms for partially observable markov decision processes,” Institute of Science and Technology Austria, 2016. ista: Chmelik M. 2016. Algorithms for partially observable markov decision processes. Institute of Science and Technology Austria. mla: Chmelik, Martin. Algorithms for Partially Observable Markov Decision Processes. Institute of Science and Technology Austria, 2016. short: M. Chmelik, Algorithms for Partially Observable Markov Decision Processes, Institute of Science and Technology Austria, 2016. date_created: 2018-12-11T11:51:47Z date_published: 2016-02-01T00:00:00Z date_updated: 2023-09-07T11:54:58Z day: '01' degree_awarded: PhD department: - _id: KrCh language: - iso: eng month: '02' oa_version: None page: '232' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5810' status: public supervisor: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X title: Algorithms for partially observable markov decision processes type: dissertation user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2016' ... --- _id: '1689' abstract: - lang: eng text: We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study. author: - first_name: Mária full_name: Svoreňová, Mária last_name: Svoreňová - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ivana full_name: Cěrná, Ivana last_name: Cěrná - first_name: Cǎlin full_name: Belta, Cǎlin last_name: Belta citation: ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608' apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728608' chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.' ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.' ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.' mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.' short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.' conference: end_date: 2015-04-16 location: Seattle, WA, United States name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2015-04-14 date_created: 2018-12-11T11:53:29Z date_published: 2015-04-14T00:00:00Z date_updated: 2023-09-20T09:43:09Z day: '14' department: - _id: ToHe - _id: KrCh doi: 10.1145/2728606.2728608 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1410.5387 month: '04' oa: 1 oa_version: Preprint page: 259 - 268 project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: 'Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control' publication_status: published publisher: ACM publist_id: '5456' related_material: record: - id: '1407' relation: later_version status: public scopus_import: 1 status: public title: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1691' abstract: - lang: eng text: We consider a case study of the problem of deploying an autonomous air vehicle in a partially observable, dynamic, indoor environment from a specification given as a linear temporal logic (LTL) formula over regions of interest. We model the motion and sensing capabilities of the vehicle as a partially observable Markov decision process (POMDP). We adapt recent results for solving POMDPs with parity objectives to generate a control policy. We also extend the existing framework with a policy minimization technique to obtain a better implementable policy, while preserving its correctness. The proposed techniques are illustrated in an experimental setup involving an autonomous quadrotor performing surveillance in a dynamic environment. author: - first_name: Mária full_name: Svoreňová, Mária last_name: Svoreňová - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Kevin full_name: Leahy, Kevin last_name: Leahy - first_name: Hasan full_name: Eniser, Hasan last_name: Eniser - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ivana full_name: Cěrná, Ivana last_name: Cěrná - first_name: Cǎlin full_name: Belta, Cǎlin last_name: Belta citation: ama: 'Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:233-238. doi:10.1145/2728606.2728617' apa: 'Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 233–238). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728617' chicago: 'Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 233–38. ACM, 2015. https://doi.org/10.1145/2728606.2728617.' ieee: 'M. Svoreňová et al., “Temporal logic motion planning using POMDPs with parity objectives: Case study paper,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 233–238.' ista: 'Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238.' mla: 'Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–38, doi:10.1145/2728606.2728617.' short: 'M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–238.' conference: end_date: 2015-04-16 location: Seattle, WA, United States name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2015-04-14 date_created: 2018-12-11T11:53:29Z date_published: 2015-04-14T00:00:00Z date_updated: 2021-01-12T06:52:33Z day: '14' department: - _id: KrCh doi: 10.1145/2728606.2728617 ec_funded: 1 language: - iso: eng month: '04' oa_version: None page: 233 - 238 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: 'Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control' publication_status: published publisher: ACM publist_id: '5453' scopus_import: 1 status: public title: 'Temporal logic motion planning using POMDPs with parity objectives: Case study paper' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1732' abstract: - lang: eng text: We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty. arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. In: IEEE; 2015:325-330. doi:10.1109/ICRA.2015.7139019' apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications (pp. 325–330). Presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States: IEEE. https://doi.org/10.1109/ICRA.2015.7139019' chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications,” 325–30. IEEE, 2015. https://doi.org/10.1109/ICRA.2015.7139019. ieee: 'K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Qualitative analysis of POMDPs with temporal logic specifications for robotics applications,” presented at the ICRA: International Conference on Robotics and Automation, Seattle, WA, United States, 2015, pp. 325–330.' ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. ICRA: International Conference on Robotics and Automation, 325–330.' mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IEEE, 2015, pp. 325–30, doi:10.1109/ICRA.2015.7139019. short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, IEEE, 2015, pp. 325–330. conference: end_date: 2015-05-30 location: Seattle, WA, United States name: 'ICRA: International Conference on Robotics and Automation' start_date: 2015-05-26 date_created: 2018-12-11T11:53:43Z date_published: 2015-01-01T00:00:00Z date_updated: 2023-02-23T12:25:52Z day: '01' department: - _id: KrCh doi: 10.1109/ICRA.2015.7139019 ec_funded: 1 external_id: arxiv: - '1409.3360' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1409.3360 month: '01' oa: 1 oa_version: Preprint page: 325 - 330 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: IEEE publist_id: '5394' quality_controlled: '1' related_material: record: - id: '5424' relation: earlier_version status: public - id: '5426' relation: earlier_version status: public scopus_import: 1 status: public title: Qualitative analysis of POMDPs with temporal logic specifications for robotics applications type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1820' abstract: - lang: eng text: 'We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objec- tive we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present ap- proximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst- case running time of our algorithm is double exponential, we present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples.' acknowledgement: ' The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.' alternative_title: - Artifical Intelligence arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: ama: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence . Vol 5. AAAI Press; 2015:3496-3502.' apa: 'Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Optimal cost almost-sure reachability in POMDPs. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3496–3502). Austin, TX, USA: AAAI Press.' chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , 5:3496–3502. AAAI Press, 2015. ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” in Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , Austin, TX, USA, 2015, vol. 5, pp. 3496–3502. ista: 'Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Optimal cost almost-sure reachability in POMDPs. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence . IAAI: Innovative Applications of Artificial Intelligence, Artifical Intelligence, vol. 5, 3496–3502.' mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , vol. 5, AAAI Press, 2015, pp. 3496–502. short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp. 3496–3502. conference: end_date: 2015-01-30 location: Austin, TX, USA name: 'IAAI: Innovative Applications of Artificial Intelligence' start_date: 2015-01-25 date_created: 2018-12-11T11:54:11Z date_published: 2015-06-01T00:00:00Z date_updated: 2023-02-23T10:02:57Z day: '01' department: - _id: KrCh ec_funded: 1 external_id: arxiv: - '1411.3880' intvolume: ' 5' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1411.3880 month: '06' oa: 1 oa_version: Preprint page: 3496-3502 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: 'Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ' publication_status: published publisher: AAAI Press publist_id: '5286' quality_controlled: '1' related_material: record: - id: '1529' relation: later_version status: public scopus_import: 1 status: public title: Optimal cost almost-sure reachability in POMDPs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 5 year: '2015' ... --- _id: '1873' abstract: - lang: eng text: 'We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated with every transition, and the payoff of an infinite path is the long-run average of the rewards. We consider two types of path constraints: (i) a quantitative constraint defines the set of paths where the payoff is at least a given threshold λ1ε(0,1]; and (ii) a qualitative constraint which is a special case of the quantitative constraint with λ1=1. We consider the computation of the almost-sure winning set, where the controller needs to ensure that the path constraint is satisfied with probability 1. Our main results for qualitative path constraints are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative path constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We also present a prototype implementation of our EXPTIME algorithm and experimental results on several examples.' arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: Chatterjee K, Chmelik M. POMDPs under probabilistic semantics. Artificial Intelligence. 2015;221:46-72. doi:10.1016/j.artint.2014.12.009 apa: Chatterjee, K., & Chmelik, M. (2015). POMDPs under probabilistic semantics. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2014.12.009 chicago: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” Artificial Intelligence. Elsevier, 2015. https://doi.org/10.1016/j.artint.2014.12.009. ieee: K. Chatterjee and M. Chmelik, “POMDPs under probabilistic semantics,” Artificial Intelligence, vol. 221. Elsevier, pp. 46–72, 2015. ista: Chatterjee K, Chmelik M. 2015. POMDPs under probabilistic semantics. Artificial Intelligence. 221, 46–72. mla: Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” Artificial Intelligence, vol. 221, Elsevier, 2015, pp. 46–72, doi:10.1016/j.artint.2014.12.009. short: K. Chatterjee, M. Chmelik, Artificial Intelligence 221 (2015) 46–72. date_created: 2018-12-11T11:54:28Z date_published: 2015-04-01T00:00:00Z date_updated: 2021-01-12T06:53:46Z day: '01' department: - _id: KrCh doi: 10.1016/j.artint.2014.12.009 external_id: arxiv: - '1408.2058' intvolume: ' 221' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1408.2058 month: '04' oa: 1 oa_version: Preprint page: 46 - 72 publication: Artificial Intelligence publication_status: published publisher: Elsevier publist_id: '5224' quality_controlled: '1' scopus_import: 1 status: public title: POMDPs under probabilistic semantics type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 221 year: '2015' ... --- _id: '5443' abstract: - lang: eng text: POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Jessica full_name: Davies, Jessica id: 378E0060-F248-11E8-B48F-1D18A9856A87 last_name: Davies citation: ama: Chatterjee K, Chmelik M, Davies J. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1 apa: Chatterjee, K., Chmelik, M., & Davies, J. (2015). A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1 chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1. ieee: K. Chatterjee, M. Chmelik, and J. Davies, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria, 2015. ista: Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, IST Austria, 23p. mla: Chatterjee, Krishnendu, et al. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1. short: K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015. date_created: 2018-12-12T11:39:22Z date_published: 2015-11-06T00:00:00Z date_updated: 2023-02-21T16:24:05Z day: '06' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2015-325-v2-1 file: - access_level: open_access checksum: f0fa31ad8161ed655137e94012123ef9 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:05Z date_updated: 2020-07-14T12:46:57Z file_id: '5466' file_name: IST-2015-325-v2+1_main.pdf file_size: 412379 relation: main_file file_date_updated: 2020-07-14T12:46:57Z has_accepted_license: '1' language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: '23' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '362' related_material: record: - id: '1166' relation: later_version status: public status: public title: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1501' abstract: - lang: eng text: 'We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ' acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca citation: ama: Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 2015;47(2):230-264. doi:10.1007/s10703-015-0235-2 apa: Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2 chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2. ieee: K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” Formal Methods in System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015. ista: Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264. mla: Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2. short: K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264. date_created: 2018-12-11T11:52:23Z date_published: 2015-10-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/s10703-015-0235-2 ec_funded: 1 intvolume: ' 47' issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1405.0835 month: '10' oa: 1 oa_version: Preprint page: 230 - 264 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '5677' quality_controlled: '1' related_material: record: - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: CEGAR for compositional analysis of qualitative properties in Markov decision processes type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 47 year: '2015' ... --- _id: '1603' abstract: - lang: eng text: "For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour." acknowledgement: This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734. alternative_title: - LNCS author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Andreas full_name: Fellner, Andreas id: 42BABFB4-F248-11E8-B48F-1D18A9856A87 last_name: Fellner - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10. ieee: 'T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.' ista: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.' mla: Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10. short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177. conference: end_date: 2015-07-24 location: San Francisco, CA, United States name: 'CAV: Computer Aided Verification' start_date: 2015-07-18 date_created: 2018-12-11T11:52:58Z date_published: 2015-07-16T00:00:00Z date_updated: 2024-02-21T13:52:07Z day: '16' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-21690-4_10 ec_funded: 1 intvolume: ' 9206' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1502.02834 month: '07' oa: 1 oa_version: Preprint page: 158 - 177 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_identifier: eisbn: - 978-3-319-21690-4 publication_status: published publisher: Springer publist_id: '5564' quality_controlled: '1' related_material: record: - id: '5549' relation: research_paper status: public scopus_import: 1 status: public title: Counterexample explanation by learning small strategies in Markov decision processes type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 9206 year: '2015' ... --- _id: '1733' abstract: - lang: eng text: The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies. author: - first_name: Pavol full_name: Cerny, Pavol last_name: Cerny - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Arjun full_name: Radhakrishna, Arjun id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87 last_name: Radhakrishna citation: ama: Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. Theoretical Computer Science. 2014;560(3):348-363. doi:10.1016/j.tcs.2014.08.019 apa: Cerny, P., Chmelik, M., Henzinger, T. A., & Radhakrishna, A. (2014). Interface simulation distances. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2014.08.019 chicago: Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2014.08.019. ieee: P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” Theoretical Computer Science, vol. 560, no. 3. Elsevier, pp. 348–363, 2014. ista: Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363. mla: Cerny, Pavol, et al. “Interface Simulation Distances.” Theoretical Computer Science, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:10.1016/j.tcs.2014.08.019. short: P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363. date_created: 2018-12-11T11:53:43Z date_published: 2014-12-04T00:00:00Z date_updated: 2023-02-23T11:04:00Z day: '04' department: - _id: ToHe - _id: KrCh doi: 10.1016/j.tcs.2014.08.019 ec_funded: 1 intvolume: ' 560' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1210.2450 month: '12' oa: 1 oa_version: Submitted Version page: 348 - 363 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Theoretical Computer Science publication_status: published publisher: Elsevier publist_id: '5392' quality_controlled: '1' related_material: record: - id: '2916' relation: earlier_version status: public scopus_import: 1 status: public title: Interface simulation distances type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 560 year: '2014' ... --- _id: '2027' abstract: - lang: eng text: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples. acknowledgement: This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1. alternative_title: - LNCS author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Marta full_name: Kwiatkowska, Marta last_name: Kwiatkowska - first_name: David full_name: Parker, David last_name: Parker - first_name: Mateusz full_name: Ujma, Mateusz last_name: Ujma citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8. ieee: T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114. ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.' mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8. short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ALENEX: Algorithm Engineering and Experiments' start_date: 2014-11-03 date_created: 2018-12-11T11:55:17Z date_published: 2014-11-01T00:00:00Z date_updated: 2021-01-12T06:54:49Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-11936-6_8 ec_funded: 1 editor: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin intvolume: ' 8837' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.2967 month: '11' oa: 1 oa_version: Submitted Version page: 98 - 114 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 26241A12-B435-11E9-9278-68D0E5697425 grant_number: '24696' name: LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ' Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)' publication_status: published publisher: Society of Industrial and Applied Mathematics publist_id: '5046' quality_controlled: '1' status: public title: Verification of markov decision processes using learning algorithms type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2063' abstract: - lang: eng text: We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca citation: ama: 'Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31' apa: 'Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31' chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31. ieee: 'K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.' ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.' mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31. short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490. conference: end_date: 2014-07-22 location: Vienna, Austria name: 'CAV: Computer Aided Verification' start_date: 2014-07-18 date_created: 2018-12-11T11:55:30Z date_published: 2014-07-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-08867-9_31 ec_funded: 1 intvolume: ' 8559' language: - iso: eng month: '07' oa_version: None page: 473 - 490 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '4978' quality_controlled: '1' related_material: record: - id: '5412' relation: earlier_version status: public - id: '5413' relation: earlier_version status: public - id: '5414' relation: earlier_version status: public - id: '1155' relation: dissertation_contains status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ...