--- _id: '14259' abstract: - lang: eng 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." acknowledgement: This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro). alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Maximilian full_name: Prokop, Maximilian last_name: Prokop - first_name: Sabine full_name: Rieder, Sabine last_name: Rieder citation: 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' 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' 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. 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.' 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. short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414. conference: end_date: 2023-07-22 location: Paris, France name: 'CAV: Computer Aided Verification' start_date: 2023-07-17 date_created: 2023-09-03T22:01:16Z date_published: 2023-07-17T00:00:00Z date_updated: 2023-09-06T08:27:33Z day: '17' ddc: - '000' department: - _id: KrCh doi: 10.1007/978-3-031-37706-8_20 file: - access_level: open_access checksum: ed66278b61bb869e1baba3d9b9081271 content_type: application/pdf creator: dernst date_created: 2023-09-06T08:25:50Z date_updated: 2023-09-06T08:25:50Z file_id: '14276' file_name: 2023_LNCS_CAV_Kretinsky.pdf file_size: 428354 relation: main_file success: 1 file_date_updated: 2023-09-06T08:25:50Z has_accepted_license: '1' intvolume: ' 13964' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: 390-414 publication: '35th International Conference on Computer Aided Verification ' publication_identifier: eissn: - 1611-3349 isbn: - '9783031377051' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Guessing winning policies in LTL synthesis by semantic learning tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13964 year: '2023' ... --- _id: '13967' 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.' acknowledgement: This research was funded in part by DFG projects 383882557 “SUV” and 427755713 “GOPro”. article_processing_charge: No author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger citation: 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' 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' 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. 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. 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. 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. conference: end_date: 2023-06-29 location: Boston, MA, United States name: 'LICS: Symposium on Logic in Computer Science' start_date: 2023-06-26 date_created: 2023-08-06T22:01:10Z date_published: 2023-07-01T00:00:00Z date_updated: 2023-12-13T12:06:10Z day: '01' department: - _id: KrCh doi: 10.1109/LICS56636.2023.10175771 external_id: arxiv: - '2304.09930' isi: - '001036707700042' intvolume: ' 2023' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2304.09930 month: '07' oa: 1 oa_version: Preprint publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science publication_identifier: isbn: - '9798350335873' issn: - 1043-6871 publication_status: published publisher: Institute of Electrical and Electronics Engineers quality_controlled: '1' scopus_import: '1' status: public title: Stopping criteria for value iteration on stochastic games with quantitative objectives type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 2023 year: '2023' ... --- _id: '10602' 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. 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. article_processing_charge: Yes (via OA deal) article_type: original author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Clara full_name: Waldmann, Clara last_name: Waldmann - first_name: Maximilian full_name: Weininger, Maximilian last_name: Weininger citation: 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 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 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. 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. short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618. date_created: 2022-01-06T12:37:27Z date_published: 2022-10-01T00:00:00Z date_updated: 2023-08-02T13:49:28Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1007/s00236-021-00412-y external_id: isi: - '000735765500001' file: - access_level: open_access checksum: bf1c195b6aaf59e8530cf9e3a9d731f7 content_type: application/pdf creator: cchlebak date_created: 2022-01-07T07:50:31Z date_updated: 2022-01-07T07:50:31Z file_id: '10603' file_name: 2021_ActaInfor_Křetínský.pdf file_size: 1066082 relation: main_file success: 1 file_date_updated: 2022-01-07T07:50:31Z has_accepted_license: '1' intvolume: ' 59' isi: 1 keyword: - computer networks and communications - information systems - software language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 585-618 project: - _id: B67AFEDC-15C9-11EA-A837-991A96BB2854 name: IST Austria Open Access Fund publication: Acta Informatica publication_identifier: eissn: - 1432-0525 issn: - 0001-5903 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Index appearance record with preorders tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 59 year: '2022' ... --- _id: '12775' abstract: - lang: eng 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." 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)" alternative_title: - LIPIcs article_number: '11' article_processing_charge: No author: - first_name: Kush full_name: Grover, Kush last_name: Grover - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Maimilian full_name: Weininger, Maimilian last_name: Weininger citation: 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' 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' 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. 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. 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. short: K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International Conference on Concurrency Theory , Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. conference: end_date: 2022-09-16 location: Warsaw, Poland name: 'CONCUR: Conference on Concurrency Theory' start_date: 2022-09-13 date_created: 2023-03-28T08:09:32Z date_published: 2022-09-15T00:00:00Z date_updated: 2023-09-26T10:43:30Z day: '15' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.CONCUR.2022.11 external_id: arxiv: - '2008.04824' file: - access_level: open_access checksum: e282e43d3ae0ba6e067b72f4583e13c0 content_type: application/pdf creator: dernst date_created: 2023-09-26T10:43:15Z date_updated: 2023-09-26T10:43:15Z file_id: '14372' file_name: 2022_LIPIcS_Grover.pdf file_size: 960036 relation: main_file success: 1 file_date_updated: 2023-09-26T10:43:15Z has_accepted_license: '1' intvolume: ' 243' language: - iso: eng month: '09' oa: 1 oa_version: Published Version publication: '33rd International Conference on Concurrency Theory ' publication_identifier: issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: Anytime guarantees for reachability in uncountable Markov decision processes tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 243 year: '2022' ... --- _id: '297' 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. alternative_title: - LNCS article_processing_charge: No author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Viktor full_name: Toman, Viktor id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87 last_name: Toman orcid: 0000-0001-9036-063X citation: 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' 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' 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.' 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. short: T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407. conference: end_date: 2018-04-20 location: Thessaloniki, Greece name: 'TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2018-04-14 date_created: 2018-12-11T11:45:41Z date_published: 2018-04-12T00:00:00Z date_updated: 2023-09-19T09:57:08Z day: '12' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-89960-2_21 ec_funded: 1 external_id: isi: - '000546326300021' file: - access_level: open_access checksum: b13874ffb114932ad9cc2586b7469db4 content_type: application/pdf creator: dernst date_created: 2018-12-17T16:29:08Z date_updated: 2020-07-14T12:45:57Z file_id: '5723' file_name: 2018_LNCS_Brazdil.pdf file_size: 1829940 relation: main_file file_date_updated: 2020-07-14T12:45:57Z has_accepted_license: '1' intvolume: ' 10805' isi: 1 language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: 385 - 407 project: - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2564DBCA-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '665385' name: International IST Doctoral Program publication_status: published publisher: Springer publist_id: '7584' quality_controlled: '1' scopus_import: '1' status: public title: Strategy representation by decision trees in reactive synthesis tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 10805 year: '2018' ... --- _id: '471' abstract: - lang: eng 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. ' article_number: '12' author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tatjana full_name: Petrov, Tatjana id: 3D5811FC-F248-11E8-B48F-1D18A9856A87 last_name: Petrov orcid: 0000-0002-9041-0905 citation: 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 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 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. 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. 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. 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. short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017). date_created: 2018-12-11T11:46:39Z date_published: 2017-05-01T00:00:00Z date_updated: 2023-02-21T16:48:11Z day: '01' department: - _id: ToHe doi: 10.1145/3060139 ec_funded: 1 intvolume: ' 18' issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1504.05739 month: '05' oa: 1 oa_version: Submitted Version project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication: ACM Transactions on Computational Logic (TOCL) publication_identifier: issn: - '15293785' publication_status: published publisher: ACM publist_id: '7349' quality_controlled: '1' related_material: record: - id: '1234' relation: earlier_version status: public scopus_import: 1 status: public title: Faster statistical model checking for unbounded temporal properties type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 18 year: '2017' ... --- _id: '466' 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. ' article_number: '15' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Zuzana full_name: Křetínská, Zuzana last_name: Křetínská - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: 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 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 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. 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. 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. 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. short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017). date_created: 2018-12-11T11:46:38Z date_published: 2017-07-03T00:00:00Z date_updated: 2023-02-23T12:26:16Z day: '03' ddc: - '004' department: - _id: KrCh doi: 10.23638/LMCS-13(2:15)2017 ec_funded: 1 file: - access_level: open_access checksum: bfa405385ec6229ad5ead89ab5751639 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:32Z date_updated: 2020-07-14T12:46:33Z file_id: '5354' file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf file_size: 511832 relation: main_file file_date_updated: 2020-07-14T12:46:33Z has_accepted_license: '1' intvolume: ' 13' issue: '2' language: - iso: eng license: https://creativecommons.org/licenses/by-nd/4.0/ month: '07' oa: 1 oa_version: Published Version project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2590DB08-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '701309' name: Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020) publication: Logical Methods in Computer Science publication_identifier: issn: - '18605974' publication_status: published publisher: International Federation of Computational Logic publist_id: '7355' pubrep_id: '957' quality_controlled: '1' related_material: record: - id: '1657' relation: earlier_version status: public - id: '5429' relation: earlier_version status: public - id: '5435' relation: earlier_version status: public scopus_import: 1 status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes tmp: image: /image/cc_by_nd.png legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0) short: CC BY-ND (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13 year: '2017' ... --- _id: '645' abstract: - lang: eng 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. alternative_title: - LNCS author: - first_name: Pranav full_name: Ashok, Pranav last_name: Ashok - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias last_name: Meggendorfer citation: 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' 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' 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. 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.' 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.' 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. short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221. conference: end_date: 2017-07-28 location: Heidelberg, Germany name: 'CAV: Computer Aided Verification' start_date: 2017-07-24 date_created: 2018-12-11T11:47:41Z date_published: 2017-07-13T00:00:00Z date_updated: 2021-01-12T08:07:32Z day: '13' department: - _id: KrCh doi: 10.1007/978-3-319-63387-9_10 ec_funded: 1 editor: - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar - first_name: Viktor full_name: Kunčak, Viktor last_name: Kunčak intvolume: ' 10426' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1705.02326 month: '07' oa: 1 oa_version: Submitted Version page: 201 - 221 project: - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_identifier: isbn: - 978-331963386-2 publication_status: published publisher: Springer publist_id: '7135' quality_controlled: '1' scopus_import: 1 status: public title: Value iteration for long run average reward in markov decision processes type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 10426 year: '2017' ... --- _id: '13160' abstract: - lang: eng 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." acknowledgement: This work is partially funded by the DFG project “Verified Model Checkers” and by the Czech Science Foundation, grant No. P202/12/G061. alternative_title: - LNCS article_processing_charge: No author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Clara full_name: Waldmann, Clara last_name: Waldmann - first_name: Maximilian full_name: Weininger, Maximilian last_name: Weininger citation: 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' 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' 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. 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. 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.' 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. 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. conference: end_date: 2017-04-29 location: Uppsala, Sweden name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2017-04-22 date_created: 2023-06-21T13:21:14Z date_published: 2017-03-31T00:00:00Z date_updated: 2023-06-21T13:29:46Z day: '31' department: - _id: KrCh doi: 10.1007/978-3-662-54577-5_26 external_id: arxiv: - '1701.05738' intvolume: ' 10205' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.1701.05738 month: '03' oa: 1 oa_version: Preprint page: 443-460 publication: Tools and Algorithms for the Construction and Analysis of Systems publication_identifier: eisbn: - '9783662545775' eissn: - 1611-3349 isbn: - '9783662545768' issn: - 0302-9743 publication_status: published publisher: Springer quality_controlled: '1' status: public title: Index appearance record for transforming Rabin automata into parity automata type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 10205 year: '2017' ... --- _id: '1407' abstract: - lang: eng text: We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study. article_processing_charge: No author: - first_name: Mária full_name: Svoreňová, Mária last_name: Svoreňová - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ivana full_name: Cěrná, Ivana last_name: Cěrná - first_name: Cǎlin full_name: Belta, Cǎlin last_name: Belta citation: ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006' apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006' chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.' ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.' ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.' mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.' short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.' date_created: 2018-12-11T11:51:50Z date_published: 2017-02-01T00:00:00Z date_updated: 2023-09-20T09:43:09Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1016/j.nahs.2016.04.006 ec_funded: 1 external_id: arxiv: - '1410.5387' isi: - '000390637000014' intvolume: ' 23' isi: 1 issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1410.5387 month: '02' oa: 1 oa_version: Preprint page: 230 - 253 project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: 'Nonlinear Analysis: Hybrid Systems' publication_status: published publisher: Elsevier publist_id: '5800' quality_controlled: '1' related_material: record: - id: '1689' relation: earlier_version status: public scopus_import: '1' status: public title: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 23 year: '2017' ... --- _id: '1093' abstract: - lang: eng 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. ' 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." alternative_title: - LIPIcs article_number: '20' author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tatjana full_name: Petrov, Tatjana id: 3D5811FC-F248-11E8-B48F-1D18A9856A87 last_name: Petrov orcid: 0000-0002-9041-0905 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' 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.' 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. short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. conference: end_date: 2016-08-26 location: Quebec City; Canada name: 'CONCUR: Concurrency Theory' start_date: 2016-08-23 date_created: 2018-12-11T11:50:06Z date_published: 2016-08-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' ddc: - '004' department: - _id: ToHe - _id: KrCh - _id: CaGu doi: 10.4230/LIPIcs.CONCUR.2016.20 ec_funded: 1 file: - access_level: open_access content_type: application/pdf creator: system date_created: 2018-12-12T10:11:39Z date_updated: 2018-12-12T10:11:39Z file_id: '4895' file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf file_size: 501827 relation: main_file file_date_updated: 2018-12-12T10:11:39Z has_accepted_license: '1' intvolume: ' 59' language: - iso: eng month: '08' oa: 1 oa_version: Published Version project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '6283' pubrep_id: '794' quality_controlled: '1' related_material: record: - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: Linear distances between Markov chains tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 59 year: '2016' ... --- _id: '1234' abstract: - lang: eng 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. 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." alternative_title: - LNCS author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tatjana full_name: Petrov, Tatjana id: 3D5811FC-F248-11E8-B48F-1D18A9856A87 last_name: Petrov orcid: 0000-0002-9041-0905 citation: 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' 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' 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. 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.' 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. short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129. conference: end_date: 2016-04-08 location: Eindhoven, The Netherlands name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2016-04-02 date_created: 2018-12-11T11:50:51Z date_published: 2016-01-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: ToHe - _id: CaGu doi: 10.1007/978-3-662-49674-9_7 ec_funded: 1 intvolume: ' 9636' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1504.05739 month: '01' oa: 1 oa_version: Preprint page: 112 - 129 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_status: published publisher: Springer publist_id: '6099' quality_controlled: '1' related_material: record: - id: '471' relation: later_version status: public - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: Faster statistical model checking for unbounded temporal properties type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 9636 year: '2016' ... --- _id: '1499' 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." 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." alternative_title: - LIPIcs author: - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Kim full_name: Larsen, Kim last_name: Larsen - first_name: Simon full_name: Laursen, Simon last_name: Laursen - first_name: Jiří full_name: Srba, Jiří last_name: Srba citation: 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' 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.' 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. short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154. conference: end_date: 2015-09-04 location: Madrid, Spain name: 'CONCUR: Concurrency Theory' start_date: 2015-09-01 date_created: 2018-12-11T11:52:22Z date_published: 2015-01-01T00:00:00Z date_updated: 2021-01-12T06:51:10Z day: '01' ddc: - '000' - '003' department: - _id: ToHe - _id: KrCh doi: 10.4230/LIPIcs.CONCUR.2015.142 ec_funded: 1 file: - access_level: open_access checksum: 49eb5021caafaabe5356c65b9c5f8c9c content_type: application/pdf creator: system date_created: 2018-12-12T10:08:12Z date_updated: 2020-07-14T12:44:58Z file_id: '4672' file_name: IST-2016-498-v1+1_32.pdf file_size: 623563 relation: main_file file_date_updated: 2020-07-14T12:44:58Z has_accepted_license: '1' intvolume: ' 42' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: 142 - 154 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '5680' pubrep_id: '498' quality_controlled: '1' scopus_import: 1 status: public title: Polynomial time decidability of weighted synchronization under partial observability tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 42 year: '2015' ... --- _id: '1594' abstract: - lang: eng text: Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata. acknowledgement: "This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n" alternative_title: - LNCS author: - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Krčál, Jan last_name: Krčál - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12' apa: 'Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. https://doi.org/10.1007/978-3-662-48899-7_12' chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12. ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.' ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.' mla: Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU. Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12. short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177. conference: end_date: 2015-11-28 location: Suva, Fiji name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning' start_date: 2015-11-24 date_created: 2018-12-11T11:52:55Z date_published: 2015-11-22T00:00:00Z date_updated: 2021-01-12T06:51:50Z day: '22' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-662-48899-7_12 ec_funded: 1 intvolume: ' 9450' language: - iso: eng month: '11' oa_version: None page: 162 - 177 project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: Springer publist_id: '5577' quality_controlled: '1' scopus_import: 1 status: public title: Controller synthesis for MDPs and frequency LTL\GU type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 9450 year: '2015' ... --- _id: '1601' abstract: - lang: eng text: We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata. alternative_title: - LNCS article_processing_charge: No author: - first_name: Tomáš full_name: Babiak, Tomáš last_name: Babiak - first_name: František full_name: Blahoudek, František last_name: Blahoudek - first_name: Alexandre full_name: Duret Lutz, Alexandre last_name: Duret Lutz - first_name: Joachim full_name: Klein, Joachim last_name: Klein - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Daniel full_name: Mueller, Daniel last_name: Mueller - first_name: David full_name: Parker, David last_name: Parker - first_name: Jan full_name: Strejček, Jan last_name: Strejček citation: ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31' apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_31' chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_31. ieee: 'T. Babiak et al., “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.' ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.' mla: Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer, 2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31. short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486. conference: end_date: 2015-07-24 location: San Francisco, CA, United States name: 'CAV: Computer Aided Verification' start_date: 2015-07-18 date_created: 2018-12-11T11:52:57Z date_published: 2015-07-16T00:00:00Z date_updated: 2021-01-12T06:51:54Z day: '16' ddc: - '000' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-319-21690-4_31 ec_funded: 1 file: - access_level: open_access checksum: 5885236fa88a439baba9ac6f3e801e93 content_type: application/pdf creator: dernst date_created: 2020-05-15T08:38:12Z date_updated: 2020-07-14T12:45:04Z file_id: '7850' file_name: 2015_CAV_Babiak.pdf file_size: 1651779 relation: main_file file_date_updated: 2020-07-14T12:45:04Z has_accepted_license: '1' intvolume: ' 9206' language: - iso: eng month: '07' oa: 1 oa_version: Submitted Version page: 479 - 486 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '5566' quality_controlled: '1' scopus_import: 1 status: public title: The Hanoi omega-automata format type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 9206 year: '2015' ... --- _id: '1846' abstract: - lang: eng text: Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS. article_processing_charge: No article_type: original author: - first_name: Nikola full_name: Beneš, Nikola last_name: Beneš - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Kim full_name: Larsen, Kim last_name: Larsen - first_name: Mikael full_name: Möller, Mikael last_name: Möller - first_name: Salomon full_name: Sickert, Salomon last_name: Sickert - first_name: Jiří full_name: Srba, Jiří last_name: Srba citation: 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 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 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. 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. short: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297. date_created: 2018-12-11T11:54:20Z date_published: 2015-04-01T00:00:00Z date_updated: 2021-01-12T06:53:35Z day: '01' ddc: - '000' department: - _id: ToHe - _id: KrCh doi: 10.1007/s00236-015-0215-4 ec_funded: 1 file: - access_level: open_access checksum: fb4037ddc4fc05f33080dd3547ede350 content_type: application/pdf creator: dernst date_created: 2020-05-15T08:57:44Z date_updated: 2020-07-14T12:45:19Z file_id: '7854' file_name: 2015_ActaInfo_Benes.pdf file_size: 488482 relation: main_file file_date_updated: 2020-07-14T12:45:19Z has_accepted_license: '1' intvolume: ' 52' issue: 2-3 language: - iso: eng month: '04' oa: 1 oa_version: Submitted Version page: 269 - 297 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: Acta Informatica publication_status: published publisher: Springer publist_id: '5255' quality_controlled: '1' scopus_import: 1 status: public title: Refinement checking on parametric modal transition systems type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 52 year: '2015' ... --- _id: '1882' abstract: - lang: eng 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. 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. alternative_title: - LNCS author: - first_name: Uli full_name: Fahrenberg, Uli last_name: Fahrenberg - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Axel full_name: Legay, Axel last_name: Legay - first_name: Louis full_name: Traonouez, Louis last_name: Traonouez citation: 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' 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' 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. ieee: 'U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.' ista: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.' mla: Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications. Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19. short: U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324. conference: end_date: 2014-09-12 location: Bertinoro, Italy name: 'FACS: Formal Aspects of Component Software' start_date: 2014-09-10 date_created: 2018-12-11T11:54:31Z date_published: 2015-01-30T00:00:00Z date_updated: 2021-01-12T06:53:49Z day: '30' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-319-15317-9_19 ec_funded: 1 intvolume: ' 8997' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1408.1256 month: '01' oa: 1 oa_version: Preprint page: 306 - 324 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '5216' quality_controlled: '1' scopus_import: 1 status: public title: Compositionality for quantitative specifications type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8997 year: '2015' ... --- _id: '1657' 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. ' acknowledgement: "A Technical Report of this paper is available at: https://repository.ist.ac.at/327\r\n" alternative_title: - LICS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Zuzana full_name: Komárková, Zuzana last_name: Komárková - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 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 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' 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. 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. ista: Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256. 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. short: K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256. conference: end_date: 2015-07-10 location: Kyoto, Japan name: 'LICS: Logic in Computer Science' start_date: 2015-07-06 date_created: 2018-12-11T11:53:18Z date_published: 2015-07-01T00:00:00Z date_updated: 2023-02-23T12:26:16Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1109/LICS.2015.32 ec_funded: 1 language: - iso: eng month: '07' oa_version: None page: 244 - 256 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_status: published publisher: IEEE publist_id: '5493' quality_controlled: '1' related_material: record: - id: '466' relation: later_version status: public - id: '5429' relation: earlier_version status: public - id: '5435' relation: earlier_version status: public scopus_import: 1 series_title: LICS status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5429' 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." alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Zuzana full_name: Komarkova, Zuzana last_name: Komarkova - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: 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 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 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. ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015. ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p. 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. short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015. date_created: 2018-12-12T11:39:17Z date_published: 2015-01-12T00:00:00Z date_updated: 2023-02-23T12:26:16Z day: '12' ddc: - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2015-318-v1-1 file: - access_level: open_access checksum: e4869a584567c506349abda9c8ec7db3 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:11Z date_updated: 2020-07-14T12:46:52Z file_id: '5533' file_name: IST-2015-318-v1+1_main.pdf file_size: 689863 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '41' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '318' related_material: record: - id: '1657' relation: later_version status: public - id: '466' relation: later_version status: public - id: '5435' relation: later_version status: public status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5435' 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. 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." alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Zuzana full_name: Komarkova, Zuzana last_name: Komarkova - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: 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 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 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. ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015. 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. short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015. date_created: 2018-12-12T11:39:19Z date_published: 2015-02-23T00:00:00Z date_updated: 2023-02-23T12:26:00Z day: '23' ddc: - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2015-318-v2-1 file: - access_level: open_access checksum: 75284adec80baabdfe71ff9ebbc27445 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:03Z date_updated: 2020-07-14T12:46:53Z file_id: '5525' file_name: IST-2015-318-v2+1_main.pdf file_size: 717630 relation: main_file file_date_updated: 2020-07-14T12:46:53Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '51' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '327' related_material: record: - id: '1657' relation: later_version status: public - id: '466' relation: later_version status: public - id: '5429' relation: earlier_version status: public status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1502' abstract: - lang: eng 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. 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." alternative_title: - 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering ' author: - first_name: Nikola full_name: Beneš, Nikola last_name: Beneš - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Dejan full_name: Nickovic, Dejan last_name: Nickovic citation: 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' 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' 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.' 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.' mla: Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175. short: N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110. conference: end_date: 2015-05-08 location: Montreal, QC, Canada name: 'CBSE: Component-Based Software Engineering ' start_date: 2015-05-04 date_created: 2018-12-11T11:52:24Z date_published: 2015-05-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' ddc: - '000' department: - _id: ToHe - _id: KrCh doi: 10.1145/2737166.2737175 ec_funded: 1 file: - access_level: open_access checksum: c6ce681035c163a158751f240cb7d389 content_type: application/pdf creator: system date_created: 2018-12-12T10:17:46Z date_updated: 2020-07-14T12:44:59Z file_id: '5303' file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf file_size: 467561 relation: main_file file_date_updated: 2020-07-14T12:44:59Z has_accepted_license: '1' language: - iso: eng month: '05' oa: 1 oa_version: Submitted Version page: 101 - 110 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_identifier: isbn: - 978-1-4503-3471-6 publication_status: published publisher: ACM publist_id: '5676' pubrep_id: '625' quality_controlled: '1' related_material: record: - id: '1155' relation: dissertation_contains status: public scopus_import: 1 status: public title: Complete composition operators for IOCO-testing theory type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1689' abstract: - lang: eng text: We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study. author: - first_name: Mária full_name: Svoreňová, Mária last_name: Svoreňová - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ivana full_name: Cěrná, Ivana last_name: Cěrná - first_name: Cǎlin full_name: Belta, Cǎlin last_name: Belta citation: ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608' apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728608' chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.' ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.' ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.' mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.' short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.' conference: end_date: 2015-04-16 location: Seattle, WA, United States name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2015-04-14 date_created: 2018-12-11T11:53:29Z date_published: 2015-04-14T00:00:00Z date_updated: 2023-09-20T09:43:09Z day: '14' department: - _id: ToHe - _id: KrCh doi: 10.1145/2728606.2728608 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1410.5387 month: '04' oa: 1 oa_version: Preprint page: 259 - 268 project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: 'Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control' publication_status: published publisher: ACM publist_id: '5456' related_material: record: - id: '1407' relation: later_version status: public scopus_import: 1 status: public title: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '1603' abstract: - lang: eng text: "For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour." acknowledgement: This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734. alternative_title: - LNCS author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Andreas full_name: Fellner, Andreas id: 42BABFB4-F248-11E8-B48F-1D18A9856A87 last_name: Fellner - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10. ieee: 'T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.' ista: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.' mla: Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10. short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177. conference: end_date: 2015-07-24 location: San Francisco, CA, United States name: 'CAV: Computer Aided Verification' start_date: 2015-07-18 date_created: 2018-12-11T11:52:58Z date_published: 2015-07-16T00:00:00Z date_updated: 2024-02-21T13:52:07Z day: '16' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-21690-4_10 ec_funded: 1 intvolume: ' 9206' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1502.02834 month: '07' oa: 1 oa_version: Preprint page: 158 - 177 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme publication_identifier: eisbn: - 978-3-319-21690-4 publication_status: published publisher: Springer publist_id: '5564' quality_controlled: '1' related_material: record: - id: '5549' relation: research_paper status: public scopus_import: 1 status: public title: Counterexample explanation by learning small strategies in Markov decision processes type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 9206 year: '2015' ... --- _id: '2027' abstract: - lang: eng text: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples. acknowledgement: This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1. alternative_title: - LNCS author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Marta full_name: Kwiatkowska, Marta last_name: Kwiatkowska - first_name: David full_name: Parker, David last_name: Parker - first_name: Mateusz full_name: Ujma, Mateusz last_name: Ujma citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8. ieee: T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114. ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.' mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8. short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ALENEX: Algorithm Engineering and Experiments' start_date: 2014-11-03 date_created: 2018-12-11T11:55:17Z date_published: 2014-11-01T00:00:00Z date_updated: 2021-01-12T06:54:49Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-11936-6_8 ec_funded: 1 editor: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin intvolume: ' 8837' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.2967 month: '11' oa: 1 oa_version: Submitted Version page: 98 - 114 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 26241A12-B435-11E9-9278-68D0E5697425 grant_number: '24696' name: LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ' Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)' publication_status: published publisher: Society of Industrial and Applied Mathematics publist_id: '5046' quality_controlled: '1' status: public title: Verification of markov decision processes using learning algorithms type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2026' abstract: - lang: eng text: 'We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.' acknowledgement: "Sponsor: P202/12/G061; GACR; Czech Science Foundation\r\n\r\n" alternative_title: - LNCS author: - first_name: Zuzana full_name: Komárková, Zuzana last_name: Komárková - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Komárková Z, Kretinsky J. Rabinizer 3: Safraless translation of ltl to small deterministic automata. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Springer; 2014:235-241. doi:10.1007/978-3-319-11936-6_17' apa: 'Komárková, Z., & Kretinsky, J. (2014). Rabinizer 3: Safraless translation of ltl to small deterministic automata. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 235–241). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_17' chicago: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:235–41. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_17.' ieee: 'Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl to small deterministic automata,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 235–241.' ista: 'Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl to small deterministic automata. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.' mla: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 235–41, doi:10.1007/978-3-319-11936-6_17.' short: Z. Komárková, J. Kretinsky, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, 2014, pp. 235–241. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2014-11-03 date_created: 2018-12-11T11:55:17Z date_published: 2014-01-01T00:00:00Z date_updated: 2021-01-12T06:54:49Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-319-11936-6_17 ec_funded: 1 editor: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin intvolume: ' 8837' language: - iso: eng month: '01' oa_version: None page: 235 - 241 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_status: published publisher: Springer publist_id: '5045' quality_controlled: '1' status: public title: 'Rabinizer 3: Safraless translation of ltl to small deterministic automata' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2053' abstract: - lang: eng text: In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems. acknowledgement: This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams. alternative_title: - LNCS author: - first_name: Holger full_name: Hermanns, Holger last_name: Hermanns - first_name: Jan full_name: Krčál, Jan last_name: Krčál - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:10.1007/978-3-662-44584-6_18' apa: 'Hermanns, H., Krčál, J., & Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_18' chicago: 'Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_18.' ieee: 'H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.' ista: 'Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.' mla: 'Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.' short: H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265. conference: end_date: 2014-09-05 location: Rome, Italy name: 'CONCUR: Concurrency Theory' start_date: 2014-09-02 date_created: 2018-12-11T11:55:27Z date_published: 2014-09-01T00:00:00Z date_updated: 2021-01-12T06:55:00Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-662-44584-6_18 ec_funded: 1 editor: - first_name: Paolo full_name: Baldan, Paolo last_name: Baldan - first_name: Daniele full_name: Gorla, Daniele last_name: Gorla intvolume: ' 8704' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1404.5084 month: '09' oa: 1 oa_version: Submitted Version page: 249 - 265 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '4993' status: public title: 'Probabilistic bisimulation: Naturally on distributions' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8704 year: '2014' ... --- _id: '2190' abstract: - lang: eng text: We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods. acknowledgement: The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061. alternative_title: - LNCS author: - first_name: Javier full_name: Esparza, Javier last_name: Esparza - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13' apa: 'Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13' chicago: 'Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.' ieee: 'J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.' ista: 'Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.' mla: 'Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.' short: J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T11:56:14Z date_published: 2014-01-01T00:00:00Z date_updated: 2021-01-12T06:55:53Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-319-08867-9_13 ec_funded: 1 intvolume: ' 8559' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.3388 month: '01' oa: 1 oa_version: Submitted Version page: 192 - 208 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication_status: published publisher: Springer publist_id: '4784' quality_controlled: '1' status: public title: 'From LTL to deterministic automata: A safraless compositional approach' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ... --- _id: '2446' abstract: - lang: eng text: The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Gaiser, Andreas last_name: Gaiser - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37 apa: 'Chatterjee, K., Gaiser, A., & Kretinsky, J. (2013). Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_37' chicago: Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_37. ieee: K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013. ista: Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575. mla: Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37. short: K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575. conference: end_date: 2013-07-19 location: St. Petersburg, Russia name: 'CAV: Computer Aided Verification' start_date: 2013-07-13 date_created: 2018-12-11T11:57:42Z date_published: 2013-07-01T00:00:00Z date_updated: 2020-08-11T10:09:47Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-39799-8_37 ec_funded: 1 external_id: arxiv: - '1304.5281' intvolume: ' 8044' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1304.5281 month: '07' oa: 1 oa_version: Preprint page: 559 - 575 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '4457' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8044 year: '2013' ...