[{"month":"06","conference":{"location":"Austin, TX, USA","start_date":"2015-01-25","end_date":"2015-01-30","name":"IAAI: Innovative Applications of Artificial Intelligence"},"language":[{"iso":"eng"}],"external_id":{"arxiv":["1411.3880"]},"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1411.3880","open_access":"1"}],"quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"publist_id":"5286","ec_funded":1,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"first_name":"Raghav","last_name":"Gupta","full_name":"Gupta, Raghav"},{"last_name":"Kanodia","first_name":"Ayush","full_name":"Kanodia, Ayush"}],"related_material":{"record":[{"id":"1529","status":"public","relation":"later_version"}]},"date_created":"2018-12-11T11:54:11Z","date_updated":"2023-02-23T10:02:57Z","volume":5,"year":"2015","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.","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"AAAI Press","day":"01","scopus_import":1,"date_published":"2015-06-01T00:00:00Z","publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ","citation":{"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.","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.","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.","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.","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.","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."},"page":"3496-3502","abstract":[{"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.","lang":"eng"}],"type":"conference","alternative_title":["Artifical Intelligence"],"oa_version":"Preprint","_id":"1820","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Optimal cost almost-sure reachability in POMDPs","intvolume":" 5"},{"day":"01","scopus_import":1,"date_published":"2015-01-01T00:00:00Z","citation":{"chicago":"Bloem, Roderick, Krishnendu Chatterjee, Swen Jacobs, and Robert Könighofer. “Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information,” 9035:517–32. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_50.","short":"R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532.","mla":"Bloem, Roderick, et al. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information. Vol. 9035, Springer, 2015, pp. 517–32, doi:10.1007/978-3-662-46681-0_50.","apa":"Bloem, R., Chatterjee, K., Jacobs, S., & Könighofer, R. (2015). Assume-guarantee synthesis for concurrent reactive programs with partial information (Vol. 9035, pp. 517–532). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_50","ieee":"R. Bloem, K. Chatterjee, S. Jacobs, and R. Könighofer, “Assume-guarantee synthesis for concurrent reactive programs with partial information,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom, 2015, vol. 9035, pp. 517–532.","ista":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. 2015. Assume-guarantee synthesis for concurrent reactive programs with partial information. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9035, 517–532.","ama":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Vol 9035. Springer; 2015:517-532. doi:10.1007/978-3-662-46681-0_50"},"page":"517 - 532","abstract":[{"lang":"eng","text":"Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize.We resolve this shortcoming by defining AGS under partial information. We analyze the complexity and decidability in different settings, showing that the problem has a high worstcase complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","_id":"1838","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Assume-guarantee synthesis for concurrent reactive programs with partial information","intvolume":" 9035","month":"01","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2015-04-18","start_date":"2015-04-11","location":"London, United Kingdom"},"doi":"10.1007/978-3-662-46681-0_50","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1411.4604"}],"oa":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"publist_id":"5264","ec_funded":1,"author":[{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"last_name":"Jacobs","first_name":"Swen","full_name":"Jacobs, Swen"},{"first_name":"Robert","last_name":"Könighofer","full_name":"Könighofer, Robert"}],"date_created":"2018-12-11T11:54:17Z","date_updated":"2021-01-12T06:53:32Z","volume":9035,"acknowledgement":"This work was supported by the Austrian Science Fund (FWF) through the research network RiSE (S11406-N23, S11407-N23) and grant nr. P23499-N23, by the European Commission through an ERC Start grant (279307: Graph Games) and project STANCE (317753), as well as by the German Research Foundation (DFG) through SFB/TR 14 AVACS and project ASDPS(JA 2357/2-1).","year":"2015","publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"}]},{"month":"01","doi":"10.1007/978-3-662-46681-0_12","conference":{"location":"London, United Kingdom","start_date":"2015-04-11","end_date":"2015-04-18","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1501.03093"}],"oa":1,"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"quality_controlled":"1","publist_id":"5263","ec_funded":1,"author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"}],"volume":9035,"date_created":"2018-12-11T11:54:18Z","date_updated":"2020-01-21T13:18:52Z","year":"2015","department":[{"_id":"KrCh"}],"publisher":"Springer","publication_status":"published","day":"01","series_title":"Lecture Notes in Computer Science","date_published":"2015-01-01T00:00:00Z","citation":{"ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2015. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 9035, 181–187.","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives,” vol. 9035. Springer, pp. 181–187, 2015.","apa":"Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2015). Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_12","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 2015;9035:181-187. doi:10.1007/978-3-662-46681-0_12","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_12.","mla":"Brázdil, Tomáš, et al. Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. Vol. 9035, Springer, 2015, pp. 181–87, doi:10.1007/978-3-662-46681-0_12.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187."},"page":"181 - 187","abstract":[{"lang":"eng","text":"We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","_id":"1839","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 9035","status":"public","title":"Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives"},{"oa":1,"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"doi":"10.1007/s00236-015-0215-4","language":[{"iso":"eng"}],"month":"04","year":"2015","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Springer","author":[{"full_name":"Beneš, Nikola","last_name":"Beneš","first_name":"Nikola"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"},{"last_name":"Larsen","first_name":"Kim","full_name":"Larsen, Kim"},{"full_name":"Möller, Mikael","first_name":"Mikael","last_name":"Möller"},{"full_name":"Sickert, Salomon","last_name":"Sickert","first_name":"Salomon"},{"last_name":"Srba","first_name":"Jiří","full_name":"Srba, Jiří"}],"date_created":"2018-12-11T11:54:20Z","date_updated":"2021-01-12T06:53:35Z","volume":52,"file_date_updated":"2020-07-14T12:45:19Z","publist_id":"5255","ec_funded":1,"publication":"Acta Informatica","citation":{"chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” Acta Informatica, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba, J. (2015). Refinement checking on parametric modal transition systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297. doi:10.1007/s00236-015-0215-4"},"article_type":"original","page":"269 - 297","date_published":"2015-04-01T00:00:00Z","scopus_import":1,"day":"01","article_processing_charge":"No","has_accepted_license":"1","_id":"1846","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Refinement checking on parametric modal transition systems","ddc":["000"],"status":"public","intvolume":" 52","oa_version":"Submitted Version","file":[{"file_name":"2015_ActaInfo_Benes.pdf","access_level":"open_access","content_type":"application/pdf","file_size":488482,"creator":"dernst","relation":"main_file","file_id":"7854","date_created":"2020-05-15T08:57:44Z","date_updated":"2020-07-14T12:45:19Z","checksum":"fb4037ddc4fc05f33080dd3547ede350"}],"type":"journal_article","abstract":[{"lang":"eng","text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS."}],"issue":"2-3"},{"title":"Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating","status":"public","ddc":["570"],"intvolume":" 69","_id":"1851","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2020-05-15T09:05:34Z","date_updated":"2020-07-14T12:45:19Z","checksum":"1e8be0b1d7598a78cd2623d8ee8e7798","relation":"main_file","file_id":"7855","file_size":967214,"content_type":"application/pdf","creator":"dernst","file_name":"2015_Evolution_Priklopil.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","type":"journal_article","abstract":[{"lang":"eng","text":"We consider mating strategies for females who search for males sequentially during a season of limited length. We show that the best strategy rejects a given male type if encountered before a time-threshold but accepts him after. For frequency-independent benefits, we obtain the optimal time-thresholds explicitly for both discrete and continuous distributions of males, and allow for mistakes being made in assessing the correct male type. When the benefits are indirect (genes for the offspring) and the population is under frequency-dependent ecological selection, the benefits depend on the mating strategy of other females as well. This case is particularly relevant to speciation models that seek to explore the stability of reproductive isolation by assortative mating under frequency-dependent ecological selection. We show that the indirect benefits are to be quantified by the reproductive values of couples, and describe how the evolutionarily stable time-thresholds can be found. We conclude with an example based on the Levene model, in which we analyze the evolutionarily stable assortative mating strategies and the strength of reproductive isolation provided by them."}],"issue":"4","article_type":"original","page":"1015 - 1026","publication":"Evolution","citation":{"short":"T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.","mla":"Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” Evolution, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:10.1111/evo.12618.","chicago":"Priklopil, Tadeas, Eva Kisdi, and Mats Gyllenberg. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” Evolution. Wiley, 2015. https://doi.org/10.1111/evo.12618.","ama":"Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. 2015;69(4):1015-1026. doi:10.1111/evo.12618","ieee":"T. Priklopil, E. Kisdi, and M. Gyllenberg, “Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating,” Evolution, vol. 69, no. 4. Wiley, pp. 1015–1026, 2015.","apa":"Priklopil, T., Kisdi, E., & Gyllenberg, M. (2015). Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. Wiley. https://doi.org/10.1111/evo.12618","ista":"Priklopil T, Kisdi E, Gyllenberg M. 2015. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. 69(4), 1015–1026."},"date_published":"2015-02-09T00:00:00Z","scopus_import":"1","day":"09","has_accepted_license":"1","article_processing_charge":"No","publication_status":"published","publisher":"Wiley","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"year":"2015","pmid":1,"date_updated":"2022-06-07T10:52:37Z","date_created":"2018-12-11T11:54:21Z","volume":69,"author":[{"first_name":"Tadeas","last_name":"Priklopil","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","full_name":"Priklopil, Tadeas"},{"first_name":"Eva","last_name":"Kisdi","full_name":"Kisdi, Eva"},{"last_name":"Gyllenberg","first_name":"Mats","full_name":"Gyllenberg, Mats"}],"file_date_updated":"2020-07-14T12:45:19Z","ec_funded":1,"publist_id":"5249","quality_controlled":"1","project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"oa":1,"external_id":{"pmid":["25662095"]},"language":[{"iso":"eng"}],"doi":"10.1111/evo.12618","month":"02","publication_identifier":{"eissn":["1558-5646"],"issn":["0014-3820"]}}]