[{"_id":"1667","date_published":"2015-08-22T00:00:00Z","abstract":[{"text":"We consider parametric version of fixed-delay continuoustime Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay transitions are specified by parameters, rather than concrete values. Our goal is to synthesize values of these parameters that, for a given cost function, minimise expected total cost incurred before reaching a given set of target states. We show that under mild assumptions, optimal values of parameters can be effectively approximated using translation to a Markov decision process (MDP) whose actions correspond to discretized values of these parameters. To this end we identify and overcome several interesting phenomena arising in systems with fixed delays.","lang":"eng"}],"volume":9259,"publication_status":"published","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1407.4777"}],"oa":1,"publist_id":"5482","oa_version":"Preprint","year":"2015","date_updated":"2021-01-12T06:52:24Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"month":"08","date_created":"2018-12-11T11:53:22Z","series_title":"Lecture Notes in Computer Science","page":"141 - 159","department":[{"_id":"KrCh"}],"quality_controlled":"1","status":"public","intvolume":"      9259","publisher":"Springer","day":"22","alternative_title":["LNCS"],"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"last_name":"Korenčiak","first_name":"L'Uboš","full_name":"Korenčiak, L'Uboš"},{"first_name":"Jan","full_name":"Krčál, Jan","last_name":"Krčál"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Řehák","first_name":"Vojtěch","full_name":"Řehák, Vojtěch"}],"type":"conference","ec_funded":1,"citation":{"short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.","apa":"Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., &#38; Řehák, V. (2015). Optimizing performance of continuous-time stochastic systems using timeout synthesis. Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>","ama":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159. doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>","ista":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.","ieee":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing performance of continuous-time stochastic systems using timeout synthesis,” vol. 9259. Springer, pp. 141–159, 2015.","chicago":"Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>.","mla":"Brázdil, Tomáš, et al. <i>Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis</i>. Vol. 9259, Springer, 2015, pp. 141–59, doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>."},"conference":{"location":"Madrid, Spain","end_date":"2015-09-03","start_date":"2015-09-01","name":"QEST: Quantitative Evaluation of Systems"},"title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-22264-6_10","acknowledgement":"The research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation, grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}]},{"file":[{"relation":"main_file","file_id":"6342","content_type":"application/pdf","date_created":"2019-04-18T12:39:56Z","creator":"kschuh","file_size":391466,"file_name":"2015_rspa_Adlam.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:11Z","checksum":"e613d94d283c776322403a28aad11bdd"}],"article_number":"20150114","date_published":"2015-09-08T00:00:00Z","_id":"1673","abstract":[{"text":"When a new mutant arises in a population, there is a probability it outcompetes the residents and fixes. The structure of the population can affect this fixation probability. Suppressing population structures reduce the difference between two competing variants, while amplifying population structures enhance the difference. Suppressors are ubiquitous and easy to construct, but amplifiers for the large population limit are more elusive and only a few examples have been discovered. Whether or not a population structure is an amplifier of selection depends on the probability distribution for the placement of the invading mutant. First, we prove that there exist only bounded amplifiers for adversarial placement-that is, for arbitrary initial conditions. Next, we show that the Star population structure, which is known to amplify for mutants placed uniformly at random, does not amplify for mutants that arise through reproduction and are therefore placed proportional to the temperatures of the vertices. Finally, we construct population structures that amplify for all mutational events that arise through reproduction, uniformly at random, or through some combination of the two. ","lang":"eng"}],"issue":"2181","file_date_updated":"2020-07-14T12:45:11Z","volume":471,"publication_status":"published","oa":1,"publist_id":"5477","has_accepted_license":"1","year":"2015","oa_version":"Published Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:52:26Z","scopus_import":1,"month":"09","date_created":"2018-12-11T11:53:24Z","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","intvolume":"       471","status":"public","publisher":"Royal Society of London","day":"08","author":[{"last_name":"Adlam","first_name":"Ben","full_name":"Adlam, Ben"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"type":"journal_article","ec_funded":1,"citation":{"chicago":"Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London, 2015. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>.","ieee":"B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181. Royal Society of London, 2015.","ista":"Adlam B, Chatterjee K, Nowak M. 2015. Amplifiers of selection. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. 471(2181), 20150114.","mla":"Adlam, Ben, et al. “Amplifiers of Selection.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181, 20150114, Royal Society of London, 2015, doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>.","short":"B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015).","ama":"Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2015;471(2181). doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>","apa":"Adlam, B., Chatterjee, K., &#38; Nowak, M. (2015). Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>"},"title":"Amplifiers of selection","language":[{"iso":"eng"}],"doi":"10.1098/rspa.2015.0114","ddc":["000"],"acknowledgement":"K.C. gratefully acknowledges support from ERC Start grant no. (279307: Graph Games), Austrian Science Fund (FWF) grant no. P23499-N23, and FWF NFN grant no. S11407-N23 (RiSE). ","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}]},{"publisher":"MDPI","publication":"Games","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"quality_controlled":"1","status":"public","intvolume":"         6","page":"413 - 437","month":"09","date_created":"2018-12-11T11:53:26Z","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"language":[{"iso":"eng"}],"doi":"10.3390/g6040413","ddc":["000"],"citation":{"short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.","apa":"Priklopil, T., &#38; Chatterjee, K. (2015). Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. MDPI. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>","ama":"Priklopil T, Chatterjee K. Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. 2015;6(4):413-437. doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437.","ieee":"T. Priklopil and K. Chatterjee, “Evolution of decisions in population games with sequentially searching individuals,” <i>Games</i>, vol. 6, no. 4. MDPI, pp. 413–437, 2015.","chicago":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>. MDPI, 2015. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>.","mla":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>, vol. 6, no. 4, MDPI, 2015, pp. 413–37, doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>."},"ec_funded":1,"title":"Evolution of decisions in population games with sequentially searching individuals","day":"29","type":"journal_article","author":[{"last_name":"Priklopil","full_name":"Priklopil, Tadeas","first_name":"Tadeas","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:45:12Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"448","volume":6,"article_processing_charge":"No","issue":"4","file":[{"checksum":"912e1acbaf201100f447a43e4d5958bd","access_level":"open_access","date_updated":"2020-07-14T12:45:12Z","creator":"system","file_size":518832,"file_name":"IST-2016-448-v1+1_games-06-00413.pdf","date_created":"2018-12-12T10:12:41Z","file_id":"4959","relation":"main_file","content_type":"application/pdf"}],"date_published":"2015-09-29T00:00:00Z","_id":"1681","abstract":[{"lang":"eng","text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game."}],"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-10-17T11:42:52Z","publication_identifier":{"eissn":["2073-4336"]},"article_type":"original","publist_id":"5467","year":"2015","oa_version":"Published Version","has_accepted_license":"1"},{"doi":"10.1145/2728606.2728608","language":[{"iso":"eng"}],"date_updated":"2023-09-20T09:43:09Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"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","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"related_material":{"record":[{"relation":"later_version","id":"1407","status":"public"}]},"oa_version":"Preprint","year":"2015","type":"conference","author":[{"full_name":"Svoreňová, Mária","first_name":"Mária","last_name":"Svoreňová"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Cěrná","full_name":"Cěrná, Ivana","first_name":"Ivana"},{"last_name":"Belta","first_name":"Cǎlin","full_name":"Belta, Cǎlin"}],"publist_id":"5456","day":"14","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2015-04-16","start_date":"2015-04-14","location":"Seattle, WA, United States"},"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","ec_funded":1,"citation":{"apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 259–268). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>","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: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:259-268. doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>","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.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 259–68, doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>.","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 <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 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.","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 <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 259–68. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>."},"status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"oa":1,"publisher":"ACM","publication_status":"published","abstract":[{"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.","lang":"eng"}],"_id":"1689","date_created":"2018-12-11T11:53:29Z","date_published":"2015-04-14T00:00:00Z","month":"04","page":"259 - 268"},{"page":"233 - 238","month":"04","abstract":[{"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.","lang":"eng"}],"_id":"1691","date_created":"2018-12-11T11:53:29Z","date_published":"2015-04-14T00:00:00Z","publication_status":"published","publisher":"ACM","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","department":[{"_id":"KrCh"}],"status":"public","citation":{"ieee":"M. Svoreňová <i>et al.</i>, “Temporal logic motion planning using POMDPs with parity objectives: Case study paper,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 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.","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 <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 233–38. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728617\">https://doi.org/10.1145/2728606.2728617</a>.","mla":"Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 233–38, doi:<a href=\"https://doi.org/10.1145/2728606.2728617\">10.1145/2728606.2728617</a>.","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.","apa":"Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 233–238). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728617\">https://doi.org/10.1145/2728606.2728617</a>","ama":"Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:233-238. doi:<a href=\"https://doi.org/10.1145/2728606.2728617\">10.1145/2728606.2728617</a>"},"ec_funded":1,"title":"Temporal logic motion planning using POMDPs with parity objectives: Case study paper","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2015-04-16","start_date":"2015-04-14","location":"Seattle, WA, United States"},"day":"14","publist_id":"5453","author":[{"first_name":"Mária","full_name":"Svoreňová, Mária","last_name":"Svoreňová"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Leahy, Kevin","first_name":"Kevin","last_name":"Leahy"},{"last_name":"Eniser","full_name":"Eniser, Hasan","first_name":"Hasan"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Ivana","full_name":"Cěrná, Ivana","last_name":"Cěrná"},{"last_name":"Belta","first_name":"Cǎlin","full_name":"Belta, Cǎlin"}],"type":"conference","year":"2015","oa_version":"None","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"scopus_import":1,"date_updated":"2021-01-12T06:52:33Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/2728606.2728617"},{"issue":"9","page":"2291 - 2306","_id":"1694","date_published":"2015-02-24T00:00:00Z","date_created":"2018-12-11T11:53:30Z","abstract":[{"text":"\r\nWe introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.\r\n","lang":"eng"}],"month":"02","publication_status":"published","publisher":"IEEE","intvolume":"        60","status":"public","volume":60,"publication":"IEEE Transactions on Automatic Control","department":[{"_id":"KrCh"}],"quality_controlled":"1","title":"Quantitative temporal simulation and refinement distances for timed systems","citation":{"chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>.","ista":"Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.","ieee":"K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement distances for timed systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9. IEEE, pp. 2291–2306, 2015.","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>.","short":"K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.","ama":"Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. 2015;60(9):2291-2306. doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>","apa":"Chatterjee, K., &#38; Prabhu, V. (2015). Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>"},"ec_funded":1,"type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"oa_version":"None","year":"2015","publist_id":"5450","day":"24","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1109/TAC.2015.2404612","scopus_import":1,"date_updated":"2021-01-12T06:52:34Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"publisher":"Elsevier","intvolume":"       241","status":"public","publication":"Information and Computation","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","page":"177 - 196","date_created":"2018-12-11T11:53:32Z","month":"04","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148), ERC Start grant (279499: inVEST).","doi":"10.1016/j.ic.2015.03.001","language":[{"iso":"eng"}],"title":"The complexity of multi-mean-payoff and multi-energy games","citation":{"short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. 2015;241(4):177-196. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &#38; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>","chicago":"Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger, Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>.","ista":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 241(4), 177–196.","ieee":"Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J. Raskin, “The complexity of multi-mean-payoff and multi-energy games,” <i>Information and Computation</i>, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.","mla":"Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>, vol. 241, no. 4, Elsevier, 2015, pp. 177–96, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>."},"ec_funded":1,"type":"journal_article","author":[{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Alexander","full_name":"Rabinovich, Alexander","last_name":"Rabinovich"},{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean"}],"day":"01","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1209.3234"}],"oa":1,"publication_status":"published","volume":241,"issue":"4","_id":"1698","date_published":"2015-04-01T00:00:00Z","abstract":[{"lang":"eng","text":"In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete."}],"scopus_import":1,"date_updated":"2021-01-12T06:52:36Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015","oa_version":"Preprint","publist_id":"5443"},{"day":"15","author":[{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353","full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter"},{"last_name":"Kanodia","first_name":"Ayush","full_name":"Kanodia, Ayush"},{"full_name":"Gupta, Raghav","first_name":"Raghav","last_name":"Gupta"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"type":"journal_article","citation":{"mla":"Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812, Royal Society, 2015, doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>.","ieee":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological auctions with multiple rewards,” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812. Royal Society, 2015.","ista":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 282(1812).","chicago":"Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu Chatterjee. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society, 2015. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>.","apa":"Reiter, J., Kanodia, A., Gupta, R., Nowak, M., &#38; Chatterjee, K. (2015). Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>","ama":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. 2015;282(1812). doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>","short":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015)."},"title":"Biological auctions with multiple rewards","language":[{"iso":"eng"}],"doi":"10.1098/rspb.2015.1041","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1400"}]},"pmid":1,"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This work was supported by grants from the John Templeton Foundation, ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE), FWF Grant (No P23499N23) and a Microsoft faculty fellows award.","month":"07","date_created":"2018-12-11T11:53:35Z","publication":"Proceedings of the Royal Society of London Series B Biological Sciences","department":[{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"       282","status":"public","publisher":"Royal Society","article_type":"original","publist_id":"5425","oa_version":"Submitted Version","year":"2015","external_id":{"pmid":["26180069"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:40:43Z","_id":"1709","abstract":[{"lang":"eng","text":"The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards."}],"date_published":"2015-07-15T00:00:00Z","article_processing_charge":"No","issue":"1812","volume":282,"publication_status":"published","main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/","open_access":"1"}],"oa":1},{"month":"01","date_created":"2018-12-11T11:53:37Z","page":"118 - 127","publication":"Real-Time Systems Symposium","department":[{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"      2015","status":"public","publisher":"IEEE","day":"15","type":"conference","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"first_name":"Alexander","full_name":"Kößler, Alexander","last_name":"Kößler"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"}],"citation":{"short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems Symposium, IEEE, 2015, pp. 118–127.","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In: <i>Real-Time Systems Symposium</i>. Vol 2015. IEEE; 2015:118-127. doi:<a href=\"https://doi.org/10.1109/RTSS.2014.9\">10.1109/RTSS.2014.9</a>","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., &#38; Schmid, U. (2015). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In <i>Real-Time Systems Symposium</i> (Vol. 2015, pp. 118–127). Rome, Italy: IEEE. <a href=\"https://doi.org/10.1109/RTSS.2014.9\">https://doi.org/10.1109/RTSS.2014.9</a>","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” In <i>Real-Time Systems Symposium</i>, 2015:118–27. IEEE, 2015. <a href=\"https://doi.org/10.1109/RTSS.2014.9\">https://doi.org/10.1109/RTSS.2014.9</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks,” in <i>Real-Time Systems Symposium</i>, Rome, Italy, 2015, vol. 2015, no. January, pp. 118–127.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127.","mla":"Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” <i>Real-Time Systems Symposium</i>, vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:<a href=\"https://doi.org/10.1109/RTSS.2014.9\">10.1109/RTSS.2014.9</a>."},"title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","conference":{"start_date":"2014-12-02","end_date":"2014-12-05","name":"RTSS: Real-Time Systems Symposium","location":"Rome, Italy"},"language":[{"iso":"eng"}],"doi":"10.1109/RTSS.2014.9","related_material":{"record":[{"status":"public","id":"5423","relation":"earlier_version"},{"relation":"dissertation_contains","id":"821","status":"public"}]},"_id":"1714","abstract":[{"text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.","lang":"eng"}],"date_published":"2015-01-15T00:00:00Z","article_processing_charge":"No","issue":"January","volume":2015,"publication_status":"published","publist_id":"5417","oa_version":"None","year":"2015","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T12:01:59Z"},{"publication":"Information and Computation","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","intvolume":"       245","status":"public","publisher":"Elsevier","month":"12","date_created":"2018-12-11T11:53:42Z","page":"3 - 16","language":[{"iso":"eng"}],"doi":"10.1016/j.ic.2015.06.003","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3856"}]},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","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"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"day":"01","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"last_name":"Gimbert","full_name":"Gimbert, Hugo","first_name":"Hugo"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"type":"journal_article","citation":{"ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” <i>Information and Computation</i>, vol. 245, no. 12. Elsevier, pp. 3–16, 2015.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>.","mla":"Chatterjee, Krishnendu, et al. “Randomness for Free.” <i>Information and Computation</i>, vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>.","short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2015). Randomness for free. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>","ama":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. <i>Information and Computation</i>. 2015;245(12):3-16. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>"},"ec_funded":1,"title":"Randomness for free","volume":245,"publication_status":"published","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1006.0673"}],"oa":1,"_id":"1731","abstract":[{"text":"We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (both players interact simultaneously); and (b) turn-based (both players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. In this work we present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. ","lang":"eng"}],"date_published":"2015-12-01T00:00:00Z","issue":"12","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T11:45:42Z","publist_id":"5395","oa_version":"Preprint","year":"2015"},{"ec_funded":1,"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:<a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">10.1109/ICRA.2015.7139019</a>","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; 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. <a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">https://doi.org/10.1109/ICRA.2015.7139019</a>","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, IEEE, 2015, pp. 325–330.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IEEE, 2015, pp. 325–30, doi:<a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">10.1109/ICRA.2015.7139019</a>.","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. <a href=\"https://doi.org/10.1109/ICRA.2015.7139019\">https://doi.org/10.1109/ICRA.2015.7139019</a>.","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.","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."},"conference":{"start_date":"2015-05-26","end_date":"2015-05-30","name":"ICRA: International Conference on Robotics and Automation","location":"Seattle, WA, United States"},"title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","day":"01","type":"conference","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"last_name":"Gupta","full_name":"Gupta, Raghav","first_name":"Raghav"},{"last_name":"Kanodia","full_name":"Kanodia, Ayush","first_name":"Ayush"}],"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"related_material":{"record":[{"status":"public","id":"5424","relation":"earlier_version"},{"id":"5426","relation":"earlier_version","status":"public"}]},"language":[{"iso":"eng"}],"doi":"10.1109/ICRA.2015.7139019","page":"325 - 330","month":"01","date_created":"2018-12-11T11:53:43Z","publisher":"IEEE","quality_controlled":"1","department":[{"_id":"KrCh"}],"status":"public","publist_id":"5394","year":"2015","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:25:52Z","scopus_import":1,"external_id":{"arxiv":["1409.3360"]},"arxiv":1,"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."}],"_id":"1732","date_published":"2015-01-01T00:00:00Z","publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1409.3360","open_access":"1"}],"oa":1},{"publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ","department":[{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"         5","status":"public","publisher":"AAAI Press","month":"06","date_created":"2018-12-11T11:54:11Z","page":"3496-3502","language":[{"iso":"eng"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"1529"}]},"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.","day":"01","type":"conference","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Raghav","full_name":"Gupta, Raghav","last_name":"Gupta"},{"full_name":"Kanodia, Ayush","first_name":"Ayush","last_name":"Kanodia"}],"alternative_title":["Artifical Intelligence"],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, vol. 5, AAAI Press, 2015, pp. 3496–502.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” in <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, 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.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>, 5:3496–3502. AAAI Press, 2015.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2015). Optimal cost almost-sure reachability in POMDPs. In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i> (Vol. 5, pp. 3496–3502). Austin, TX, USA: AAAI Press.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. In: <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence </i>. Vol 5. AAAI Press; 2015:3496-3502.","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."},"ec_funded":1,"title":"Optimal cost almost-sure reachability in POMDPs","conference":{"name":"IAAI: Innovative Applications of Artificial Intelligence","end_date":"2015-01-30","start_date":"2015-01-25","location":"Austin, TX, USA"},"volume":5,"publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1411.3880","open_access":"1"}],"oa":1,"date_published":"2015-06-01T00:00:00Z","_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."}],"arxiv":1,"external_id":{"arxiv":["1411.3880"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:02:57Z","publist_id":"5286","year":"2015","oa_version":"Preprint"},{"month":"01","date_created":"2018-12-11T11:54:17Z","page":"517 - 532","department":[{"_id":"KrCh"}],"intvolume":"      9035","status":"public","publisher":"Springer","day":"01","type":"conference","author":[{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Jacobs","first_name":"Swen","full_name":"Jacobs, Swen"},{"first_name":"Robert","full_name":"Könighofer, Robert","last_name":"Könighofer"}],"alternative_title":["LNCS"],"citation":{"mla":"Bloem, Roderick, et al. <i>Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information</i>. Vol. 9035, Springer, 2015, pp. 517–32, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">10.1007/978-3-662-46681-0_50</a>.","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.","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.","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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">https://doi.org/10.1007/978-3-662-46681-0_50</a>.","apa":"Bloem, R., Chatterjee, K., Jacobs, S., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">https://doi.org/10.1007/978-3-662-46681-0_50</a>","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:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_50\">10.1007/978-3-662-46681-0_50</a>","short":"R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532."},"ec_funded":1,"title":"Assume-guarantee synthesis for concurrent reactive programs with partial information","conference":{"start_date":"2015-04-11","end_date":"2015-04-18","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"London, United Kingdom"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-46681-0_50","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"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).","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."}],"_id":"1838","date_published":"2015-01-01T00:00:00Z","volume":9035,"publication_status":"published","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1411.4604","open_access":"1"}],"publist_id":"5264","year":"2015","oa_version":"Preprint","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:32Z"},{"date_updated":"2020-01-21T13:18:52Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","year":"2015","publist_id":"5263","volume":9035,"main_file_link":[{"url":"http://arxiv.org/abs/1501.03093","open_access":"1"}],"oa":1,"publication_status":"published","abstract":[{"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.","lang":"eng"}],"_id":"1839","date_published":"2015-01-01T00:00:00Z","doi":"10.1007/978-3-662-46681-0_12","language":[{"iso":"eng"}],"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"}],"type":"conference","alternative_title":["LNCS"],"day":"01","title":"Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives","conference":{"start_date":"2015-04-11","end_date":"2015-04-18","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"London, United Kingdom"},"citation":{"apa":"Brázdil, T., Chatterjee, K., Forejt, V., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">https://doi.org/10.1007/978-3-662-46681-0_12</a>","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:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">10.1007/978-3-662-46681-0_12</a>","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.","mla":"Brázdil, Tomáš, et al. <i>Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives</i>. Vol. 9035, Springer, 2015, pp. 181–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">10.1007/978-3-662-46681-0_12</a>.","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.","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.","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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_12\">https://doi.org/10.1007/978-3-662-46681-0_12</a>."},"ec_funded":1,"status":"public","intvolume":"      9035","quality_controlled":"1","department":[{"_id":"KrCh"}],"publisher":"Springer","date_created":"2018-12-11T11:54:18Z","series_title":"Lecture Notes in Computer Science","month":"01","page":"181 - 187"},{"page":"269 - 297","date_created":"2018-12-11T11:54:20Z","month":"04","publisher":"Springer","status":"public","intvolume":"        52","publication":"Acta Informatica","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Refinement checking on parametric modal transition systems","citation":{"ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. 2015;52(2-3):269-297. doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &#38; Srba, J. (2015). Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>.","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>.","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,” <i>Acta Informatica</i>, vol. 52, no. 2–3. Springer, pp. 269–297, 2015."},"ec_funded":1,"type":"journal_article","author":[{"last_name":"Beneš","full_name":"Beneš, Nikola","first_name":"Nikola"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Larsen, Kim","first_name":"Kim","last_name":"Larsen"},{"last_name":"Möller","full_name":"Möller, Mikael","first_name":"Mikael"},{"full_name":"Sickert, Salomon","first_name":"Salomon","last_name":"Sickert"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"day":"01","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"ddc":["000"],"doi":"10.1007/s00236-015-0215-4","language":[{"iso":"eng"}],"article_processing_charge":"No","issue":"2-3","_id":"1846","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."}],"date_published":"2015-04-01T00:00:00Z","file":[{"checksum":"fb4037ddc4fc05f33080dd3547ede350","date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","file_name":"2015_ActaInfo_Benes.pdf","creator":"dernst","file_size":488482,"date_created":"2020-05-15T08:57:44Z","content_type":"application/pdf","file_id":"7854","relation":"main_file"}],"oa":1,"publication_status":"published","volume":52,"file_date_updated":"2020-07-14T12:45:19Z","year":"2015","has_accepted_license":"1","oa_version":"Submitted Version","article_type":"original","publist_id":"5255","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:35Z"},{"month":"02","date_created":"2018-12-11T11:54:21Z","page":"1015 - 1026","quality_controlled":"1","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"publication":"Evolution","status":"public","intvolume":"        69","publisher":"Wiley","day":"09","type":"journal_article","author":[{"id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","last_name":"Priklopil","full_name":"Priklopil, Tadeas","first_name":"Tadeas"},{"full_name":"Kisdi, Eva","first_name":"Eva","last_name":"Kisdi"},{"full_name":"Gyllenberg, Mats","first_name":"Mats","last_name":"Gyllenberg"}],"ec_funded":1,"citation":{"short":"T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.","apa":"Priklopil, T., Kisdi, E., &#38; Gyllenberg, M. (2015). Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. <i>Evolution</i>. Wiley. <a href=\"https://doi.org/10.1111/evo.12618\">https://doi.org/10.1111/evo.12618</a>","ama":"Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. <i>Evolution</i>. 2015;69(4):1015-1026. doi:<a href=\"https://doi.org/10.1111/evo.12618\">10.1111/evo.12618</a>","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.","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,” <i>Evolution</i>, vol. 69, no. 4. Wiley, pp. 1015–1026, 2015.","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.” <i>Evolution</i>. Wiley, 2015. <a href=\"https://doi.org/10.1111/evo.12618\">https://doi.org/10.1111/evo.12618</a>.","mla":"Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” <i>Evolution</i>, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:<a href=\"https://doi.org/10.1111/evo.12618\">10.1111/evo.12618</a>."},"title":"Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating","language":[{"iso":"eng"}],"doi":"10.1111/evo.12618","ddc":["570"],"pmid":1,"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"file":[{"date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","checksum":"1e8be0b1d7598a78cd2623d8ee8e7798","file_name":"2015_Evolution_Priklopil.pdf","file_size":967214,"creator":"dernst","date_created":"2020-05-15T09:05:34Z","content_type":"application/pdf","file_id":"7855","relation":"main_file"}],"abstract":[{"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.","lang":"eng"}],"_id":"1851","date_published":"2015-02-09T00:00:00Z","issue":"4","article_processing_charge":"No","file_date_updated":"2020-07-14T12:45:19Z","volume":69,"publication_status":"published","oa":1,"publist_id":"5249","article_type":"original","year":"2015","oa_version":"Submitted Version","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2022-06-07T10:52:37Z","scopus_import":"1","external_id":{"pmid":["25662095"]},"publication_identifier":{"eissn":["1558-5646"],"issn":["0014-3820"]}},{"issue":"1","abstract":[{"text":"The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.","lang":"eng"}],"_id":"1856","date_published":"2015-02-01T00:00:00Z","article_number":"9","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1004.0739"}],"oa":1,"publication_status":"published","volume":62,"year":"2015","oa_version":"Preprint","publist_id":"5244","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T11:46:04Z","date_created":"2018-12-11T11:54:23Z","month":"02","publisher":"ACM","intvolume":"        62","status":"public","publication":"Journal of the ACM","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Measuring and synthesizing systems in probabilistic environments","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 62(1), 9.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” <i>Journal of the ACM</i>, vol. 62, no. 1. ACM, 2015.","mla":"Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>, vol. 62, no. 1, 9, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>.","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015).","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. 2015;62(1). doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>"},"ec_funded":1,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"},{"first_name":"Rohit","full_name":"Singh, Rohit","last_name":"Singh"}],"type":"journal_article","day":"01","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"related_material":{"record":[{"id":"3864","relation":"earlier_version","status":"public"}]},"doi":"10.1145/2699430","language":[{"iso":"eng"}]},{"type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"}],"day":"01","title":"POMDPs under probabilistic semantics","citation":{"short":"K. Chatterjee, M. Chmelik, Artificial Intelligence 221 (2015) 46–72.","ama":"Chatterjee K, Chmelik M. POMDPs under probabilistic semantics. <i>Artificial Intelligence</i>. 2015;221:46-72. doi:<a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">10.1016/j.artint.2014.12.009</a>","apa":"Chatterjee, K., &#38; Chmelik, M. (2015). POMDPs under probabilistic semantics. <i>Artificial Intelligence</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">https://doi.org/10.1016/j.artint.2014.12.009</a>","chicago":"Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” <i>Artificial Intelligence</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">https://doi.org/10.1016/j.artint.2014.12.009</a>.","ista":"Chatterjee K, Chmelik M. 2015. POMDPs under probabilistic semantics. Artificial Intelligence. 221, 46–72.","ieee":"K. Chatterjee and M. Chmelik, “POMDPs under probabilistic semantics,” <i>Artificial Intelligence</i>, vol. 221. Elsevier, pp. 46–72, 2015.","mla":"Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” <i>Artificial Intelligence</i>, vol. 221, Elsevier, 2015, pp. 46–72, doi:<a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">10.1016/j.artint.2014.12.009</a>."},"doi":"10.1016/j.artint.2014.12.009","language":[{"iso":"eng"}],"date_created":"2018-12-11T11:54:28Z","month":"04","page":"46 - 72","status":"public","intvolume":"       221","publication":"Artificial Intelligence","department":[{"_id":"KrCh"}],"quality_controlled":"1","publisher":"Elsevier","year":"2015","oa_version":"Preprint","publist_id":"5224","external_id":{"arxiv":["1408.2058"]},"scopus_import":1,"date_updated":"2021-01-12T06:53:46Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1873","date_published":"2015-04-01T00:00:00Z","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,"volume":221,"main_file_link":[{"url":"https://arxiv.org/abs/1408.2058","open_access":"1"}],"oa":1,"publication_status":"published"},{"_id":"1882","abstract":[{"text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.","lang":"eng"}],"date_published":"2015-01-30T00:00:00Z","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1408.1256"}],"oa":1,"publication_status":"published","volume":8997,"year":"2015","oa_version":"Preprint","publist_id":"5216","date_updated":"2021-01-12T06:53:49Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"page":"306 - 324","date_created":"2018-12-11T11:54:31Z","month":"01","publisher":"Springer","intvolume":"      8997","status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","conference":{"location":"Bertinoro, Italy","end_date":"2014-09-12","start_date":"2014-09-10","name":"FACS: Formal Aspects of Component Software"},"title":"Compositionality for quantitative specifications","ec_funded":1,"citation":{"short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., &#38; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>.","ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","mla":"Fahrenberg, Uli, et al. <i>Compositionality for Quantitative Specifications</i>. Vol. 8997, Springer, 2015, pp. 306–24, doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>."},"alternative_title":["LNCS"],"author":[{"last_name":"Fahrenberg","first_name":"Uli","full_name":"Fahrenberg, Uli"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"full_name":"Traonouez, Louis","first_name":"Louis","last_name":"Traonouez"}],"type":"conference","day":"30","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"doi":"10.1007/978-3-319-15317-9_19","language":[{"iso":"eng"}]},{"quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":" Information Processing Letters","intvolume":"       115","status":"public","publisher":"Elsevier","month":"01","date_created":"2018-12-11T11:55:20Z","page":"52 - 59","language":[{"iso":"eng"}],"doi":"10.1016/j.ipl.2014.09.001","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_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"}],"day":"01","type":"journal_article","author":[{"last_name":"Bérard","full_name":"Bérard, Béatrice","first_name":"Béatrice"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sznajder, Nathalie","first_name":"Nathalie","last_name":"Sznajder"}],"ec_funded":1,"citation":{"ieee":"B. Bérard, K. Chatterjee, and N. Sznajder, “Probabilistic opacity for Markov decision processes,” <i> Information Processing Letters</i>, vol. 115, no. 1. Elsevier, pp. 52–59, 2015.","ista":"Bérard B, Chatterjee K, Sznajder N. 2015. Probabilistic opacity for Markov decision processes.  Information Processing Letters. 115(1), 52–59.","chicago":"Bérard, Béatrice, Krishnendu Chatterjee, and Nathalie Sznajder. “Probabilistic Opacity for Markov Decision Processes.” <i> Information Processing Letters</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">https://doi.org/10.1016/j.ipl.2014.09.001</a>.","mla":"Bérard, Béatrice, et al. “Probabilistic Opacity for Markov Decision Processes.” <i> Information Processing Letters</i>, vol. 115, no. 1, Elsevier, 2015, pp. 52–59, doi:<a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">10.1016/j.ipl.2014.09.001</a>.","short":"B. Bérard, K. Chatterjee, N. Sznajder,  Information Processing Letters 115 (2015) 52–59.","apa":"Bérard, B., Chatterjee, K., &#38; Sznajder, N. (2015). Probabilistic opacity for Markov decision processes. <i> Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">https://doi.org/10.1016/j.ipl.2014.09.001</a>","ama":"Bérard B, Chatterjee K, Sznajder N. Probabilistic opacity for Markov decision processes. <i> Information Processing Letters</i>. 2015;115(1):52-59. doi:<a href=\"https://doi.org/10.1016/j.ipl.2014.09.001\">10.1016/j.ipl.2014.09.001</a>"},"title":"Probabilistic opacity for Markov decision processes","volume":115,"publication_status":"published","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1407.4225"}],"oa":1,"_id":"2034","abstract":[{"text":"Opacity is a generic security property, that has been defined on (non-probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non-deterministicchoice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and ω-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non-opaquebecomes decidable for a restricted class of ω-regular secrets, as well as for all ω-regular secrets under finite-memory schedulers.","lang":"eng"}],"date_published":"2015-01-01T00:00:00Z","issue":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:54:52Z","scopus_import":1,"publist_id":"5025","oa_version":"Preprint","year":"2015"}]