[{"status":"public","type":"conference","alternative_title":["LIPIcs"],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"file":[{"file_name":"IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf","file_id":"4714","date_created":"2018-12-12T10:08:52Z","date_updated":"2018-12-12T10:08:52Z","creator":"system","relation":"main_file","access_level":"open_access","file_size":546133,"content_type":"application/pdf"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Published Version","month":"01","conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2016-07-12","location":"Rome, Italy","end_date":"2016-07-15"},"language":[{"iso":"eng"}],"title":"Computation tree logic for synchronization properties","pubrep_id":"812","date_updated":"2021-01-12T06:48:03Z","oa":1,"scopus_import":1,"has_accepted_license":"1","intvolume":"        55","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"quality_controlled":"1","volume":55,"department":[{"_id":"KrCh"}],"date_published":"2016-01-01T00:00:00Z","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","publication_status":"published","abstract":[{"text":"We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. ","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["005"],"_id":"1070","file_date_updated":"2018-12-12T10:08:52Z","doi":"10.4230/LIPIcs.ICALP.2016.98","citation":{"short":"K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ama":"Chatterjee K, Doyen L. Computation tree logic for synchronization properties. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>","ieee":"K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Computation Tree Logic for Synchronization Properties</i>. Vol. 55, 98, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for Synchronization Properties,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>.","ista":"Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.","apa":"Chatterjee, K., &#38; Doyen, L. (2016). Computation tree logic for synchronization properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>"},"date_created":"2018-12-11T11:49:59Z","publist_id":"6313","year":"2016","acknowledgement":"This research was partially supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003, and European project Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for their insightful\r\ncomments and suggestions.\r\n","article_number":"98","ec_funded":1},{"title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","pubrep_id":"777","date_updated":"2023-09-07T12:01:58Z","oa":1,"has_accepted_license":"1","scopus_import":1,"intvolume":"        57","language":[{"iso":"eng"}],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"}],"oa_version":"Published Version","day":"01","file":[{"file_id":"5084","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","date_created":"2018-12-12T10:14:31Z","date_updated":"2018-12-12T10:14:31Z","creator":"system","access_level":"open_access","file_size":579225,"relation":"main_file","content_type":"application/pdf"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2016-08-22","name":"ESA: European Symposium on Algorithms","end_date":"2016-08-24","location":"Aarhus, Denmark"},"month":"08","alternative_title":["LIPIcs"],"status":"public","type":"conference","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs (Vol. 57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs,” presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016, vol. 57.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. ESA: European Symposium on Algorithms, LIPIcs, vol. 57, 28.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs</i>. Vol. 57, 28, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>."},"publist_id":"6312","date_created":"2018-12-11T11:49:59Z","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE) and ERC Start grant (279307: Graph Games).","year":"2016","ec_funded":1,"related_material":{"record":[{"status":"public","id":"821","relation":"dissertation_contains"}]},"article_number":"28","file_date_updated":"2018-12-12T10:14:31Z","_id":"1071","doi":"10.4230/LIPIcs.ESA.2016.28","publication_status":"published","abstract":[{"text":"We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. ","lang":"eng"}],"ddc":["004","006"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":57,"publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","date_published":"2016-08-01T00:00:00Z"},{"_id":"9867","doi":"10.1371/journal.pone.0163867.s008","article_processing_charge":"No","year":"2016","date_updated":"2023-02-21T16:59:01Z","citation":{"apa":"Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Experimental game instructions. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">https://doi.org/10.1371/journal.pone.0163867.s008</a>","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental game instructions.” Public Library of Science, 2016.","ama":"Hilbe C, Hagel K, Milinski M. Experimental game instructions. 2016. doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental game instructions, Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>.","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Game Instructions.” Public Library of Science, 2016. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">https://doi.org/10.1371/journal.pone.0163867.s008</a>.","mla":"Hilbe, Christian, et al. <i>Experimental Game Instructions</i>. Public Library of Science, 2016, doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>."},"date_created":"2021-08-10T08:42:00Z","title":"Experimental game instructions","related_material":{"record":[{"status":"public","id":"1322","relation":"used_in_publication"}]},"type":"research_data_reference","status":"public","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"author":[{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian"},{"full_name":"Hagel, Kristin","first_name":"Kristin","last_name":"Hagel"},{"last_name":"Milinski","first_name":"Manfred","full_name":"Milinski, Manfred"}],"month":"10","abstract":[{"lang":"eng","text":"In the beginning of our experiment, subjects were asked to read a few pages on their computer screens that would explain the rules of the subsequent game. Here, we provide these instructions, translated from German."}],"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","oa_version":"Published Version","day":"04"},{"related_material":{"record":[{"id":"1322","relation":"used_in_publication","status":"public"}]},"date_created":"2021-08-10T08:45:00Z","title":"Experimental data","citation":{"apa":"Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Experimental data. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">https://doi.org/10.1371/journal.pone.0163867.s009</a>","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Data.” Public Library of Science, 2016. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">https://doi.org/10.1371/journal.pone.0163867.s009</a>.","mla":"Hilbe, Christian, et al. <i>Experimental Data</i>. Public Library of Science, 2016, doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>.","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental data, Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>.","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ama":"Hilbe C, Hagel K, Milinski M. Experimental data. 2016. doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental data.” Public Library of Science, 2016."},"article_processing_charge":"No","year":"2016","date_updated":"2023-02-21T16:59:01Z","doi":"10.1371/journal.pone.0163867.s009","_id":"9868","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","abstract":[{"text":"The raw data file containing the experimental decisions of all our study subjects.","lang":"eng"}],"oa_version":"Published Version","day":"04","month":"10","author":[{"last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","first_name":"Christian","full_name":"Hilbe, Christian"},{"full_name":"Hagel, Kristin","first_name":"Kristin","last_name":"Hagel"},{"last_name":"Milinski","full_name":"Milinski, Manfred","first_name":"Manfred"}],"department":[{"_id":"KrCh"}],"type":"research_data_reference","status":"public","date_published":"2016-10-04T00:00:00Z","publisher":"Public Library of Science"},{"file_date_updated":"2018-12-12T10:17:31Z","_id":"1090","doi":"10.4230/LIPIcs.MFCS.2016.24","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","year":"2016","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland, 2016, vol. 58.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 24."},"publist_id":"6286","date_created":"2018-12-11T11:50:05Z","ec_funded":1,"article_number":"24","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2016-08-01T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":58,"quality_controlled":"1","publication_status":"published","ddc":["004"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.","lang":"eng"}],"language":[{"iso":"eng"}],"date_updated":"2021-01-12T06:48:12Z","pubrep_id":"795","oa":1,"title":"Nested weighted limit-average automata of bounded width","intvolume":"        58","has_accepted_license":"1","scopus_import":1,"alternative_title":["LIPIcs"],"type":"conference","status":"public","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan"}],"conference":{"location":"Krakow; Poland","end_date":"2016-08-26","name":"MFCS: Mathematical Foundations of Computer Science (SG)","start_date":"2016-08-22"},"month":"08","oa_version":"Published Version","day":"01","file":[{"file_id":"5286","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","date_updated":"2018-12-12T10:17:31Z","date_created":"2018-12-12T10:17:31Z","creator":"system","content_type":"application/pdf","file_size":564560,"access_level":"open_access","relation":"main_file"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"volume":59,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2016-08-01T00:00:00Z","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"ddc":["004"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publication_status":"published","doi":"10.4230/LIPIcs.CONCUR.2016.20","file_date_updated":"2018-12-12T10:11:39Z","_id":"1093","ec_funded":1,"article_number":"20","related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"date_created":"2018-12-11T11:50:06Z","publist_id":"6283","citation":{"ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>"},"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","year":"2016","alternative_title":["LIPIcs"],"type":"conference","status":"public","oa_version":"Published Version","day":"01","file":[{"creator":"system","file_size":501827,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"4895","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","date_created":"2018-12-12T10:11:39Z","date_updated":"2018-12-12T10:11:39Z"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City; Canada","end_date":"2016-08-26"},"month":"08","author":[{"first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"language":[{"iso":"eng"}],"intvolume":"        59","has_accepted_license":"1","scopus_import":1,"title":"Linear distances between Markov chains","oa":1,"pubrep_id":"794","date_updated":"2023-09-07T11:58:33Z"},{"language":[{"iso":"eng"}],"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","oa":1,"date_updated":"2021-01-12T06:48:34Z","title":"Quantitative automata under probabilistic semantics","scopus_import":1,"type":"conference","status":"public","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"arxiv":1,"conference":{"end_date":"2016-07-08","location":"New York, NY, USA","start_date":"2016-07-05","name":"LICS: Logic in Computer Science"},"month":"07","day":"05","main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1138","doi":"10.1145/2933575.2933588","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","year":"2016","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, 76–85. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, IEEE, 2016, pp. 76–85, doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, New York, NY, USA, 2016, pp. 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>. IEEE; 2016:76-85. doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative automata under probabilistic semantics. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i> (pp. 76–85). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>"},"date_created":"2018-12-11T11:50:21Z","publist_id":"6220","ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"publisher":"IEEE","date_published":"2016-07-05T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"76 - 85","quality_controlled":"1","publication_status":"published","external_id":{"arxiv":["1604.06764"]},"abstract":[{"text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.","lang":"eng"}]},{"publication_status":"published","external_id":{"arxiv":["1602.02670"]},"abstract":[{"text":"Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.","lang":"eng"}],"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"publisher":"IEEE","date_published":"2016-07-05T00:00:00Z","page":"197 - 206","department":[{"_id":"KrCh"}],"quality_controlled":"1","acknowledgement":"K.  C.,  M.  H.,  and  W.  D.  are  partially  supported  by  the  Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003.\r\nK. C. is partially supported by the Austrian Science Fund (FWF)\r\nNFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant\r\n(279307: Graph Games). For W. D., M. H., and V. L. the research\r\nleading to these results has received funding from the European\r\nResearch Council under the European Union’s Seventh Framework\r\nProgramme (FP/2007-2013) / ERC Grant Agreement no. 340506.","year":"2016","publist_id":"6219","date_created":"2018-12-11T11:50:22Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2016, pp. 197–206, doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>.","ista":"Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. 2016. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, , 197–206.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvoák, Monika H Henzinger, and Veronika Loitzenbauer. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 197–206. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>.","ama":"Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2016:197-206. doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>","ieee":"K. Chatterjee, W. Dvoák, M. H. Henzinger, and V. Loitzenbauer, “Model and objective separation with conditional lower bounds: disjunction is harder than conjunction,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, New York, NY, USA, 2016, pp. 197–206.","short":"K. Chatterjee, W. Dvoák, M.H. Henzinger, V. Loitzenbauer, in:, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206.","apa":"Chatterjee, K., Dvoák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2016). Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 197–206). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>"},"_id":"1140","doi":"10.1145/2933575.2935304","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Dvoák","full_name":"Dvoák, Wolfgang","first_name":"Wolfgang"},{"full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"arxiv":1,"conference":{"start_date":"2016-07-05","name":"LICS: Logic in Computer Science","end_date":"2016-07-08","location":"New York, NY, USA"},"month":"07","main_file_link":[{"url":"https://arxiv.org/abs/1602.02670","open_access":"1"}],"oa_version":"Preprint","day":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["Proceedings Symposium on Logic in Computer Science"],"type":"conference","status":"public","date_updated":"2025-06-02T08:53:44Z","oa":1,"article_processing_charge":"No","title":"Model and objective separation with conditional lower bounds: disjunction is harder than conjunction","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science"},{"publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Davies, Jessica","first_name":"Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87","last_name":"Davies"}],"day":"02","oa_version":"None","abstract":[{"text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.","lang":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2016-02-17","location":"Phoenix, AZ, USA","start_date":"2016-02-12","name":"AAAI: Conference on Artificial Intelligence"},"month":"12","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"3225 - 3232","volume":2016,"quality_controlled":"1","publisher":"AAAI Press","status":"public","type":"conference","date_published":"2016-12-02T00:00:00Z","title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps","date_created":"2018-12-11T11:50:30Z","publist_id":"6191","citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i> (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.","mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, vol. 2016, AAAI Press, 2016, pp. 3225–32.","ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, 2016:3225–32. AAAI Press, 2016.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>. Vol 2016. AAAI Press; 2016:3225-3232.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232."},"date_updated":"2023-02-23T12:26:41Z","year":"2016","ec_funded":1,"intvolume":"      2016","related_material":{"record":[{"relation":"earlier_version","id":"5443","status":"public"}],"link":[{"url":"https://dl.acm.org/citation.cfm?id=3016355","relation":"table_of_contents"}]},"_id":"1166","language":[{"iso":"eng"}],"publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence"},{"_id":"1182","language":[{"iso":"eng"}],"oa":1,"date_updated":"2023-02-21T10:04:26Z","year":"2016","publist_id":"6171","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Tkadlec, J. (2016). Robust draws in balanced knockout tournaments (Vol. 2016–January, pp. 172–179). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA: AAAI Press.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Josef Tkadlec. “Robust Draws in Balanced Knockout Tournaments,” 2016–January:172–79. AAAI Press, 2016.","mla":"Chatterjee, Krishnendu, et al. <i>Robust Draws in Balanced Knockout Tournaments</i>. Vol. 2016–January, AAAI Press, 2016, pp. 172–79.","ista":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. 2016. Robust draws in balanced knockout tournaments. IJCAI: International Joint Conference on Artificial Intelligence vol. 2016–January, 172–179.","ama":"Chatterjee K, Ibsen-Jensen R, Tkadlec J. Robust draws in balanced knockout tournaments. In: Vol 2016-January. AAAI Press; 2016:172-179.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and J. Tkadlec, “Robust draws in balanced knockout tournaments,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, New York, NY, USA, 2016, vol. 2016–January, pp. 172–179.","short":"K. Chatterjee, R. Ibsen-Jensen, J. Tkadlec, in:, AAAI Press, 2016, pp. 172–179."},"date_created":"2018-12-11T11:50:35Z","title":"Robust draws in balanced knockout tournaments","ec_funded":1,"related_material":{"link":[{"url":"https://www.ijcai.org/proceedings/2016","relation":"table_of_contents"}]},"scopus_import":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"publisher":"AAAI Press","status":"public","type":"conference","date_published":"2016-01-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"172 - 179","quality_controlled":"1","volume":"2016-January","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen"},{"first_name":"Josef","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684"}],"publication_status":"published","conference":{"end_date":"2016-07-15","location":"New York, NY, USA","start_date":"2016-07-09","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"month":"01","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/1604.05090v1","open_access":"1"}],"day":"01","abstract":[{"text":"Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decisionmaking and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a) there exist deterministic tournaments (where the pairwise winning probabilities are 0 or 1) where one optimal draw is much more robust than the other; and (b) in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"has_accepted_license":"1","intvolume":"        19","scopus_import":1,"date_updated":"2021-01-12T06:49:03Z","oa":1,"pubrep_id":"798","title":"Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze","publication":"Physics of Life Reviews","language":[{"iso":"eng"}],"month":"12","file":[{"checksum":"95e6dc78278334b99dacbf8822509364","file_name":"IST-2017-798-v1+1_comment_adami.pdf","file_id":"4855","date_updated":"2020-07-14T12:44:39Z","date_created":"2018-12-12T10:11:02Z","creator":"system","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_size":171352}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Submitted Version","author":[{"orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian","first_name":"Christian"},{"full_name":"Traulsen, Arne","first_name":"Arne","last_name":"Traulsen"}],"status":"public","type":"journal_article","ec_funded":1,"year":"2016","acknowledgement":"C.H. acknowledges generous support from the ISTFELLOW program.","date_created":"2018-12-11T11:50:40Z","citation":{"apa":"Hilbe, C., &#38; Traulsen, A. (2016). Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. <i>Physics of Life Reviews</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">https://doi.org/10.1016/j.plrev.2016.10.004</a>","chicago":"Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling: Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J. Schossau and A. Hintze.” <i>Physics of Life Reviews</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">https://doi.org/10.1016/j.plrev.2016.10.004</a>.","ista":"Hilbe C, Traulsen A. 2016. Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. Physics of Life Reviews. 19, 29–31.","mla":"Hilbe, Christian, and Arne Traulsen. “Only the Combination of Mathematics and Agent Based Simulations Can Leverage the Full Potential of Evolutionary Modeling: Comment on ‘Evolutionary Game Theory Using Agent-Based Methods’ by C. Adami, J. Schossau and A. Hintze.” <i>Physics of Life Reviews</i>, vol. 19, Elsevier, 2016, pp. 29–31, doi:<a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">10.1016/j.plrev.2016.10.004</a>.","ieee":"C. Hilbe and A. Traulsen, “Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on ‘Evolutionary game theory using agent-based methods’ by C. Adami, J. Schossau and A. Hintze,” <i>Physics of Life Reviews</i>, vol. 19. Elsevier, pp. 29–31, 2016.","ama":"Hilbe C, Traulsen A. Only the combination of mathematics and agent based simulations can leverage the full potential of evolutionary modeling: Comment on “Evolutionary game theory using agent-based methods” by C. Adami, J. Schossau and A. Hintze. <i>Physics of Life Reviews</i>. 2016;19:29-31. doi:<a href=\"https://doi.org/10.1016/j.plrev.2016.10.004\">10.1016/j.plrev.2016.10.004</a>","short":"C. Hilbe, A. Traulsen, Physics of Life Reviews 19 (2016) 29–31."},"publist_id":"6150","doi":"10.1016/j.plrev.2016.10.004","_id":"1200","file_date_updated":"2020-07-14T12:44:39Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"ddc":["530"],"publication_status":"published","date_published":"2016-12-01T00:00:00Z","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","publisher":"Elsevier","quality_controlled":"1","volume":19,"department":[{"_id":"KrCh"}],"page":"29 - 31","project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}]},{"language":[{"iso":"eng"}],"intvolume":"       285","has_accepted_license":"1","scopus_import":1,"date_updated":"2021-01-12T08:00:54Z","oa":1,"pubrep_id":"950","title":"The complexity of deciding legality of a single step of magic: The gathering","status":"public","type":"conference","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"month":"01","conference":{"name":"ECAI: European Conference on Artificial Intelligence","start_date":"2016-08-29","location":"The Hague, Netherlands","end_date":"2016-09-02"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2020-07-14T12:46:35Z","date_created":"2018-12-12T10:07:59Z","checksum":"848043c812ace05e459579c923f3d3cf","file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","file_id":"4658","content_type":"application/pdf","file_size":2116225,"relation":"main_file","access_level":"open_access","creator":"system"}],"oa_version":"Published Version","day":"01","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"}],"doi":"10.3233/978-1-61499-672-9-1432","_id":"478","file_date_updated":"2020-07-14T12:46:35Z","year":"2016","citation":{"apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2016). The complexity of deciding legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands: IOS Press. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Complexity of Deciding Legality of a Single Step of Magic: The Gathering</i>. Vol. 285, IOS Press, 2016, pp. 1432–39, doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>.","ista":"Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of a single step of magic: The gathering. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285, 1432–1439.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of a single step of magic: The gathering,” presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.","ama":"Chatterjee K, Ibsen-Jensen R. The complexity of deciding legality of a single step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>"},"date_created":"2018-12-11T11:46:41Z","publist_id":"7342","date_published":"2016-01-01T00:00:00Z","license":"https://creativecommons.org/licenses/by-nc/4.0/","publisher":"IOS Press","quality_controlled":"1","volume":285,"page":"1432 - 1439","department":[{"_id":"KrCh"}],"tmp":{"short":"CC BY-NC (4.0)","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png"},"ddc":["004"],"abstract":[{"text":"Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic.","lang":"eng"}],"publication_status":"published"},{"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"publisher":"IEEE","date_published":"2016-07-05T00:00:00Z","page":"247 - 256","department":[{"_id":"KrCh"}],"volume":"05-08-July-2016","quality_controlled":"1","publication_status":"published","abstract":[{"text":"Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.","lang":"eng"}],"_id":"480","doi":"10.1145/2933575.2934513","year":"2016","date_created":"2018-12-11T11:46:42Z","citation":{"ista":"Chatterjee K, Doyen L. 2016. Perfect-information stochastic games with generalized mean-payoff objectives. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, vol. 05-08-July-2016, 247–256.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives</i>. Vol. 05-08-July-2016, IEEE, 2016, pp. 247–56, doi:<a href=\"https://doi.org/10.1145/2933575.2934513\">10.1145/2933575.2934513</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives,” 05-08-July-2016:247–56. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2934513\">https://doi.org/10.1145/2933575.2934513</a>.","ama":"Chatterjee K, Doyen L. Perfect-information stochastic games with generalized mean-payoff objectives. In: Vol 05-08-July-2016. IEEE; 2016:247-256. doi:<a href=\"https://doi.org/10.1145/2933575.2934513\">10.1145/2933575.2934513</a>","ieee":"K. Chatterjee and L. Doyen, “Perfect-information stochastic games with generalized mean-payoff objectives,” presented at the LICS: Logic in Computer Science, New York, NY, USA, 2016, vol. 05-08-July-2016, pp. 247–256.","short":"K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.","apa":"Chatterjee, K., &#38; Doyen, L. (2016). Perfect-information stochastic games with generalized mean-payoff objectives (Vol. 05-08-July-2016, pp. 247–256). Presented at the LICS: Logic in Computer Science, New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2934513\">https://doi.org/10.1145/2933575.2934513</a>"},"publist_id":"7340","ec_funded":1,"alternative_title":["Proceedings Symposium on Logic in Computer Science"],"type":"conference","status":"public","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"conference":{"location":"New York, NY, USA","end_date":"2016-07-08","name":"LICS: Logic in Computer Science","start_date":"2016-07-05"},"month":"07","day":"05","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06376"}],"oa_version":"Preprint","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"oa":1,"date_updated":"2021-01-12T08:00:56Z","title":"Perfect-information stochastic games with generalized mean-payoff objectives","scopus_import":1},{"conference":{"start_date":"2015-01-25","name":"AAAI: Conference on Artificial Intelligence","end_date":"2015-01-30","location":"Austin, TX, USA"},"month":"01","oa_version":"None","main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300","open_access":"1"}],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Ahmed, Umair","first_name":"Umair","last_name":"Ahmed"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Gulwani","first_name":"Sumit","full_name":"Gulwani, Sumit"}],"type":"conference","status":"public","intvolume":"         2","scopus_import":1,"date_updated":"2023-02-23T12:25:07Z","oa":1,"article_processing_charge":"No","title":"Automatic generation of alternative starting positions for simple traditional board games","publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"abstract":[{"text":"Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in the development of mathematical and logical skills, but also in the emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. We present an approach that generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. The presence of such states for standard game variants like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played as the default start state is heavily biased. ","lang":"eng"}],"publication_status":"published","publisher":"AAAI Press","date_published":"2015-01-01T00:00:00Z","page":"745 - 752","department":[{"_id":"KrCh"}],"volume":2,"quality_controlled":"1","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"5410","status":"public"}]},"acknowledgement":"A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n","year":"2015","publist_id":"5713","date_created":"2018-12-11T11:52:16Z","citation":{"apa":"Ahmed, U., Chatterjee, K., &#38; Gulwani, S. (2015). Automatic generation of alternative starting positions for simple traditional board games. In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i> (Vol. 2, pp. 745–752). Austin, TX, USA: AAAI Press.","short":"U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative starting positions for simple traditional board games,” in <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, Austin, TX, USA, 2015, vol. 2, pp. 745–752.","ama":"Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting positions for simple traditional board games. In: <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>. Vol 2. AAAI Press; 2015:745-752.","mla":"Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, vol. 2, AAAI Press, 2015, pp. 745–52.","chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, 2:745–52. AAAI Press, 2015.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative starting positions for simple traditional board games. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2, 745–752."},"_id":"1481"},{"publication_status":"published","abstract":[{"text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000","003"],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"volume":42,"quality_controlled":"1","page":"142 - 154","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2015-01-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>","apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>"},"date_created":"2018-12-11T11:52:22Z","publist_id":"5680","year":"2015","acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","ec_funded":1,"_id":"1499","file_date_updated":"2020-07-14T12:44:58Z","doi":"10.4230/LIPIcs.CONCUR.2015.142","author":[{"full_name":"Kretinsky, Jan","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"},{"last_name":"Larsen","first_name":"Kim","full_name":"Larsen, Kim"},{"last_name":"Laursen","first_name":"Simon","full_name":"Laursen, Simon"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"file":[{"date_created":"2018-12-12T10:08:12Z","date_updated":"2020-07-14T12:44:58Z","file_id":"4672","file_name":"IST-2016-498-v1+1_32.pdf","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","access_level":"open_access","file_size":623563,"relation":"main_file","content_type":"application/pdf","creator":"system"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Published Version","month":"01","conference":{"start_date":"2015-09-01","name":"CONCUR: Concurrency Theory","end_date":"2015-09-04","location":"Madrid, Spain"},"type":"conference","status":"public","alternative_title":["LIPIcs"],"title":"Polynomial time decidability of weighted synchronization under partial observability","oa":1,"pubrep_id":"498","date_updated":"2021-01-12T06:51:10Z","intvolume":"        42","scopus_import":1,"has_accepted_license":"1","language":[{"iso":"eng"}]},{"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"ec_funded":1,"citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>.","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264."},"publist_id":"5677","date_created":"2018-12-11T11:52:23Z","year":"2015","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","doi":"10.1007/s10703-015-0235-2","_id":"1501","abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"publication_status":"published","quality_controlled":"1","volume":47,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"230 - 264","date_published":"2015-10-01T00:00:00Z","publisher":"Springer","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"intvolume":"        47","scopus_import":1,"title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","issue":"2","oa":1,"date_updated":"2023-09-07T11:58:33Z","publication":"Formal Methods in System Design","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1405.0835","open_access":"1"}],"month":"10","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin"},{"last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"}],"type":"journal_article","status":"public"},{"type":"conference","status":"public","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"author":[{"first_name":"Nikola","full_name":"Beneš, Nikola","last_name":"Beneš"},{"first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"file":[{"creator":"system","relation":"main_file","access_level":"open_access","file_size":467561,"content_type":"application/pdf","file_id":"5303","checksum":"c6ce681035c163a158751f240cb7d389","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","date_created":"2018-12-12T10:17:46Z","date_updated":"2020-07-14T12:44:59Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Submitted Version","month":"05","publication_identifier":{"isbn":["978-1-4503-3471-6"]},"conference":{"location":"Montreal, QC, Canada","end_date":"2015-05-08","name":"CBSE: Component-Based Software Engineering ","start_date":"2015-05-04"},"language":[{"iso":"eng"}],"title":"Complete composition operators for IOCO-testing theory","pubrep_id":"625","date_updated":"2023-09-07T11:58:33Z","oa":1,"scopus_import":1,"has_accepted_license":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"quality_controlled":"1","page":"101 - 110","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2015-05-01T00:00:00Z","publisher":"ACM","publication_status":"published","abstract":[{"text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.","lang":"eng"}],"ddc":["000"],"_id":"1502","file_date_updated":"2020-07-14T12:44:59Z","doi":"10.1145/2737166.2737175","date_created":"2018-12-11T11:52:24Z","publist_id":"5676","citation":{"apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>.","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>."},"year":"2015","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer).  Jan Křetínský has been partially supported by the Czech Science Foundation, grant No.  P202/12/G061.  Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","related_material":{"record":[{"relation":"dissertation_contains","id":"1155","status":"public"}]},"ec_funded":1},{"doi":"10.1073/pnas.1511366112","_id":"1559","citation":{"short":"R. Ibsen-Jensen, K. Chatterjee, M. Nowak, PNAS 112 (2015) 15636–15641.","ieee":"R. Ibsen-Jensen, K. Chatterjee, and M. Nowak, “Computational complexity of ecological and evolutionary spatial dynamics,” <i>PNAS</i>, vol. 112, no. 51. National Academy of Sciences, pp. 15636–15641, 2015.","ama":"Ibsen-Jensen R, Chatterjee K, Nowak M. Computational complexity of ecological and evolutionary spatial dynamics. <i>PNAS</i>. 2015;112(51):15636-15641. doi:<a href=\"https://doi.org/10.1073/pnas.1511366112\">10.1073/pnas.1511366112</a>","chicago":"Ibsen-Jensen, Rasmus, Krishnendu Chatterjee, and Martin Nowak. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1511366112\">https://doi.org/10.1073/pnas.1511366112</a>.","mla":"Ibsen-Jensen, Rasmus, et al. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” <i>PNAS</i>, vol. 112, no. 51, National Academy of Sciences, 2015, pp. 15636–41, doi:<a href=\"https://doi.org/10.1073/pnas.1511366112\">10.1073/pnas.1511366112</a>.","ista":"Ibsen-Jensen R, Chatterjee K, Nowak M. 2015. Computational complexity of ecological and evolutionary spatial dynamics. PNAS. 112(51), 15636–15641.","apa":"Ibsen-Jensen, R., Chatterjee, K., &#38; Nowak, M. (2015). Computational complexity of ecological and evolutionary spatial dynamics. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1511366112\">https://doi.org/10.1073/pnas.1511366112</a>"},"date_created":"2018-12-11T11:52:43Z","publist_id":"5612","year":"2015","page":"15636 - 15641","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":112,"publisher":"National Academy of Sciences","date_published":"2015-12-22T00:00:00Z","external_id":{"pmid":["26644569"]},"abstract":[{"lang":"eng","text":"There are deep, yet largely unexplored, connections between computer science and biology. Both disciplines examine how information proliferates in time and space. Central results in computer science describe the complexity of algorithms that solve certain classes of problems. An algorithm is deemed efficient if it can solve a problem in polynomial time, which means the running time of the algorithm is a polynomial function of the length of the input. There are classes of harder problems for which the fastest possible algorithm requires exponential time. Another criterion is the space requirement of the algorithm. There is a crucial distinction between algorithms that can find a solution, verify a solution, or list several distinct solutions in given time and space. The complexity hierarchy that is generated in this way is the foundation of theoretical computer science. Precise complexity results can be notoriously difficult. The famous question whether polynomial time equals nondeterministic polynomial time (i.e., P = NP) is one of the hardest open problems in computer science and all of mathematics. Here, we consider simple processes of ecological and evolutionary spatial dynamics. The basic question is: What is the probability that a new invader (or a new mutant)will take over a resident population?We derive precise complexity results for a variety of scenarios. We therefore show that some fundamental questions in this area cannot be answered by simple equations (assuming that P is not equal to NP)."}],"publication_status":"published","publication":"PNAS","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"       112","title":"Computational complexity of ecological and evolutionary spatial dynamics","oa":1,"date_updated":"2021-01-12T06:51:36Z","issue":"51","pmid":1,"status":"public","type":"journal_article","day":"22","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4697423/"}],"oa_version":"Submitted Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"12","author":[{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}]},{"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"quality_controlled":"1","volume":9450,"page":"162 - 177","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2015-11-22T00:00:00Z","publisher":"Springer","publication_status":"published","abstract":[{"lang":"eng","text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata."}],"_id":"1594","doi":"10.1007/978-3-662-48899-7_12","publist_id":"5577","citation":{"ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>.","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>.","ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>"},"date_created":"2018-12-11T11:52:55Z","year":"2015","acknowledgement":"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 Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","ec_funded":1,"type":"conference","status":"public","alternative_title":["LNCS"],"author":[{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"first_name":"Jan","full_name":"Krčál, Jan","last_name":"Krčál"},{"first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"22","month":"11","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","start_date":"2015-11-24","location":"Suva, Fiji","end_date":"2015-11-28"},"language":[{"iso":"eng"}],"title":"Controller synthesis for MDPs and frequency LTL\\GU","date_updated":"2021-01-12T06:51:50Z","intvolume":"      9450","scopus_import":1},{"type":"journal_article","status":"public","month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"30","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1202.4175"}],"oa_version":"Preprint","arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Joglekar","full_name":"Joglekar, Manas","first_name":"Manas"},{"first_name":"Nisarg","full_name":"Shah, Nisarg","last_name":"Shah"}],"publication":"Theoretical Computer Science","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"       573","article_processing_charge":"No","issue":"3","date_updated":"2023-02-23T10:55:03Z","oa":1,"title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","date_published":"2015-03-30T00:00:00Z","publisher":"Elsevier","volume":573,"quality_controlled":"1","page":"71 - 89","department":[{"_id":"KrCh"}],"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure winning vertices such that the objective can be ensured with probability 1 from these vertices. We study for the first time the average-case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average-case running time is linear (as compared to the worst-case linear number of iterations and quadratic time complexity). Second, for the average-case analysis over all MDPs we show that the expected number of iterations is constant and the average-case running time is linear (again as compared to the worst-case linear number of iterations and quadratic time complexity). Finally we also show that when all MDPs are equally likely, the probability that the classical algorithm requires more than a constant number of iterations is exponentially small."}],"external_id":{"arxiv":["1202.4175"]},"publication_status":"published","doi":"10.1016/j.tcs.2015.01.050","_id":"1598","related_material":{"record":[{"relation":"earlier_version","id":"2715","status":"public"}]},"ec_funded":1,"year":"2015","acknowledgement":"The research was supported by FWF Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start Grant (279307: Graph Games), and the Microsoft Faculty Fellows Award. Nisarg Shah is also supported by NSF Grant CCF-1215883.\r\n","publist_id":"5571","date_created":"2018-12-11T11:52:56Z","citation":{"apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2015). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>","mla":"Chatterjee, Krishnendu, et al. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>, vol. 573, no. 3, Elsevier, 2015, pp. 71–89, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>.","ista":"Chatterjee K, Joglekar M, Shah N. 2015. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. Theoretical Computer Science. 573(3), 71–89.","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>.","short":"K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015) 71–89.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” <i>Theoretical Computer Science</i>, vol. 573, no. 3. Elsevier, pp. 71–89, 2015.","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. 2015;573(3):71-89. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>"}}]