[{"department":[{"_id":"KrCh"}],"publisher":"Institute of Electrical and Electronics Engineers","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","article_processing_charge":"No","publication":"38th Annual ACM/IEEE Symposium on Logic in Computer Science","day":"01","author":[{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"}],"arxiv":1,"title":"Stopping criteria for value iteration on stochastic games with quantitative objectives","language":[{"iso":"eng"}],"conference":{"end_date":"2023-06-29","name":"LICS: Symposium on Logic in Computer Science","location":"Boston, MA, United States","start_date":"2023-06-26"},"isi":1,"publication_identifier":{"isbn":["9798350335873"],"issn":["1043-6871"]},"quality_controlled":"1","doi":"10.1109/LICS56636.2023.10175771","year":"2023","acknowledgement":"This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”.","_id":"13967","oa_version":"Preprint","month":"07","type":"conference","date_updated":"2023-12-13T12:06:10Z","abstract":[{"lang":"eng","text":"A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution."}],"date_created":"2023-08-06T22:01:10Z","volume":2023,"external_id":{"isi":["001036707700042"],"arxiv":["2304.09930"]},"status":"public","citation":{"short":"J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2023.","ieee":"J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value iteration on stochastic games with quantitative objectives,” in 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States, 2023, vol. 2023.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 2023. Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LICS56636.2023.10175771.","ista":"Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science vol. 2023.","mla":"Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.” 38th Annual ACM/IEEE Symposium on Logic in Computer Science, vol. 2023, Institute of Electrical and Electronics Engineers, 2023, doi:10.1109/LICS56636.2023.10175771.","apa":"Kretinsky, J., Meggendorfer, T., & Weininger, M. (2023). Stopping criteria for value iteration on stochastic games with quantitative objectives. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2023). Boston, MA, United States: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS56636.2023.10175771","ama":"Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration on stochastic games with quantitative objectives. In: 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Vol 2023. Institute of Electrical and Electronics Engineers; 2023. doi:10.1109/LICS56636.2023.10175771"},"intvolume":" 2023","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2304.09930"}],"date_published":"2023-07-01T00:00:00Z"},{"file":[{"date_updated":"2023-09-06T08:25:50Z","file_id":"14276","checksum":"ed66278b61bb869e1baba3d9b9081271","date_created":"2023-09-06T08:25:50Z","access_level":"open_access","success":1,"file_name":"2023_LNCS_CAV_Kretinsky.pdf","relation":"main_file","content_type":"application/pdf","file_size":428354,"creator":"dernst"}],"day":"17","author":[{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"last_name":"Prokop","first_name":"Maximilian","full_name":"Prokop, Maximilian"},{"last_name":"Rieder","first_name":"Sabine","full_name":"Rieder, Sabine"}],"title":"Guessing winning policies in LTL synthesis by semantic learning","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","article_processing_charge":"Yes (in subscription journal)","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publication":"35th International Conference on Computer Aided Verification ","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031377051"],"issn":["0302-9743"]},"quality_controlled":"1","doi":"10.1007/978-3-031-37706-8_20","language":[{"iso":"eng"}],"conference":{"start_date":"2023-07-17","location":"Paris, France","name":"CAV: Computer Aided Verification","end_date":"2023-07-22"},"date_updated":"2023-09-06T08:27:33Z","abstract":[{"text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.","lang":"eng"}],"type":"conference","month":"07","oa_version":"Published Version","page":"390-414","file_date_updated":"2023-09-06T08:25:50Z","date_created":"2023-09-03T22:01:16Z","volume":13964,"year":"2023","acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","_id":"14259","has_accepted_license":"1","publication_status":"published","oa":1,"ddc":["000"],"date_published":"2023-07-17T00:00:00Z","status":"public","alternative_title":["LNCS"],"citation":{"apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In 35th International Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20","mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” 35th International Conference on Computer Aided Verification , vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.","ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: 35th International Conference on Computer Aided Verification . Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20","short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th International Conference on Computer Aided Verification , 13964:390–414. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.","ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in 35th International Conference on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 390–414."},"intvolume":" 13964"},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"publication":"Acta Informatica","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"scopus_import":"1","article_processing_charge":"Yes (via OA deal)","author":[{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"},{"full_name":"Waldmann, Clara","first_name":"Clara","last_name":"Waldmann"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"file":[{"checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_id":"10603","date_updated":"2022-01-07T07:50:31Z","access_level":"open_access","date_created":"2022-01-07T07:50:31Z","file_name":"2021_ActaInfor_Křetínský.pdf","success":1,"creator":"cchlebak","file_size":1066082,"relation":"main_file","content_type":"application/pdf"}],"day":"01","title":"Index appearance record with preorders","project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"keyword":["computer networks and communications","information systems","software"],"isi":1,"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"doi":"10.1007/s00236-021-00412-y","quality_controlled":"1","acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","year":"2022","_id":"10602","page":"585-618","oa_version":"Published Version","type":"journal_article","month":"10","date_updated":"2023-08-02T13:49:28Z","abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"volume":59,"file_date_updated":"2022-01-07T07:50:31Z","date_created":"2022-01-06T12:37:27Z","external_id":{"isi":["000735765500001"]},"status":"public","intvolume":" 59","citation":{"apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022). Index appearance record with preorders. Acta Informatica. Springer Nature. https://doi.org/10.1007/s00236-021-00412-y","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica, vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” Acta Informatica. Springer Nature, 2022. https://doi.org/10.1007/s00236-021-00412-y.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp. 585–618, 2022."},"oa":1,"publication_status":"published","has_accepted_license":"1","ddc":["000"],"date_published":"2022-10-01T00:00:00Z"},{"quality_controlled":"1","doi":"10.4230/LIPIcs.CONCUR.2022.11","publication_identifier":{"issn":["1868-8969"]},"language":[{"iso":"eng"}],"conference":{"location":"Warsaw, Poland","name":"CONCUR: Conference on Concurrency Theory","start_date":"2022-09-13","end_date":"2022-09-16"},"arxiv":1,"title":"Anytime guarantees for reachability in uncountable Markov decision processes","article_number":"11","day":"15","file":[{"file_size":960036,"content_type":"application/pdf","relation":"main_file","creator":"dernst","file_name":"2022_LIPIcS_Grover.pdf","success":1,"date_created":"2023-09-26T10:43:15Z","access_level":"open_access","file_id":"14372","date_updated":"2023-09-26T10:43:15Z","checksum":"e282e43d3ae0ba6e067b72f4583e13c0"}],"author":[{"full_name":"Grover, Kush","last_name":"Grover","first_name":"Kush"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias"},{"last_name":"Weininger","first_name":"Maimilian","full_name":"Weininger, Maimilian"}],"scopus_import":"1","article_processing_charge":"No","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publication":"33rd International Conference on Concurrency Theory ","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2022-09-15T00:00:00Z","ddc":["000"],"has_accepted_license":"1","oa":1,"publication_status":"published","citation":{"short":"K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International Conference on Concurrency Theory , Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","ieee":"K. Grover, J. Kretinsky, T. Meggendorfer, and M. Weininger, “Anytime guarantees for reachability in uncountable Markov decision processes,” in 33rd International Conference on Concurrency Theory , Warsaw, Poland, 2022, vol. 243.","chicago":"Grover, Kush, Jan Kretinsky, Tobias Meggendorfer, and Maimilian Weininger. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” In 33rd International Conference on Concurrency Theory , Vol. 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11.","ista":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. 2022. Anytime guarantees for reachability in uncountable Markov decision processes. 33rd International Conference on Concurrency Theory . CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 11.","mla":"Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” 33rd International Conference on Concurrency Theory , vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.CONCUR.2022.11.","apa":"Grover, K., Kretinsky, J., Meggendorfer, T., & Weininger, M. (2022). Anytime guarantees for reachability in uncountable Markov decision processes. In 33rd International Conference on Concurrency Theory (Vol. 243). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.11","ama":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. Anytime guarantees for reachability in uncountable Markov decision processes. In: 33rd International Conference on Concurrency Theory . Vol 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:10.4230/LIPIcs.CONCUR.2022.11"},"intvolume":" 243","external_id":{"arxiv":["2008.04824"]},"status":"public","alternative_title":["LIPIcs"],"file_date_updated":"2023-09-26T10:43:15Z","date_created":"2023-03-28T08:09:32Z","volume":243,"date_updated":"2023-09-26T10:43:30Z","abstract":[{"text":"We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation.\r\nAs this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the \"boundary\" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations.\r\nWe present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees.","lang":"eng"}],"oa_version":"Published Version","type":"conference","month":"09","_id":"12775","year":"2022","acknowledgement":"Kush Grover: The author has been supported by the DFG research training group GRK\r\n2428 ConVeY.\r\nMaximilian Weininger: The author has been partially supported by DFG projects 383882557\r\nStatistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic\r\nVerification (GOPro)"},{"language":[{"iso":"eng"}],"isi":1,"conference":{"end_date":"2018-04-20","start_date":"2018-04-14","location":"Thessaloniki, Greece","name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems"},"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"quality_controlled":"1","doi":"10.1007/978-3-319-89960-2_21","ec_funded":1,"article_processing_charge":"No","scopus_import":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"7584","title":"Strategy representation by decision trees in reactive synthesis","day":"12","file":[{"date_created":"2018-12-17T16:29:08Z","access_level":"open_access","file_id":"5723","date_updated":"2020-07-14T12:45:57Z","checksum":"b13874ffb114932ad9cc2586b7469db4","file_size":1829940,"content_type":"application/pdf","relation":"main_file","creator":"dernst","file_name":"2018_LNCS_Brazdil.pdf"}],"author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Toman","first_name":"Viktor","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X"}],"citation":{"short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. https://doi.org/10.1007/978-3-319-89960-2_21.","ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407.","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., & Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89960-2_21","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.","mla":"Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:10.1007/978-3-319-89960-2_21"},"intvolume":" 10805","external_id":{"isi":["000546326300021"]},"status":"public","alternative_title":["LNCS"],"ddc":["000"],"date_published":"2018-04-12T00:00:00Z","has_accepted_license":"1","publication_status":"published","oa":1,"_id":"297","year":"2018","date_created":"2018-12-11T11:45:41Z","file_date_updated":"2020-07-14T12:45:57Z","volume":10805,"abstract":[{"lang":"eng","text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs."}],"date_updated":"2025-06-02T08:53:40Z","month":"04","oa_version":"Published Version","type":"conference","page":"385 - 407"},{"publication_identifier":{"issn":["18605974"]},"pubrep_id":"957","doi":"10.23638/LMCS-13(2:15)2017","quality_controlled":"1","project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","_id":"2590DB08-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"701309"}],"language":[{"iso":"eng"}],"issue":"2","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Zuzana","last_name":"Křetínská","full_name":"Křetínská, Zuzana"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"day":"03","license":"https://creativecommons.org/licenses/by-nd/4.0/","file":[{"file_size":511832,"content_type":"application/pdf","relation":"main_file","creator":"system","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","date_created":"2018-12-12T10:18:32Z","access_level":"open_access","file_id":"5354","date_updated":"2020-07-14T12:46:33Z","checksum":"bfa405385ec6229ad5ead89ab5751639"}],"title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","article_number":"15","publist_id":"7355","publisher":"International Federation of Computational Logic","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"publication":"Logical Methods in Computer Science","ec_funded":1,"scopus_import":1,"tmp":{"short":"CC BY-ND (4.0)","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"publication_status":"published","oa":1,"has_accepted_license":"1","ddc":["004"],"date_published":"2017-07-03T00:00:00Z","status":"public","related_material":{"record":[{"id":"1657","status":"public","relation":"earlier_version"},{"status":"public","id":"5429","relation":"earlier_version"},{"status":"public","id":"5435","relation":"earlier_version"}]},"intvolume":" 13","citation":{"mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017.","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15.","apa":"Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 2017;13(2). doi:10.23638/LMCS-13(2:15)2017","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” Logical Methods in Computer Science, vol. 13, no. 2. International Federation of Computational Logic, 2017.","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(2:15)2017."},"date_updated":"2023-02-23T12:26:16Z","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"month":"07","oa_version":"Published Version","type":"journal_article","volume":13,"file_date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-11T11:46:38Z","year":"2017","_id":"466"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"language":[{"iso":"eng"}],"issue":"2","publication_identifier":{"issn":["15293785"]},"quality_controlled":"1","doi":"10.1145/3060139","department":[{"_id":"ToHe"}],"publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"ec_funded":1,"publication":"ACM Transactions on Computational Logic (TOCL)","day":"01","author":[{"last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Petrov","first_name":"Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"publist_id":"7349","title":"Faster statistical model checking for unbounded temporal properties","article_number":"12","status":"public","citation":{"short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 2. ACM, 2017.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3060139.","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM Transactions on Computational Logic (TOCL), vol. 18, no. 2, 12, ACM, 2017, doi:10.1145/3060139.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3060139","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 2017;18(2). doi:10.1145/3060139"},"intvolume":" 18","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1234"}]},"publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"date_published":"2017-05-01T00:00:00Z","year":"2017","_id":"471","date_updated":"2023-02-21T16:48:11Z","abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. ","lang":"eng"}],"oa_version":"Submitted Version","month":"05","type":"journal_article","date_created":"2018-12-11T11:46:39Z","volume":18},{"title":"Value iteration for long run average reward in markov decision processes","publist_id":"7135","author":[{"last_name":"Ashok","first_name":"Pranav","full_name":"Ashok, Pranav"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"}],"day":"13","scopus_import":1,"ec_funded":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"KrCh"}],"doi":"10.1007/978-3-319-63387-9_10","quality_controlled":"1","publication_identifier":{"isbn":["978-331963386-2"]},"conference":{"start_date":"2017-07-24","name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany","end_date":"2017-07-28"},"language":[{"iso":"eng"}],"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"volume":10426,"date_created":"2018-12-11T11:47:41Z","page":"201 - 221","month":"07","type":"conference","oa_version":"Submitted Version","date_updated":"2021-01-12T08:07:32Z","abstract":[{"text":"Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.","lang":"eng"}],"_id":"645","year":"2017","date_published":"2017-07-13T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.02326"}],"publication_status":"published","oa":1,"intvolume":" 10426","citation":{"short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","ieee":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value iteration for long run average reward in markov decision processes,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 201–221.","chicago":"Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer, 2017. https://doi.org/10.1007/978-3-319-63387-9_10.","mla":"Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.","ista":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration for long run average reward in markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 10426, 201–221.","apa":"Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T. (2017). Value iteration for long run average reward in markov decision processes. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10","ama":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration for long run average reward in markov decision processes. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10"},"alternative_title":["LNCS"],"status":"public","editor":[{"last_name":"Majumdar","first_name":"Rupak","full_name":"Majumdar, Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}]},{"year":"2017","acknowledgement":"This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061.","_id":"13160","date_updated":"2023-06-21T13:29:46Z","abstract":[{"text":"Transforming deterministic ω\r\n-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.","lang":"eng"}],"month":"03","oa_version":"Preprint","type":"conference","page":"443-460","date_created":"2023-06-21T13:21:14Z","volume":10205,"status":"public","external_id":{"arxiv":["1701.05738"]},"alternative_title":["LNCS"],"citation":{"ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In Tools and Algorithms for the Construction and Analysis of Systems, 10205:443–60. Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_26.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 10205. Springer; 2017:443-460. doi:10.1007/978-3-662-54577-5_26","mla":"Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_26"},"intvolume":" 10205","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1701.05738"}],"date_published":"2017-03-31T00:00:00Z","department":[{"_id":"KrCh"}],"publisher":"Springer","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","publication":"Tools and Algorithms for the Construction and Analysis of Systems","day":"31","author":[{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias"},{"first_name":"Clara","last_name":"Waldmann","full_name":"Waldmann, Clara"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"title":"Index appearance record for transforming Rabin automata into parity automata","arxiv":1,"language":[{"iso":"eng"}],"conference":{"end_date":"2017-04-29","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Uppsala, Sweden"},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783662545768"],"eisbn":["9783662545775"]},"quality_controlled":"1","doi":"10.1007/978-3-662-54577-5_26"},{"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"isi":1,"issue":"2","language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2016.04.006","quality_controlled":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publisher":"Elsevier","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication":"Nonlinear Analysis: Hybrid Systems","scopus_import":"1","ec_funded":1,"article_processing_charge":"No","author":[{"last_name":"Svoreňová","first_name":"Mária","full_name":"Svoreňová, Mária"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Cěrná, Ivana","last_name":"Cěrná","first_name":"Ivana"},{"first_name":"Cǎlin","last_name":"Belta","full_name":"Belta, Cǎlin"}],"day":"01","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","arxiv":1,"publist_id":"5800","external_id":{"arxiv":["1410.5387"],"isi":["000390637000014"]},"status":"public","related_material":{"record":[{"id":"1689","status":"public","relation":"earlier_version"}]},"intvolume":" 23","citation":{"apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2. Elsevier, pp. 230–253, 2017."},"publication_status":"published","oa":1,"date_published":"2017-02-01T00:00:00Z","main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"year":"2017","_id":"1407","page":"230 - 253","oa_version":"Preprint","type":"journal_article","month":"02","abstract":[{"text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.","lang":"eng"}],"date_updated":"2023-09-20T09:43:09Z","volume":23,"date_created":"2018-12-11T11:51:50Z"},{"publication_status":"published","oa":1,"has_accepted_license":"1","date_published":"2016-08-01T00:00:00Z","ddc":["004"],"alternative_title":["LIPIcs"],"status":"public","related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"intvolume":" 59","citation":{"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:10.4230/LIPIcs.CONCUR.2016.20","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., & 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. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20","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. Linear Distances between Markov Chains. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.","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. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.","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.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"date_updated":"2023-09-07T11:58:33Z","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"}],"type":"conference","oa_version":"Published Version","month":"08","volume":59,"file_date_updated":"2018-12-12T10:11:39Z","date_created":"2018-12-11T11:50:06Z","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","_id":"1093","pubrep_id":"794","doi":"10.4230/LIPIcs.CONCUR.2016.20","quality_controlled":"1","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"conference":{"location":"Quebec City; Canada","name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","end_date":"2016-08-26"},"language":[{"iso":"eng"}],"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"},{"last_name":"Petrov","first_name":"Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"file":[{"file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","relation":"main_file","content_type":"application/pdf","file_size":501827,"creator":"system","date_updated":"2018-12-12T10:11:39Z","file_id":"4895","date_created":"2018-12-12T10:11:39Z","access_level":"open_access"}],"day":"01","title":"Linear distances between Markov chains","article_number":"20","publist_id":"6283","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"scopus_import":1,"ec_funded":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"}},{"language":[{"iso":"eng"}],"conference":{"end_date":"2016-04-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Eindhoven, The Netherlands","start_date":"2016-04-02"},"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"quality_controlled":"1","doi":"10.1007/978-3-662-49674-9_7","scopus_import":1,"ec_funded":1,"department":[{"_id":"ToHe"},{"_id":"CaGu"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","publist_id":"6099","title":"Faster statistical model checking for unbounded temporal properties","day":"01","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Tatjana","last_name":"Petrov","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"citation":{"ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","mla":"Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7."},"intvolume":" 9636","related_material":{"record":[{"relation":"later_version","id":"471","status":"public"},{"status":"public","id":"1155","relation":"dissertation_contains"}]},"status":"public","alternative_title":["LNCS"],"main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"date_published":"2016-01-01T00:00:00Z","publication_status":"published","oa":1,"_id":"1234","year":"2016","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","date_created":"2018-12-11T11:50:51Z","volume":9636,"abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.","lang":"eng"}],"date_updated":"2023-09-07T11:58:33Z","type":"conference","oa_version":"Preprint","month":"01","page":"112 - 129"},{"alternative_title":["LICS"],"status":"public","related_material":{"record":[{"relation":"later_version","status":"public","id":"466"},{"relation":"earlier_version","status":"public","id":"5429"},{"relation":"earlier_version","status":"public","id":"5435"}]},"citation":{"ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:10.1109/LICS.2015.32","mla":"Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IEEE, 2015, pp. 244–56, doi:10.1109/LICS.2015.32.","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","apa":"Chatterjee, K., Komárková, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.32","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.","chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. https://doi.org/10.1109/LICS.2015.32.","short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256."},"publication_status":"published","date_published":"2015-07-01T00:00:00Z","acknowledgement":"A Technical Report of this paper is available at: https://repository.ist.ac.at/327\r\n","year":"2015","_id":"1657","page":"244 - 256","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"date_updated":"2023-02-23T12:26:16Z","oa_version":"None","month":"07","type":"conference","date_created":"2018-12-11T11:53:18Z","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"series_title":"LICS","conference":{"location":"Kyoto, Japan","name":"LICS: Logic in Computer Science","start_date":"2015-07-06","end_date":"2015-07-10"},"language":[{"iso":"eng"}],"doi":"10.1109/LICS.2015.32","quality_controlled":"1","publisher":"IEEE","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":1,"ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Komárková, Zuzana","last_name":"Komárková","first_name":"Zuzana"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"day":"01","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","publist_id":"5493"},{"author":[{"full_name":"Svoreňová, Mária","first_name":"Mária","last_name":"Svoreňová"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","last_name":"Kretinsky","first_name":"Jan"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Cěrná","first_name":"Ivana","full_name":"Cěrná, Ivana"},{"first_name":"Cǎlin","last_name":"Belta","full_name":"Belta, Cǎlin"}],"page":"259 - 268","oa_version":"Preprint","month":"04","type":"conference","day":"14","date_updated":"2023-09-20T09:43:09Z","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study."}],"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","publist_id":"5456","date_created":"2018-12-11T11:53:29Z","publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"year":"2015","_id":"1689","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","ec_funded":1,"scopus_import":1,"oa":1,"publication_status":"published","date_published":"2015-04-14T00:00:00Z","doi":"10.1145/2728606.2728608","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"project":[{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"status":"public","conference":{"end_date":"2015-04-16","name":"HSCC: Hybrid Systems - Computation and Control","location":"Seattle, WA, United States","start_date":"2015-04-14"},"related_material":{"record":[{"status":"public","id":"1407","relation":"later_version"}]},"language":[{"iso":"eng"}],"citation":{"chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728608","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608."}},{"language":[{"iso":"eng"}],"issue":"2-3","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"doi":"10.1007/s00236-015-0215-4","quality_controlled":"1","publication":"Acta Informatica","article_processing_charge":"No","ec_funded":1,"scopus_import":1,"article_type":"original","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Refinement checking on parametric modal transition systems","publist_id":"5255","author":[{"first_name":"Nikola","last_name":"Beneš","full_name":"Beneš, Nikola"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Larsen, Kim","first_name":"Kim","last_name":"Larsen"},{"last_name":"Möller","first_name":"Mikael","full_name":"Möller, Mikael"},{"full_name":"Sickert, Salomon","last_name":"Sickert","first_name":"Salomon"},{"full_name":"Srba, Jiří","first_name":"Jiří","last_name":"Srba"}],"file":[{"date_created":"2020-05-15T08:57:44Z","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","file_id":"7854","checksum":"fb4037ddc4fc05f33080dd3547ede350","relation":"main_file","content_type":"application/pdf","file_size":488482,"creator":"dernst","file_name":"2015_ActaInfo_Benes.pdf"}],"day":"01","intvolume":" 52","citation":{"short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” Acta Informatica, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba, J. (2015). Refinement checking on parametric modal transition systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4","ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297. doi:10.1007/s00236-015-0215-4"},"status":"public","ddc":["000"],"date_published":"2015-04-01T00:00:00Z","oa":1,"publication_status":"published","has_accepted_license":"1","_id":"1846","year":"2015","volume":52,"file_date_updated":"2020-07-14T12:45:19Z","date_created":"2018-12-11T11:54:20Z","page":"269 - 297","date_updated":"2021-01-12T06:53:35Z","abstract":[{"lang":"eng","text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS."}],"type":"journal_article","oa_version":"Submitted Version","month":"04"},{"intvolume":" 8997","citation":{"ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. https://doi.org/10.1007/978-3-319-15317-9_19.","short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:10.1007/978-3-319-15317-9_19","mla":"Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications. Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.","ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., & Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. https://doi.org/10.1007/978-3-319-15317-9_19"},"alternative_title":["LNCS"],"status":"public","date_published":"2015-01-30T00:00:00Z","main_file_link":[{"url":"http://arxiv.org/abs/1408.1256","open_access":"1"}],"oa":1,"publication_status":"published","_id":"1882","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","year":"2015","volume":8997,"date_created":"2018-12-11T11:54:31Z","page":"306 - 324","abstract":[{"text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.","lang":"eng"}],"date_updated":"2021-01-12T06:53:49Z","oa_version":"Preprint","type":"conference","month":"01","conference":{"location":"Bertinoro, Italy","name":"FACS: Formal Aspects of Component Software","start_date":"2014-09-10","end_date":"2014-09-12"},"language":[{"iso":"eng"}],"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"doi":"10.1007/978-3-319-15317-9_19","quality_controlled":"1","scopus_import":1,"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Compositionality for quantitative specifications","publist_id":"5216","author":[{"full_name":"Fahrenberg, Uli","first_name":"Uli","last_name":"Fahrenberg"},{"first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Legay, Axel","first_name":"Axel","last_name":"Legay"},{"full_name":"Traonouez, Louis","first_name":"Louis","last_name":"Traonouez"}],"day":"30"},{"year":"2015","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","_id":"5429","month":"01","type":"technical_report","oa_version":"Published Version","file":[{"file_size":689863,"content_type":"application/pdf","relation":"main_file","creator":"system","file_name":"IST-2015-318-v1+1_main.pdf","date_created":"2018-12-12T11:54:11Z","access_level":"open_access","file_id":"5533","date_updated":"2020-07-14T12:46:52Z","checksum":"e4869a584567c506349abda9c8ec7db3"}],"date_updated":"2023-02-23T12:26:16Z","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics.\r\nOur problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions.\r\nFinally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem."}],"day":"12","page":"41","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Komarkova","first_name":"Zuzana","full_name":"Komarkova, Zuzana"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"file_date_updated":"2020-07-14T12:46:52Z","date_created":"2018-12-12T11:39:17Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","status":"public","alternative_title":["IST Austria Technical Report"],"citation":{"mla":"Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1.","ista":"Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p.","apa":"Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2015-318-v1-1","ama":"Chatterjee K, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v1-1","short":"K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.","ieee":"K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v1-1."},"language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"later_version","id":"1657","status":"public"},{"status":"public","id":"466","relation":"later_version"},{"id":"5435","status":"public","relation":"later_version"}]},"has_accepted_license":"1","pubrep_id":"318","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","oa":1,"doi":"10.15479/AT:IST-2015-318-v1-1","ddc":["004"],"date_published":"2015-01-12T00:00:00Z"},{"has_accepted_license":"1","pubrep_id":"327","oa":1,"publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"date_published":"2015-02-23T00:00:00Z","ddc":["004"],"doi":"10.15479/AT:IST-2015-318-v2-1","status":"public","alternative_title":["IST Austria Technical Report"],"citation":{"ieee":"K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v2-1.","short":"K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015.","ama":"Chatterjee K, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v2-1","ista":"Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 51p.","mla":"Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.","apa":"Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2015-318-v2-1"},"language":[{"iso":"eng"}],"related_material":{"record":[{"id":"1657","status":"public","relation":"later_version"},{"status":"public","id":"466","relation":"later_version"},{"relation":"earlier_version","status":"public","id":"5429"}]},"date_updated":"2023-02-23T12:26:00Z","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP.\r\nWe also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Finally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem.","lang":"eng"}],"day":"23","file":[{"relation":"main_file","content_type":"application/pdf","file_size":717630,"creator":"system","file_name":"IST-2015-318-v2+1_main.pdf","date_created":"2018-12-12T11:54:03Z","access_level":"open_access","date_updated":"2020-07-14T12:46:53Z","file_id":"5525","checksum":"75284adec80baabdfe71ff9ebbc27445"}],"oa_version":"Published Version","type":"technical_report","month":"02","page":"51","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Zuzana","last_name":"Komarkova","full_name":"Komarkova, Zuzana"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan"}],"file_date_updated":"2020-07-14T12:46:53Z","date_created":"2018-12-12T11:39:19Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","department":[{"_id":"KrCh"}],"year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","_id":"5435"},{"date_published":"2015-01-01T00:00:00Z","ddc":["000","003"],"has_accepted_license":"1","oa":1,"publication_status":"published","citation":{"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. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.","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.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, 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:10.4230/LIPIcs.CONCUR.2015.142","apa":"Kretinsky, J., Larsen, K., Laursen, S., & 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. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142","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.","mla":"Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142."},"intvolume":" 42","status":"public","alternative_title":["LIPIcs"],"date_created":"2018-12-11T11:52:22Z","file_date_updated":"2020-07-14T12:44:58Z","volume":42,"abstract":[{"lang":"eng","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."}],"date_updated":"2021-01-12T06:51:10Z","month":"01","type":"conference","oa_version":"Published Version","page":"142 - 154","_id":"1499","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.","quality_controlled":"1","doi":"10.4230/LIPIcs.CONCUR.2015.142","pubrep_id":"498","language":[{"iso":"eng"}],"conference":{"end_date":"2015-09-04","name":"CONCUR: Concurrency Theory","location":"Madrid, Spain","start_date":"2015-09-01"},"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"publist_id":"5680","title":"Polynomial time decidability of weighted synchronization under partial observability","file":[{"date_updated":"2020-07-14T12:44:58Z","file_id":"4672","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","date_created":"2018-12-12T10:08:12Z","access_level":"open_access","file_name":"IST-2016-498-v1+1_32.pdf","content_type":"application/pdf","relation":"main_file","file_size":623563,"creator":"system"}],"day":"01","author":[{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Kim","last_name":"Larsen","full_name":"Larsen, Kim"},{"first_name":"Simon","last_name":"Laursen","full_name":"Laursen, Simon"},{"full_name":"Srba, Jiří","first_name":"Jiří","last_name":"Srba"}],"ec_funded":1,"scopus_import":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"ACM","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"ec_funded":1,"scopus_import":1,"author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"}],"day":"01","file":[{"date_created":"2018-12-12T10:17:46Z","access_level":"open_access","file_id":"5303","date_updated":"2020-07-14T12:44:59Z","checksum":"c6ce681035c163a158751f240cb7d389","file_size":467561,"relation":"main_file","content_type":"application/pdf","creator":"system","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf"}],"title":"Complete composition operators for IOCO-testing theory","publist_id":"5676","project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"conference":{"start_date":"2015-05-04","name":"CBSE: Component-Based Software Engineering ","location":"Montreal, QC, Canada","end_date":"2015-05-08"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-3471-6"]},"pubrep_id":"625","doi":"10.1145/2737166.2737175","quality_controlled":"1","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.","year":"2015","_id":"1502","page":"101 - 110","oa_version":"Submitted Version","type":"conference","month":"05","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"}],"date_updated":"2023-09-07T11:58:33Z","file_date_updated":"2020-07-14T12:44:59Z","date_created":"2018-12-11T11:52:24Z","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"status":"public","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"1155"}]},"citation":{"short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 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. https://doi.org/10.1145/2737166.2737175.","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.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & 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. https://doi.org/10.1145/2737166.2737175","mla":"Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.","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.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175"},"oa":1,"publication_status":"published","has_accepted_license":"1","date_published":"2015-05-01T00:00:00Z","ddc":["000"]}]