[{"month":"05","file":[{"checksum":"40405907aa012acece1bc26cf0be554d","access_level":"open_access","date_updated":"2020-07-14T12:46:55Z","file_size":589619,"creator":"system","file_name":"IST-2015-335-v1+1_report.pdf","date_created":"2018-12-12T11:53:55Z","relation":"main_file","file_id":"5517","content_type":"application/pdf"}],"date_created":"2018-12-12T11:39:20Z","_id":"5439","abstract":[{"text":"The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. ","lang":"eng"}],"date_published":"2015-05-18T00:00:00Z","page":"20","file_date_updated":"2020-07-14T12:46:55Z","department":[{"_id":"ToHe"}],"status":"public","pubrep_id":"335","publisher":"IST Austria","publication_status":"published","oa":1,"day":"18","type":"technical_report","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi","last_name":"Boker"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"year":"2015","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","has_accepted_license":"1","citation":{"ieee":"U. Boker, T. A. Henzinger, and J. Otop, <i>The target discounted-sum problem</i>. IST Austria, 2015.","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>.","mla":"Boker, Udi, et al. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>.","short":"U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015.","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). <i>The target discounted-sum problem</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>","ama":"Boker U, Henzinger TA, Otop J. <i>The Target Discounted-Sum Problem</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>"},"title":"The target discounted-sum problem","date_updated":"2023-02-23T10:08:48Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"ddc":["004","512","513"],"doi":"10.15479/AT:IST-2015-335-v1-1","related_material":{"record":[{"relation":"later_version","id":"1659","status":"public"}]}},{"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"id":"1603","relation":"popular_science","status":"public"}]},"datarep_id":"28","doi":"10.15479/AT:ISTA:28","ddc":["004"],"keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","ec_funded":1,"citation":{"ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","short":"A. Fellner, (2015).","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>"},"type":"research_data","author":[{"id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","full_name":"Fellner, Andreas","first_name":"Andreas","last_name":"Fellner"}],"day":"13","publisher":"Institute of Science and Technology Austria","status":"public","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-12T12:31:29Z","month":"08","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2024-02-21T13:52:07Z","year":"2015","oa_version":"Published Version","has_accepted_license":"1","contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"publist_id":"5564","oa":1,"license":"https://creativecommons.org/publicdomain/zero/1.0/","tmp":{"name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","short":"CC0 (1.0)"},"file_date_updated":"2020-07-14T12:47:00Z","article_processing_charge":"No","_id":"5549","date_published":"2015-08-13T00:00:00Z","abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"file":[{"date_created":"2018-12-12T13:02:31Z","relation":"main_file","file_id":"5597","content_type":"application/zip","checksum":"b8bcb43c0893023cda66c1b69c16ac62","access_level":"open_access","date_updated":"2020-07-14T12:47:00Z","file_size":49557109,"creator":"system","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip"}]},{"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"ddc":["005"],"doi":"10.4230/LIPIcs.SNAPL.2015.90","language":[{"iso":"eng"}],"title":"The need for language support for fault-tolerant distributed systems","conference":{"start_date":"2015-05-03","end_date":"2015-05-06","name":"SNAPL: Summit oN Advances in Programming Languages","location":"Asilomar, CA, United States"},"citation":{"ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102.","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.","mla":"Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>"},"ec_funded":1,"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Zufferey","first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","alternative_title":["LIPIcs"],"day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","status":"public","intvolume":"        32","quality_controlled":"1","department":[{"_id":"ToHe"}],"page":"90 - 102","date_created":"2018-12-11T11:52:22Z","series_title":"Leibniz International Proceedings in Informatics","month":"01","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"scopus_import":1,"date_updated":"2020-08-11T10:09:14Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","year":"2015","has_accepted_license":"1","publist_id":"5681","oa":1,"publication_status":"published","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"499","volume":32,"file_date_updated":"2020-07-14T12:44:58Z","abstract":[{"text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.","lang":"eng"}],"_id":"1498","date_published":"2015-01-01T00:00:00Z","file":[{"date_updated":"2020-07-14T12:44:58Z","access_level":"open_access","checksum":"cf5e94baa89a2dc4c5de01abc676eda8","file_name":"IST-2016-499-v1+1_9.pdf","creator":"system","file_size":489362,"date_created":"2018-12-12T10:14:02Z","content_type":"application/pdf","file_id":"5050","relation":"main_file"}]},{"publist_id":"5680","year":"2015","oa_version":"Published Version","has_accepted_license":"1","scopus_import":1,"date_updated":"2021-01-12T06:51:10Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"IST-2016-498-v1+1_32.pdf","file_size":623563,"creator":"system","date_updated":"2020-07-14T12:44:58Z","access_level":"open_access","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","content_type":"application/pdf","file_id":"4672","relation":"main_file","date_created":"2018-12-12T10:08:12Z"}],"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."}],"_id":"1499","date_published":"2015-01-01T00:00:00Z","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:44:58Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"498","volume":42,"citation":{"chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>.","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","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.","mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>","apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>"},"ec_funded":1,"title":"Polynomial time decidability of weighted synchronization under partial observability","conference":{"location":"Madrid, Spain","name":"CONCUR: Concurrency Theory","start_date":"2015-09-01","end_date":"2015-09-04"},"day":"01","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"last_name":"Larsen","first_name":"Kim","full_name":"Larsen, Kim"},{"last_name":"Laursen","first_name":"Simon","full_name":"Laursen, Simon"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"type":"conference","alternative_title":["LIPIcs"],"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"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.","language":[{"iso":"eng"}],"ddc":["000","003"],"doi":"10.4230/LIPIcs.CONCUR.2015.142","page":"142 - 154","month":"01","date_created":"2018-12-11T11:52:22Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","status":"public","intvolume":"        42"},{"day":"01","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca"}],"type":"journal_article","ec_funded":1,"citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>.","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>."},"title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","language":[{"iso":"eng"}],"doi":"10.1007/s10703-015-0235-2","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"1155","status":"public"}]},"month":"10","date_created":"2018-12-11T11:52:23Z","page":"230 - 264","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Formal Methods in System Design","intvolume":"        47","status":"public","publisher":"Springer","publist_id":"5677","oa_version":"Preprint","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:58:33Z","scopus_import":1,"_id":"1501","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. "}],"date_published":"2015-10-01T00:00:00Z","issue":"2","volume":47,"publication_status":"published","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1405.0835","open_access":"1"}]},{"_id":"1502","date_published":"2015-05-01T00:00:00Z","abstract":[{"text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.","lang":"eng"}],"file":[{"file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","file_size":467561,"creator":"system","date_updated":"2020-07-14T12:44:59Z","access_level":"open_access","checksum":"c6ce681035c163a158751f240cb7d389","content_type":"application/pdf","file_id":"5303","relation":"main_file","date_created":"2018-12-12T10:17:46Z"}],"oa":1,"publication_status":"published","pubrep_id":"625","file_date_updated":"2020-07-14T12:44:59Z","year":"2015","has_accepted_license":"1","oa_version":"Submitted Version","publist_id":"5676","publication_identifier":{"isbn":["978-1-4503-3471-6"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:58:33Z","page":"101 - 110","date_created":"2018-12-11T11:52:24Z","month":"05","publisher":"ACM","status":"public","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","title":"Complete composition operators for IOCO-testing theory","conference":{"location":"Montreal, QC, Canada","start_date":"2015-05-04","end_date":"2015-05-08","name":"CBSE: Component-Based Software Engineering "},"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:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>.","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>.","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."},"ec_funded":1,"author":[{"first_name":"Nikola","full_name":"Beneš, Nikola","last_name":"Beneš"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"type":"conference","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"day":"01","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"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.","doi":"10.1145/2737166.2737175","ddc":["000"],"language":[{"iso":"eng"}]},{"abstract":[{"lang":"eng","text":"Systems biology rests on the idea that biological complexity can be better unraveled through the interplay of modeling and experimentation. However, the success of this approach depends critically on the informativeness of the chosen experiments, which is usually unknown a priori. Here, we propose a systematic scheme based on iterations of optimal experiment design, flow cytometry experiments, and Bayesian parameter inference to guide the discovery process in the case of stochastic biochemical reaction networks. To illustrate the benefit of our methodology, we apply it to the characterization of an engineered light-inducible gene expression circuit in yeast and compare the performance of the resulting model with models identified from nonoptimal experiments. In particular, we compare the parameter posterior distributions and the precision to which the outcome of future experiments can be predicted. Moreover, we illustrate how the identified stochastic model can be used to determine light induction patterns that make either the average amount of protein or the variability in a population of cells follow a desired profile. Our results show that optimal experiment design allows one to derive models that are accurate enough to precisely predict and regulate the protein expression in heterogeneous cell populations over extended periods of time."}],"_id":"1538","date_published":"2015-06-30T00:00:00Z","issue":"26","volume":112,"publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4491780/"}],"publist_id":"5633","oa_version":"Submitted Version","year":"2015","date_updated":"2021-01-12T06:51:27Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"pmid":["26085136"]},"scopus_import":1,"month":"06","date_created":"2018-12-11T11:52:36Z","page":"8148 - 8153","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"quality_controlled":"1","publication":"PNAS","intvolume":"       112","status":"public","publisher":"National Academy of Sciences","day":"30","type":"journal_article","author":[{"full_name":"Ruess, Jakob","first_name":"Jakob","last_name":"Ruess","orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Francesca","full_name":"Parise, Francesca","last_name":"Parise"},{"first_name":"Andreas","full_name":"Milias Argeitis, Andreas","last_name":"Milias Argeitis"},{"last_name":"Khammash","full_name":"Khammash, Mustafa","first_name":"Mustafa"},{"last_name":"Lygeros","first_name":"John","full_name":"Lygeros, John"}],"ec_funded":1,"citation":{"ama":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. 2015;112(26):8148-8153. doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>","apa":"Ruess, J., Parise, F., Milias Argeitis, A., Khammash, M., &#38; Lygeros, J. (2015). Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>","short":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, J. Lygeros, PNAS 112 (2015) 8148–8153.","mla":"Ruess, Jakob, et al. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>, vol. 112, no. 26, National Academy of Sciences, 2015, pp. 8148–53, doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>.","chicago":"Ruess, Jakob, Francesca Parise, Andreas Milias Argeitis, Mustafa Khammash, and John Lygeros. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>.","ieee":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, and J. Lygeros, “Iterative experiment design guides the characterization of a light-inducible gene expression circuit,” <i>PNAS</i>, vol. 112, no. 26. National Academy of Sciences, pp. 8148–8153, 2015.","ista":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. 2015. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. PNAS. 112(26), 8148–8153."},"title":"Iterative experiment design guides the characterization of a light-inducible gene expression circuit","language":[{"iso":"eng"}],"doi":"10.1073/pnas.1423947112","acknowledgement":"J.R., F.P., and J.L. acknowledge support from the European Commission under the Network of Excellence HYCON2 (highly-complex and networked control systems) and SystemsX.ch under the SignalX Project. J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme FP7/2007-2013 under REA (Research Executive Agency) Grant 291734. M.K. acknowledges support from Human Frontier Science Program Grant RP0061/2011 (www.hfsp.org). ","pmid":1,"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}]},{"oa_version":"Published Version","has_accepted_license":"1","year":"2015","publist_id":"5632","scopus_import":1,"date_updated":"2021-01-12T06:51:28Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"24","abstract":[{"text":"Many stochastic models of biochemical reaction networks contain some chemical species for which the number of molecules that are present in the system can only be finite (for instance due to conservation laws), but also other species that can be present in arbitrarily large amounts. The prime example of such networks are models of gene expression, which typically contain a small and finite number of possible states for the promoter but an infinite number of possible states for the amount of mRNA and protein. One of the main approaches to analyze such models is through the use of equations for the time evolution of moments of the chemical species. Recently, a new approach based on conditional moments of the species with infinite state space given all the different possible states of the finite species has been proposed. It was argued that this approach allows one to capture more details about the full underlying probability distribution with a smaller number of equations. Here, I show that the result that less moments provide more information can only stem from an unnecessarily complicated description of the system in the classical formulation. The foundation of this argument will be the derivation of moment equations that describe the complete probability distribution over the finite state space but only low-order moments over the infinite state space. I will show that the number of equations that is needed is always less than what was previously claimed and always less than the number of conditional moment equations up to the same order. To support these arguments, a symbolic algorithm is provided that can be used to derive minimal systems of unconditional moment equations for models with partially finite state space. ","lang":"eng"}],"_id":"1539","date_published":"2015-12-22T00:00:00Z","article_number":"244103","file":[{"creator":"system","file_size":605355,"file_name":"IST-2016-593-v1+1_Minimal_moment_equations.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:01Z","checksum":"838657118ae286463a2b7737319f35ce","relation":"main_file","file_id":"4641","content_type":"application/pdf","date_created":"2018-12-12T10:07:43Z"}],"oa":1,"publication_status":"published","pubrep_id":"593","volume":143,"file_date_updated":"2020-07-14T12:45:01Z","title":"Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space","citation":{"mla":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>, vol. 143, no. 24, 244103, American Institute of Physics, 2015, doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>.","ista":"Ruess J. 2015. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. Journal of Chemical Physics. 143(24), 244103.","ieee":"J. Ruess, “Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space,” <i>Journal of Chemical Physics</i>, vol. 143, no. 24. American Institute of Physics, 2015.","chicago":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>. American Institute of Physics, 2015. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>.","apa":"Ruess, J. (2015). Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. American Institute of Physics. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>","ama":"Ruess J. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. 2015;143(24). doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>","short":"J. Ruess, Journal of Chemical Physics 143 (2015)."},"ec_funded":1,"type":"journal_article","author":[{"full_name":"Ruess, Jakob","first_name":"Jakob","last_name":"Ruess","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282"}],"day":"22","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"doi":"10.1063/1.4937937","ddc":["000"],"language":[{"iso":"eng"}],"date_created":"2018-12-11T11:52:36Z","month":"12","publisher":"American Institute of Physics","status":"public","intvolume":"       143","publication":"Journal of Chemical Physics","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"quality_controlled":"1"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2020-08-11T10:09:17Z","scopus_import":1,"publist_id":"5630","year":"2015","oa_version":"None","publication_status":"published","volume":9434,"_id":"1541","date_published":"2015-11-28T00:00:00Z","abstract":[{"text":"We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision.","lang":"eng"}],"acknowledgement":"This work was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-26287-1_1","ec_funded":1,"citation":{"ista":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating reachability analysis on multi-core processors. 9434, 3–18.","ieee":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed: Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer, pp. 3–18, 2015.","chicago":"Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>.","mla":"Ray, Rajarshi, et al. <i>XSpeed: Accelerating Reachability Analysis on Multi-Core Processors</i>. Vol. 9434, Springer, 2015, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>.","short":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015) 3–18.","apa":"Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., &#38; Grosu, R. (2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>","ama":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating reachability analysis on multi-core processors. 2015;9434:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>"},"conference":{"location":"Haifa, Israel","name":"HVC: Haifa Verification Conference","start_date":"2015-11-17","end_date":"2015-11-19"},"title":"XSpeed: Accelerating reachability analysis on multi-core processors","day":"28","alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Ray","full_name":"Ray, Rajarshi","first_name":"Rajarshi"},{"last_name":"Gurung","full_name":"Gurung, Amit","first_name":"Amit"},{"full_name":"Das, Binayak","first_name":"Binayak","last_name":"Das"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"}],"publisher":"Springer","department":[{"_id":"ToHe"}],"quality_controlled":"1","intvolume":"      9434","status":"public","page":"3 - 18","month":"11","date_created":"2018-12-11T11:52:37Z","series_title":"Lecture Notes in Computer Science"},{"intvolume":"      9450","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Springer","date_created":"2018-12-11T11:52:55Z","month":"11","page":"162 - 177","doi":"10.1007/978-3-662-48899-7_12","language":[{"iso":"eng"}],"project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"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","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","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"}],"type":"conference","alternative_title":["LNCS"],"day":"22","title":"Controller synthesis for MDPs and frequency LTL\\GU","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","start_date":"2015-11-24","end_date":"2015-11-28","location":"Suva, Fiji"},"citation":{"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.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>.","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>.","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>"},"ec_funded":1,"volume":9450,"publication_status":"published","abstract":[{"lang":"eng","text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata."}],"_id":"1594","date_published":"2015-11-22T00:00:00Z","scopus_import":1,"date_updated":"2021-01-12T06:51:50Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015","oa_version":"None","publist_id":"5577"},{"scopus_import":1,"date_updated":"2021-01-12T06:51:54Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5566","oa_version":"Submitted Version","has_accepted_license":"1","year":"2015","file_date_updated":"2020-07-14T12:45:04Z","volume":9206,"publication_status":"published","oa":1,"file":[{"relation":"main_file","file_id":"7850","content_type":"application/pdf","date_created":"2020-05-15T08:38:12Z","file_size":1651779,"creator":"dernst","file_name":"2015_CAV_Babiak.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:04Z","checksum":"5885236fa88a439baba9ac6f3e801e93"}],"abstract":[{"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.","lang":"eng"}],"_id":"1601","date_published":"2015-07-16T00:00:00Z","article_processing_charge":"No","language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.1007/978-3-319-21690-4_31","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"day":"16","author":[{"full_name":"Babiak, Tomáš","first_name":"Tomáš","last_name":"Babiak"},{"last_name":"Blahoudek","full_name":"Blahoudek, František","first_name":"František"},{"last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre","first_name":"Alexandre"},{"first_name":"Joachim","full_name":"Klein, Joachim","last_name":"Klein"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"last_name":"Mueller","full_name":"Mueller, Daniel","first_name":"Daniel"},{"last_name":"Parker","full_name":"Parker, David","first_name":"David"},{"first_name":"Jan","full_name":"Strejček, Jan","last_name":"Strejček"}],"type":"conference","alternative_title":["LNCS"],"citation":{"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. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","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.","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","ieee":"T. Babiak <i>et al.</i>, “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.","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. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>."},"ec_funded":1,"title":"The Hanoi omega-automata format","conference":{"end_date":"2015-07-24","start_date":"2015-07-18","name":"CAV: Computer Aided Verification","location":"San Francisco, CA, United States"},"quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"intvolume":"      9206","status":"public","publisher":"Springer","month":"07","date_created":"2018-12-11T11:52:57Z","page":"479 - 486"},{"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"related_material":{"record":[{"relation":"research_paper","id":"5549","status":"public"}]},"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.","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-21690-4_10","citation":{"mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>.","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.","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.","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. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>","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:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177."},"ec_funded":1,"title":"Counterexample explanation by learning small strategies in Markov decision processes","conference":{"location":"San Francisco, CA, United States","name":"CAV: Computer Aided Verification","start_date":"2015-07-18","end_date":"2015-07-24"},"day":"16","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"last_name":"Fellner","first_name":"Andreas","full_name":"Fellner, Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"}],"type":"conference","alternative_title":["LNCS"],"publisher":"Springer","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":"      9206","status":"public","page":"158 - 177","month":"07","date_created":"2018-12-11T11:52:58Z","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2024-02-21T13:52:07Z","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"publist_id":"5564","oa_version":"Preprint","year":"2015","publication_status":"published","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"oa":1,"volume":9206,"_id":"1603","date_published":"2015-07-16T00:00:00Z","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."}]},{"quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"      9434","publisher":"Springer","month":"11","date_created":"2018-12-11T11:52:59Z","page":"19 - 35","language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.1007/978-3-319-26287-1_2","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","day":"28","author":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"last_name":"Batt","full_name":"Batt, Grégory","first_name":"Grégory"},{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"type":"conference","alternative_title":["LNCS"],"citation":{"short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., &#38; Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>","ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35.","chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>.","mla":"Bogomolov, Sergiy, et al. <i>Abstraction-Based Parameter Synthesis for Multiaffine Systems</i>. Vol. 9434, Springer, 2015, pp. 19–35, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>."},"ec_funded":1,"title":"Abstraction-based parameter synthesis for multiaffine systems","conference":{"name":"HVC: Haifa Verification Conference","end_date":"2015-11-19","start_date":"2015-11-17","location":"Haifa, Israel"},"file_date_updated":"2020-07-14T12:45:05Z","volume":9434,"publication_status":"published","oa":1,"file":[{"content_type":"application/pdf","relation":"main_file","file_id":"7851","date_created":"2020-05-15T08:43:19Z","file_name":"2015_LNCS_Bogomolov.pdf","file_size":1053207,"creator":"dernst","checksum":"3aab260f3f34641d622030ba22645b3e","date_updated":"2020-07-14T12:45:05Z","access_level":"open_access"}],"_id":"1605","date_published":"2015-11-28T00:00:00Z","abstract":[{"text":"Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.","lang":"eng"}],"article_processing_charge":"No","scopus_import":1,"date_updated":"2021-01-12T06:51:56Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5561","has_accepted_license":"1","oa_version":"Submitted Version","year":"2015"},{"oa_version":"None","year":"2015","publist_id":"5562","publication_identifier":{"isbn":["978-3-319-23819-7"]},"date_updated":"2022-02-01T14:52:59Z","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","scopus_import":"1","abstract":[{"lang":"eng","text":"In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST."}],"_id":"1606","date_published":"2015-11-15T00:00:00Z","article_processing_charge":"No","volume":9333,"publication_status":"published","alternative_title":["LNCS"],"author":[{"last_name":"Nguyen","first_name":"Luan","full_name":"Nguyen, Luan"},{"last_name":"Schilling","first_name":"Christian","full_name":"Schilling, Christian"},{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"}],"type":"conference","day":"15","conference":{"name":"RV: Runtime Verification","start_date":"2015-09-22","end_date":"2015-09-25","location":"Vienna, Austria"},"title":"Runtime verification for hybrid analysis tools","ec_funded":1,"citation":{"short":"L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International Conference, Springer Nature, 2015, pp. 281–286.","ama":"Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid analysis tools. In: <i>6th International Conference</i>. Vol 9333. Springer Nature; 2015:281-286. doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>","apa":"Nguyen, L., Schilling, C., Bogomolov, S., &#38; Johnson, T. (2015). Runtime verification for hybrid analysis tools. In <i>6th International Conference</i> (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>","chicago":"Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson. “Runtime Verification for Hybrid Analysis Tools.” In <i>6th International Conference</i>, 9333:281–86. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>.","ista":"Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification for hybrid analysis tools. 6th International Conference. RV: Runtime Verification, LNCS, vol. 9333, 281–286.","ieee":"L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification for hybrid analysis tools,” in <i>6th International Conference</i>, Vienna, Austria, 2015, vol. 9333, pp. 281–286.","mla":"Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” <i>6th International Conference</i>, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>."},"doi":"10.1007/978-3-319-23820-3_19","language":[{"iso":"eng"}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:52:59Z","month":"11","page":"281 - 286","intvolume":"      9333","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"6th International Conference","publisher":"Springer Nature"},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_updated":"2023-02-23T12:26:24Z","external_id":{"arxiv":["1504.08259"]},"scopus_import":"1","publication_identifier":{"isbn":["978-3-662-47665-9"]},"publist_id":"5556","oa_version":"None","year":"2015","volume":9135,"pubrep_id":"321","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"_id":"1610","date_published":"2015-07-01T00:00:00Z","abstract":[{"lang":"eng","text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k."}],"arxiv":1,"issue":"Part II","article_processing_charge":"No","language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-47666-6_10","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_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","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"relation":"later_version","id":"465","status":"public"},{"id":"5438","relation":"earlier_version","status":"public"}]},"day":"01","alternative_title":["LNCS"],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","ec_funded":1,"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>"},"conference":{"location":"Kyoto, Japan","name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","end_date":"2015-07-10"},"title":"Edit distance for pushdown automata","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","publication":"42nd International Colloquium","status":"public","intvolume":"      9135","publisher":"Springer Nature","month":"07","date_created":"2018-12-11T11:53:01Z","page":"121 - 133"},{"doi":"10.4204/EPTCS.169.5","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:52:38Z","language":[{"iso":"eng"}],"conference":{"start_date":"2014-07-17","end_date":"2014-07-17","name":"HCVS: Horn Clauses for Verification and Synthesis","location":"Vienna, Austria"},"title":"Generalised interpolation by solving recursion free-horn clauses","citation":{"short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing, 2014, pp. 31–38.","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>. Vol 169. Open Publishing; 2014:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>","apa":"Gupta, A., Popeea, C., &#38; Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i> (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, 169:31–38. Open Publishing, 2014. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, Vienna, Austria, 2014, vol. 169, pp. 31–38.","ista":"Gupta A, Popeea C, Rybalchenko A. 2014. Generalised interpolation by solving recursion free-horn clauses. Electronic Proceedings in Theoretical Computer Science, EPTCS. HCVS: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, 31–38.","mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, vol. 169, Open Publishing, 2014, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>."},"oa_version":"Submitted Version","year":"2014","alternative_title":["EPTCS"],"author":[{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Corneliu","full_name":"Popeea, Corneliu","last_name":"Popeea"},{"last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey","first_name":"Andrey"}],"type":"conference","day":"02","publist_id":"5435","main_file_link":[{"url":"http://arxiv.org/abs/1303.7378v2","open_access":"1"}],"oa":1,"publication_status":"published","publisher":"Open Publishing","volume":169,"status":"public","intvolume":"       169","department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","page":"31 - 38","abstract":[{"lang":"eng","text":"In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools."}],"_id":"1702","date_created":"2018-12-11T11:53:33Z","date_published":"2014-12-02T00:00:00Z","month":"12"},{"publisher":"Elsevier","status":"public","intvolume":"       560","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication":"Theoretical Computer Science","page":"348 - 363","date_created":"2018-12-11T11:53:43Z","month":"12","related_material":{"record":[{"status":"public","id":"2916","relation":"earlier_version"}]},"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1016/j.tcs.2014.08.019","language":[{"iso":"eng"}],"title":"Interface simulation distances","ec_funded":1,"citation":{"ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” <i>Theoretical Computer Science</i>, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Interface simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. <i>Theoretical Computer Science</i>. 2014;560(3):348-363. doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>"},"type":"journal_article","author":[{"last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun"}],"day":"04","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1210.2450"}],"oa":1,"publication_status":"published","volume":560,"issue":"3","_id":"1733","abstract":[{"lang":"eng","text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies."}],"date_published":"2014-12-04T00:00:00Z","date_updated":"2023-02-23T11:04:00Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"oa_version":"Submitted Version","year":"2014","publist_id":"5392"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"acknowledgement":"The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement QUAINT (I774-N23)","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-13338-6_6","citation":{"apa":"Hofferek, G., &#38; Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), <i>HVC 2014</i> (Vol. 8855, pp. 68–74). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>","ama":"Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. <i>HVC 2014</i>. Vol 8855. Springer; 2014:68-74. doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>","short":"G. Hofferek, A. Gupta, in:, E. Yahav (Ed.), HVC 2014, Springer, 2014, pp. 68–74.","mla":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” <i>HVC 2014</i>, edited by Eran Yahav, vol. 8855, Springer, 2014, pp. 68–74, doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>.","ista":"Hofferek G, Gupta A. 2014. Suraq - a controller synthesis tool using uninterpreted functions. HVC 2014. HVC: Haifa Verification Conference, LNCS, vol. 8855, 68–74.","ieee":"G. Hofferek and A. Gupta, “Suraq - a controller synthesis tool using uninterpreted functions,” in <i>HVC 2014</i>, Haifa, Israel, 2014, vol. 8855, pp. 68–74.","chicago":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” In <i>HVC 2014</i>, edited by Eran Yahav, 8855:68–74. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>."},"ec_funded":1,"title":"Suraq - a controller synthesis tool using uninterpreted functions","conference":{"location":"Haifa, Israel","end_date":"2014-11-20","start_date":"2014-11-18","name":"HVC: Haifa Verification Conference"},"day":"01","type":"conference","author":[{"first_name":"Georg","full_name":"Hofferek, Georg","last_name":"Hofferek"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"}],"alternative_title":["LNCS"],"publisher":"Springer","publication":"HVC 2014","department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","intvolume":"      8855","page":"68 - 74","month":"01","date_created":"2018-12-11T11:54:27Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:44Z","editor":[{"full_name":"Yahav, Eran","first_name":"Eran","last_name":"Yahav"}],"publist_id":"5228","year":"2014","oa_version":"None","publication_status":"published","volume":8855,"_id":"1869","abstract":[{"lang":"eng","text":"Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes."}],"date_published":"2014-01-01T00:00:00Z"},{"page":"431 - 443","month":"12","date_created":"2018-12-11T11:54:27Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"Leibniz International Proceedings in Informatics, LIPIcs","status":"public","intvolume":"        29","citation":{"chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>.","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, Delhi, India, 2014, vol. 29, pp. 431–443.","ista":"Henzinger TA, Otop J, Samanta R. 2014. Lipschitz robustness of finite-state transducers. Leibniz International Proceedings in Informatics, LIPIcs. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 29, 431–443.","mla":"Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” <i>Leibniz International Proceedings in Informatics, LIPIcs</i>, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>.","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–443.","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: <i>Leibniz International Proceedings in Informatics, LIPIcs</i>. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">10.4230/LIPIcs.FSTTCS.2014.431</a>","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In <i>Leibniz International Proceedings in Informatics, LIPIcs</i> (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431\">https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431</a>"},"conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2014-12-17","start_date":"2014-12-15","location":"Delhi, India"},"title":"Lipschitz robustness of finite-state transducers","day":"01","alternative_title":["LIPIcs"],"author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.FSTTCS.2014.431","ddc":["004"],"file":[{"file_name":"IST-2017-804-v1+1_37.pdf","file_size":562151,"creator":"system","checksum":"7b1aff1710a8bffb7080ec07f62d9a17","date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","content_type":"application/pdf","file_id":"4734","relation":"main_file","date_created":"2018-12-12T10:09:11Z"}],"abstract":[{"lang":"eng","text":"We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers."}],"_id":"1870","date_published":"2014-12-01T00:00:00Z","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:45:19Z","volume":29,"pubrep_id":"804","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publist_id":"5227","year":"2014","oa_version":"Published Version","has_accepted_license":"1","date_updated":"2021-01-12T06:53:45Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},{"publisher":"Springer","status":"public","intvolume":"      8837","publication":"ATVA 2014","quality_controlled":"1","department":[{"_id":"ToHe"}],"page":"185 - 200","date_created":"2018-12-11T11:54:28Z","month":"01","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","doi":"10.1007/978-3-319-11936-6_14","ddc":["000"],"language":[{"iso":"eng"}],"title":"Extensional crisis and proving identity","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2014-11-03","end_date":"2014-11-07","location":"Sydney, Australia"},"citation":{"mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” <i>ATVA 2014</i>, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 185–200, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>.","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In <i>ATVA 2014</i>, edited by Franck Cassez and Jean-François Raskin, 8837:185–200. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>.","ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. ATVA 2014. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in <i>ATVA 2014</i>, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: Cassez F, Raskin J-F, eds. <i>ATVA 2014</i>. Vol 8837. Springer; 2014:185-200. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>","apa":"Gupta, A., Kovács, L., Kragl, B., &#38; Voronkov, A. (2014). Extensional crisis and proving identity. In F. Cassez &#38; J.-F. Raskin (Eds.), <i>ATVA 2014</i> (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, F. Cassez, J.-F. Raskin (Eds.), ATVA 2014, Springer, 2014, pp. 185–200."},"ec_funded":1,"type":"conference","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"first_name":"Laura","full_name":"Kovács, Laura","last_name":"Kovács"},{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl"},{"first_name":"Andrei","full_name":"Voronkov, Andrei","last_name":"Voronkov"}],"alternative_title":["LNCS"],"day":"01","oa":1,"publication_status":"published","pubrep_id":"641","volume":8837,"file_date_updated":"2020-07-14T12:45:19Z","abstract":[{"text":"Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.","lang":"eng"}],"_id":"1872","date_published":"2014-01-01T00:00:00Z","file":[{"date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","file_name":"IST-2016-641-v1+1_atva2014.pdf","creator":"system","file_size":244294,"date_created":"2018-12-12T10:10:15Z","content_type":"application/pdf","file_id":"4801","relation":"main_file"}],"scopus_import":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:45Z","editor":[{"first_name":"Franck","full_name":"Cassez, Franck","last_name":"Cassez"},{"full_name":"Raskin, Jean-François","first_name":"Jean-François","last_name":"Raskin"}],"year":"2014","has_accepted_license":"1","oa_version":"Submitted Version","publist_id":"5226"}]