[{"month":"02","_id":"608","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","title":"Synthesis from component libraries with costs","oa":1,"article_type":"original","department":[{"_id":"ToHe"}],"ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"Synthesis is the automated construction of a system from its specification. In real life, hardware and software systems are rarely constructed from scratch. Rather, a system is typically constructed from a library of components. Lustig and Vardi formalized this intuition and studied LTL synthesis from component libraries. In real life, designers seek optimal systems. In this paper we add optimality considerations to the setting. We distinguish between quality considerations (for example, size - the smaller a system is, the better it is), and pricing (for example, the payment to the company who manufactured the component). We study the problem of designing systems with minimal quality-cost and price. A key point is that while the quality cost is individual - the choices of a designer are independent of choices made by other designers that use the same library, pricing gives rise to a resource-allocation game - designers that use the same component share its price, with the share being proportional to the number of uses (a component can be used several times in a design). We study both closed and open settings, and in both we solve the problem of finding an optimal design. In a setting with multiple designers, we also study the game-theoretic problems of the induced resource-allocation game."}],"day":"15","citation":{"ama":"Avni G, Kupferman O. Synthesis from component libraries with costs. <i>Theoretical Computer Science</i>. 2018;712:50-72. doi:<a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">10.1016/j.tcs.2017.11.001</a>","short":"G. Avni, O. Kupferman, Theoretical Computer Science 712 (2018) 50–72.","mla":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” <i>Theoretical Computer Science</i>, vol. 712, Elsevier, 2018, pp. 50–72, doi:<a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">10.1016/j.tcs.2017.11.001</a>.","ieee":"G. Avni and O. Kupferman, “Synthesis from component libraries with costs,” <i>Theoretical Computer Science</i>, vol. 712. Elsevier, pp. 50–72, 2018.","chicago":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” <i>Theoretical Computer Science</i>. Elsevier, 2018. <a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">https://doi.org/10.1016/j.tcs.2017.11.001</a>.","ista":"Avni G, Kupferman O. 2018. Synthesis from component libraries with costs. Theoretical Computer Science. 712, 50–72.","apa":"Avni, G., &#38; Kupferman, O. (2018). Synthesis from component libraries with costs. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2017.11.001\">https://doi.org/10.1016/j.tcs.2017.11.001</a>"},"intvolume":"       712","doi":"10.1016/j.tcs.2017.11.001","publisher":"Elsevier","language":[{"iso":"eng"}],"type":"journal_article","oa_version":"Published Version","external_id":{"isi":["000424959200003"]},"date_published":"2018-02-15T00:00:00Z","publist_id":"7197","publication":"Theoretical Computer Science","author":[{"last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"year":"2018","date_created":"2018-12-11T11:47:28Z","quality_controlled":"1","page":"50 - 72","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"date_updated":"2023-09-19T10:00:21Z","isi":1,"volume":712,"article_processing_charge":"No","main_file_link":[{"url":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.636.4529","open_access":"1"}],"scopus_import":"1"},{"month":"06","_id":"1338","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_status":"published","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","related_material":{"record":[{"id":"1729","relation":"earlier_version","status":"public"}]},"oa":1,"department":[{"_id":"ToHe"}],"pubrep_id":"656","ec_funded":1,"abstract":[{"text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.","lang":"eng"}],"status":"public","has_accepted_license":"1","day":"01","citation":{"mla":"Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer, 2017, pp. 97–139, doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3. Springer, pp. 97–139, 2017.","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 50(2–3), 97–139.","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>.","ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139. doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, Formal Methods in System Design 50 (2017) 97–139."},"intvolume":"        50","publisher":"Springer","doi":"10.1007/s10703-016-0256-5","type":"journal_article","file_date_updated":"2020-07-14T12:44:44Z","language":[{"iso":"eng"}],"date_published":"2017-06-01T00:00:00Z","oa_version":"Published Version","external_id":{"isi":["000399888900001"]},"author":[{"last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Edmund","full_name":"Clarke, Edmund","last_name":"Clarke"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Leonid","full_name":"Ryzhyk, Leonid","last_name":"Ryzhyk"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","full_name":"Samanta, Roopsha","first_name":"Roopsha"},{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","full_name":"Tarrach, Thorsten","first_name":"Thorsten","last_name":"Tarrach"}],"ddc":["000"],"publication":"Formal Methods in System Design","issue":"2-3","publist_id":"5929","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"date_updated":"2023-09-20T11:13:51Z","year":"2017","date_created":"2018-12-11T11:51:27Z","quality_controlled":"1","page":"97 - 139","isi":1,"file":[{"creator":"system","file_size":1416170,"checksum":"1163dfd997e8212c789525d4178b1653","relation":"main_file","date_updated":"2020-07-14T12:44:44Z","access_level":"open_access","file_id":"4985","content_type":"application/pdf","date_created":"2018-12-12T10:13:05Z","file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf"}],"volume":50,"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)"},"article_processing_charge":"No","scopus_import":"1"},{"language":[{"iso":"eng"}],"type":"journal_article","file_date_updated":"2020-07-14T12:44:46Z","doi":"10.1007/s00236-016-0278-x","publisher":"Springer","publist_id":"5898","publication":"Acta Informatica","issue":"8","author":[{"last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904"},{"orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","first_name":"Calin C","full_name":"Guet, Calin C"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Paixao","first_name":"Tiago","full_name":"Paixao, Tiago","orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"ddc":["006","576"],"oa_version":"Published Version","external_id":{"isi":["000414343200003"]},"date_published":"2017-12-01T00:00:00Z","file":[{"creator":"dernst","file_size":755241,"checksum":"4e661d9135d7f8c342e8e258dee76f3e","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:44:46Z","file_id":"5841","date_created":"2019-01-17T15:57:29Z","content_type":"application/pdf","file_name":"2017_ActaInformatica_Giacobbe.pdf"}],"isi":1,"volume":54,"date_created":"2018-12-11T11:51:32Z","year":"2017","quality_controlled":"1","page":"765 - 787","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"_id":"25B07788-B435-11E9-9278-68D0E5697425","name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","call_identifier":"FP7"}],"date_updated":"2025-05-28T11:57:04Z","publication_identifier":{"issn":["00015903"]},"scopus_import":"1","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)"},"article_processing_charge":"No","publication_status":"published","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1835"}]},"title":"Model checking the evolution of gene regulatory networks","oa":1,"_id":"1351","month":"12","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","pubrep_id":"649","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"status":"public","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"ec_funded":1,"intvolume":"        54","citation":{"mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>, vol. 54, no. 8. Springer, pp. 765–787, 2017.","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787. doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787."},"day":"01","has_accepted_license":"1"},{"language":[{"iso":"eng"}],"arxiv":1,"type":"journal_article","doi":"10.1016/j.nahs.2016.04.006","publisher":"Elsevier","publication":"Nonlinear Analysis: Hybrid Systems","publist_id":"5800","issue":"2","author":[{"full_name":"Svoreňová, Mária","first_name":"Mária","last_name":"Svoreňová"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Cěrná, Ivana","first_name":"Ivana","last_name":"Cěrná"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"external_id":{"arxiv":["1410.5387"],"isi":["000390637000014"]},"oa_version":"Preprint","date_published":"2017-02-01T00:00:00Z","volume":23,"isi":1,"quality_controlled":"1","page":"230 - 253","date_created":"2018-12-11T11:51:50Z","year":"2017","date_updated":"2023-09-20T09:43:09Z","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"scopus_import":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"article_processing_charge":"No","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1689"}]},"oa":1,"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","publication_status":"published","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"02","_id":"1407","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"status":"public","abstract":[{"text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.","lang":"eng"}],"ec_funded":1,"intvolume":"        23","citation":{"ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253."},"day":"01"},{"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166."},"intvolume":"       254","day":"01","status":"public","abstract":[{"text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.","lang":"eng"}],"ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Quantitative fair simulation games","related_material":{"record":[{"id":"5428","status":"public","relation":"earlier_version"}]},"publication_status":"published","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1066","month":"06","scopus_import":"1","article_processing_charge":"No","volume":254,"isi":1,"page":"143 - 166","quality_controlled":"1","year":"2017","date_created":"2018-12-11T11:49:58Z","date_updated":"2023-09-20T12:07:48Z","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication":"Information and Computation","publist_id":"6322","issue":"2","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"oa_version":"None","external_id":{"isi":["000402025600002"]},"date_published":"2017-06-01T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","doi":"10.1016/j.ic.2016.10.006","publisher":"Elsevier"},{"publist_id":"6203","ddc":["004","005"],"author":[{"first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Published Version","date_published":"2017-01-02T00:00:00Z","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:34Z","type":"dissertation","doi":"10.15479/AT:ISTA:TH_730","publisher":"Institute of Science and Technology Austria","publication_identifier":{"issn":["2663-337X"]},"article_processing_charge":"No","file":[{"content_type":"application/pdf","date_created":"2018-12-12T10:11:26Z","file_id":"4880","access_level":"open_access","date_updated":"2020-07-14T12:44:34Z","file_name":"IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf","file_size":1028586,"creator":"system","relation":"main_file","checksum":"1406a681cb737508234fde34766be2c2"}],"page":"163","date_created":"2018-12-11T11:50:27Z","year":"2017","date_updated":"2023-09-07T11:58:34Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"alternative_title":["ISTA Thesis"],"pubrep_id":"730","department":[{"_id":"ToHe"}],"acknowledgement":" First of all, I want to thank my advisor, prof. Thomas A. Henzinger, for his guidance during my PhD program. I am grateful for the freedom I was given to pursue my research interests, and his continuous support. Working with prof. Henzinger was a truly inspiring experience and taught me what it means to be a scientist. I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee, Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic, Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators, and without their help this thesis would not be possible. In addition, I want to thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg Weissenbacher for their advice and reviewing this dissertation. I would especially like to acknowledge the late Helmut Veith, who was a member of my committee. I will remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring scientist. Finally, I would like to thank my colleagues for making my stay at IST such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop, Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten Tarrach, as well as other members of groups Henzinger and Chatterjee. ","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1093"},{"status":"public","relation":"part_of_dissertation","id":"1230"},{"status":"public","relation":"part_of_dissertation","id":"1234"},{"id":"1391","relation":"part_of_dissertation","status":"public"},{"id":"1501","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"1502"},{"id":"2063","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"2167"}]},"title":"Statistical and logical methods for property checking","oa":1,"publication_status":"published","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"01","_id":"1155","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"citation":{"apa":"Daca, P. (2017). <i>Statistical and logical methods for property checking</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>","chicago":"Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>.","ista":"Daca P. 2017. Statistical and logical methods for property checking. Institute of Science and Technology Austria.","mla":"Daca, Przemyslaw. <i>Statistical and Logical Methods for Property Checking</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>.","ieee":"P. Daca, “Statistical and logical methods for property checking,” Institute of Science and Technology Austria, 2017.","short":"P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017.","ama":"Daca P. Statistical and logical methods for property checking. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>"},"day":"02","has_accepted_license":"1","status":"public","abstract":[{"lang":"eng","text":"This dissertation concerns the automatic verification of probabilistic systems and programs with arrays by statistical and logical methods. Although statistical and logical methods are different in nature, we show that they can be successfully combined for system analysis. In the first part of the dissertation we present a new statistical algorithm for the verification of probabilistic systems with respect to unbounded properties, including linear temporal logic. Our algorithm often performs faster than the previous approaches, and at the same time requires less information about the system. In addition, our method can be generalized to unbounded quantitative properties such as mean-payoff bounds. In the second part, we introduce two techniques for comparing probabilistic systems. Probabilistic systems are typically compared using the notion of equivalence, which requires the systems to have the equal probability of all behaviors. However, this notion is often too strict, since probabilities are typically only empirically estimated, and any imprecision may break the relation between processes. On the one hand, we propose to replace the Boolean notion of equivalence by a quantitative distance of similarity. For this purpose, we introduce a statistical framework for estimating distances between Markov chains based on their simulation runs, and we investigate which distances can be approximated in our framework. On the other hand, we propose to compare systems with respect to a new qualitative logic, which expresses that behaviors occur with probability one or a positive probability. This qualitative analysis is robust with respect to modeling errors and applicable to many domains. In the last part, we present a new quantifier-free logic for integer arrays, which allows us to express counting. Counting properties are prevalent in array-manipulating programs, however they cannot be expressed in the quantified fragments of the theory of arrays. We present a decision procedure for our logic, and provide several complexity results."}],"degree_awarded":"PhD","ec_funded":1},{"abstract":[{"text":"We define the . model-measuring problem: given a model . M and specification . ϕ, what is the maximal distance . ρ such that all models . M' within distance . ρ from . M satisfy (or violate) . ϕ. The model-measuring problem presupposes a distance function on models. We concentrate on . automatic distance functions, which are defined by weighted automata. The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification; robustness problems that measure how much a model can be perturbed without violating the specification; and parameter synthesis for hybrid systems. We show that for automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular branching-time, and (c) hybrid specifications, the model-measuring problem can be solved.We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for word, tree, and hybrid automata by the . optimal-value question for the weighted versions of these automata. For automata over words and trees, we consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. For hybrid automata, we consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete) weighted automata.We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications. Further, we propose the modeling framework for model measuring to ease the specification and reduce the likelihood of errors in modeling.Finally, we present a variant of the model-measuring problem, called the . model-repair problem. The model-repair problem applies to models that do not satisfy the specification; it can be used to derive restrictions, under which the model satisfies the specification, i.e., to repair the model.","lang":"eng"}],"status":"public","ec_funded":1,"intvolume":"        23","citation":{"short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23:166-190. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>","apa":"Henzinger, T. A., &#38; Otop, J. (2017). Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>.","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, Elsevier, 2017, pp. 166–90, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23. Elsevier, pp. 166–190, 2017."},"day":"01","publication_status":"published","title":"Model measuring for discrete and hybrid systems","_id":"1196","month":"02","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this article is available via: https://repository.ist.ac.at/171/","department":[{"_id":"ToHe"}],"isi":1,"volume":23,"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_updated":"2023-09-20T11:18:50Z","year":"2017","date_created":"2018-12-11T11:50:39Z","page":"166 - 190","quality_controlled":"1","scopus_import":"1","article_processing_charge":"No","type":"journal_article","language":[{"iso":"eng"}],"publisher":"Elsevier","doi":"10.1016/j.nahs.2016.09.001","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"6154","publication":"Nonlinear Analysis: Hybrid Systems","date_published":"2017-02-01T00:00:00Z","external_id":{"isi":["000390637000011"]},"oa_version":"None"},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"publication_identifier":{"issn":["18605974"]},"scopus_import":1,"quality_controlled":"1","year":"2017","date_created":"2018-12-11T11:46:37Z","date_updated":"2023-02-23T12:26:25Z","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"volume":13,"file":[{"file_size":279071,"creator":"system","relation":"main_file","checksum":"08041379ba408d40664f449eb5907a8f","content_type":"application/pdf","date_created":"2018-12-12T10:14:37Z","file_id":"5090","date_updated":"2020-07-14T12:46:33Z","access_level":"open_access","file_name":"IST-2015-321-v1+1_main.pdf"},{"file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:33Z","file_id":"5091","content_type":"application/pdf","date_created":"2018-12-12T10:14:38Z","checksum":"08041379ba408d40664f449eb5907a8f","relation":"main_file","creator":"system","file_size":279071}],"oa_version":"Published Version","date_published":"2017-09-13T00:00:00Z","publist_id":"7356","issue":"3","publication":"Logical Methods in Computer Science","ddc":["004"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"doi":"10.23638/LMCS-13(3:23)2017","publisher":"International Federation of Computational Logic","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:33Z","type":"journal_article","day":"13","has_accepted_license":"1","citation":{"short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>."},"intvolume":"        13","ec_funded":1,"status":"public","abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 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 a pushdown automaton 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 the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pubrep_id":"955","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"465","month":"09","title":"Edit distance for pushdown automata","oa":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1610"},{"id":"5438","status":"public","relation":"earlier_version"}]},"publication_status":"published"},{"main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"scopus_import":1,"publication_identifier":{"issn":["15293785"]},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_updated":"2023-02-21T16:48:11Z","year":"2017","date_created":"2018-12-11T11:46:39Z","quality_controlled":"1","volume":18,"date_published":"2017-05-01T00:00:00Z","oa_version":"Submitted Version","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"publication":"ACM Transactions on Computational Logic (TOCL)","issue":"2","publist_id":"7349","publisher":"ACM","doi":"10.1145/3060139","type":"journal_article","language":[{"iso":"eng"}],"day":"01","citation":{"short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017."},"intvolume":"        18","ec_funded":1,"abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. ","lang":"eng"}],"status":"public","article_number":"12","department":[{"_id":"ToHe"}],"month":"05","_id":"471","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1234"}]},"title":"Faster statistical model checking for unbounded temporal properties","oa":1},{"date_published":"2016-01-01T00:00:00Z","oa_version":"Preprint","conference":{"start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","location":"St. Petersburg, FL, USA"},"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"6104","publisher":"Springer","doi":"10.1007/978-3-662-49122-5_16","type":"conference","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1511.02615","open_access":"1"}],"scopus_import":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"date_updated":"2023-09-07T11:58:33Z","year":"2016","date_created":"2018-12-11T11:50:50Z","quality_controlled":"1","page":"328 - 347","volume":9583,"department":[{"_id":"ToHe"}],"acknowledgement":"We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand Michael Tautschnig for help with preparing the experiments. This research 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 (RiSE) and Z211-N23 (Wittgenstein Award).","alternative_title":["LNCS"],"_id":"1230","month":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","title":"Abstraction-driven concolic testing","related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"oa":1,"day":"01","intvolume":"      9583","citation":{"apa":"Daca, P., Gupta, A., &#38; Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347.","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>.","ieee":"P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.","mla":"Daca, Przemyslaw, et al. <i>Abstraction-Driven Concolic Testing</i>. Vol. 9583, Springer, 2016, pp. 328–47, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>.","short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>"},"ec_funded":1,"abstract":[{"lang":"eng","text":"Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average."}],"status":"public"},{"acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund  (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"alternative_title":["LNCS"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1234","related_material":{"record":[{"relation":"later_version","status":"public","id":"471"},{"status":"public","relation":"dissertation_contains","id":"1155"}]},"title":"Faster statistical model checking for unbounded temporal properties","oa":1,"publication_status":"published","day":"01","citation":{"ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","mla":"Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129."},"intvolume":"      9636","ec_funded":1,"abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.","lang":"eng"}],"status":"public","date_published":"2016-01-01T00:00:00Z","oa_version":"Preprint","conference":{"end_date":"2016-04-08","location":"Eindhoven, The Netherlands","start_date":"2016-04-02","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"6099","publisher":"Springer","doi":"10.1007/978-3-662-49674-9_7","type":"conference","language":[{"iso":"eng"}],"scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"date_updated":"2023-09-07T11:58:33Z","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"page":"112 - 129","quality_controlled":"1","date_created":"2018-12-11T11:50:51Z","year":"2016","volume":9636},{"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1506.01233"}],"scopus_import":1,"volume":9583,"date_created":"2018-12-11T11:52:32Z","year":"2016","quality_controlled":"1","page":"250 - 267","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"date_updated":"2021-01-12T06:51:23Z","publist_id":"5647","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha","full_name":"Samanta, Roopsha"}],"conference":{"start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","location":"St. Petersburg, FL, USA"},"oa_version":"Preprint","date_published":"2016-01-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","doi":"10.1007/978-3-662-49122-5_12","publisher":"Springer","citation":{"ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.","mla":"Henzinger, Thomas A., et al. <i>Lipschitz Robustness of Timed I/O Systems</i>. Vol. 9583, Springer, 2016, pp. 250–67, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>.","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Timed I/O Systems,” 9583:250–67. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2016). Lipschitz robustness of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>","ista":"Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 250–267."},"intvolume":"      9583","day":"01","status":"public","abstract":[{"text":"We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system 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 over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems — timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem.","lang":"eng"}],"ec_funded":1,"alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.","publication_status":"published","title":"Lipschitz robustness of timed I/O systems","oa":1,"_id":"1526","month":"01","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"department":[{"_id":"ToHe"}],"pubrep_id":"457","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1705","month":"08","title":"Guided search for hybrid systems based on coarse-grained space abstractions","oa":1,"publication_status":"published","has_accepted_license":"1","day":"01","intvolume":"        18","citation":{"ama":"Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. 2016;18(4):449-467. doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>","short":"S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski, M. Wehrle, International Journal on Software Tools for Technology Transfer 18 (2016) 449–467.","ieee":"S. Bogomolov <i>et al.</i>, “Guided search for hybrid systems based on coarse-grained space abstractions,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4. Springer, pp. 449–467, 2016.","mla":"Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>.","chicago":"Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson, Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer, 2016. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>.","ista":"Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions. International Journal on Software Tools for Technology Transfer. 18(4), 449–467.","apa":"Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., … Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>"},"ec_funded":1,"abstract":[{"text":"Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.","lang":"eng"}],"status":"public","date_published":"2016-08-01T00:00:00Z","oa_version":"Published Version","ddc":["000"],"author":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"full_name":"Donzé, Alexandre","first_name":"Alexandre","last_name":"Donzé"},{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"},{"full_name":"Ladan, Hamed","first_name":"Hamed","last_name":"Ladan"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"},{"first_name":"Martin","full_name":"Wehrle, Martin","last_name":"Wehrle"}],"issue":"4","publist_id":"5431","publication":"International Journal on Software Tools for Technology Transfer","publisher":"Springer","doi":"10.1007/s10009-015-0393-y","file_date_updated":"2020-07-14T12:45:13Z","type":"journal_article","language":[{"iso":"eng"}],"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)"},"article_processing_charge":"Yes (via OA deal)","scopus_import":1,"date_updated":"2021-01-12T06:52:38Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"page":"449 - 467","quality_controlled":"1","date_created":"2018-12-11T11:53:34Z","year":"2016","volume":18,"file":[{"file_name":"IST-2016-457-v1+1_s10009-015-0393-y.pdf","content_type":"application/pdf","file_id":"5146","date_created":"2018-12-12T10:15:26Z","date_updated":"2020-07-14T12:45:13Z","access_level":"open_access","relation":"main_file","checksum":"31561d7705599a9bd4ea816accc0752e","file_size":2296522,"creator":"system"}]},{"scopus_import":1,"file":[{"file_name":"IST-2016-645-v1+1_sagt-cr.pdf","date_updated":"2020-07-14T12:44:45Z","access_level":"open_access","content_type":"application/pdf","date_created":"2018-12-12T10:14:22Z","file_id":"5073","checksum":"0825eefd4e22774f6f62cb7d7389b05a","relation":"main_file","creator":"system","file_size":243458}],"volume":9928,"project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"date_updated":"2023-08-17T13:52:49Z","date_created":"2018-12-11T11:51:28Z","year":"2016","page":"153 - 166","quality_controlled":"1","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"ddc":["000"],"publist_id":"5926","date_published":"2016-09-01T00:00:00Z","conference":{"start_date":"2016-09-19","name":"SAGT: Symposium on Algorithmic Game Theory","end_date":"2016-09-21","location":"Liverpool, United Kingdom"},"oa_version":"Preprint","type":"conference","file_date_updated":"2020-07-14T12:44:45Z","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-662-53354-3_13","intvolume":"      9928","citation":{"short":"G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>","ista":"Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games,” 9928:153–66. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 153–166.","mla":"Avni, Guy, et al. <i>Dynamic Resource Allocation Games</i>. Vol. 9928, Springer, 2016, pp. 153–66, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>."},"has_accepted_license":"1","day":"01","abstract":[{"text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.","lang":"eng"}],"status":"public","ec_funded":1,"pubrep_id":"645","alternative_title":["LNCS"],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"publication_status":"published","oa":1,"title":"Dynamic resource allocation games","related_material":{"record":[{"relation":"later_version","status":"public","id":"6761"}]},"month":"09","_id":"1341","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","full_name":"Fu, Hongfei","last_name":"Fu"},{"last_name":"Goharshady","full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5824","date_published":"2016-07-01T00:00:00Z","conference":{"end_date":"2016-07-23","location":"Toronto, Canada","start_date":"2016-07-17","name":"CAV: Computer Aided Verification"},"oa_version":"Preprint","type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-41528-4_1","scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1604.07169"}],"volume":9779,"date_updated":"2024-03-25T23:30:18Z","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"page":"3 - 22","quality_controlled":"1","year":"2016","date_created":"2018-12-11T11:51:43Z","alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"title":"Termination analysis of probabilistic programs through Positivstellensatz's","oa":1,"publication_status":"published","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1386","month":"07","citation":{"ama":"Chatterjee K, Fu H, Goharshady AK. Termination analysis of probabilistic programs through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">10.1007/978-3-319-41528-4_1</a>","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Termination analysis of probabilistic programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9779, pp. 3–22.","mla":"Chatterjee, Krishnendu, et al. <i>Termination Analysis of Probabilistic Programs through Positivstellensatz’s</i>. Vol. 9779, Springer, 2016, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">10.1007/978-3-319-41528-4_1</a>.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Termination Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">https://doi.org/10.1007/978-3-319-41528-4_1</a>.","ista":"Chatterjee K, Fu H, Goharshady AK. 2016. Termination analysis of probabilistic programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS, vol. 9779, 3–22.","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2016). Termination analysis of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">https://doi.org/10.1007/978-3-319-41528-4_1</a>"},"intvolume":"      9779","day":"01","abstract":[{"lang":"eng","text":"We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz's, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs."}],"status":"public","ec_funded":1},{"language":[{"iso":"eng"}],"publication_status":"published","title":"On recurrent reachability for continuous linear dynamical systems","oa":1,"type":"conference","_id":"1389","month":"07","doi":"10.1145/2933575.2934548","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"IEEE","publist_id":"5820","publication":"LICS '16","author":[{"last_name":"Chonev","full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ouaknine, Joël","first_name":"Joël","last_name":"Ouaknine"},{"full_name":"Worrell, James","first_name":"James","last_name":"Worrell"}],"oa_version":"Preprint","conference":{"location":"New York, NY, USA","end_date":"2018-07-08","name":"LICS: Logic in Computer Science","start_date":"2018-07-05"},"department":[{"_id":"KrCh"}],"date_published":"2016-07-05T00:00:00Z","status":"public","abstract":[{"text":"The continuous evolution of a wide variety of systems, including continous-time Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt = Ax reaches a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R≥0 --&gt; R satisfying a given linear\r\ndifferential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.","lang":"eng"}],"year":"2016","date_created":"2018-12-11T11:51:44Z","page":"515 - 524","quality_controlled":"1","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"ec_funded":1,"date_updated":"2021-01-12T06:50:20Z","main_file_link":[{"url":"https://arxiv.org/abs/1507.03632","open_access":"1"}],"citation":{"short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.","ama":"Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous linear dynamical systems. In: <i>LICS ’16</i>. IEEE; 2016:515-524. doi:<a href=\"https://doi.org/10.1145/2933575.2934548\">10.1145/2933575.2934548</a>","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” In <i>LICS ’16</i>, 515–24. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2934548\">https://doi.org/10.1145/2933575.2934548</a>.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.","apa":"Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On recurrent reachability for continuous linear dynamical systems. In <i>LICS ’16</i> (pp. 515–524). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2934548\">https://doi.org/10.1145/2933575.2934548</a>","mla":"Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” <i>LICS ’16</i>, IEEE, 2016, pp. 515–24, doi:<a href=\"https://doi.org/10.1145/2933575.2934548\">10.1145/2933575.2934548</a>.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for continuous linear dynamical systems,” in <i>LICS ’16</i>, New York, NY, USA, 2016, pp. 515–524."},"scopus_import":1,"day":"05"},{"alternative_title":["LNCS"],"publist_id":"5819","author":[{"first_name":"Loris","full_name":"D'Antoni, Loris","last_name":"D'Antoni"},{"full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Singh","first_name":"Rishabh","full_name":"Singh, Rishabh"}],"conference":{"location":"Toronto, Canada","end_date":"2016-07-23","name":"CAV: Computer Aided Verification","start_date":"2016-07-17"},"oa_version":"None","date_published":"2016-07-13T00:00:00Z","department":[{"_id":"ToHe"}],"title":"QLOSE: Program repair with quantitative objectives","publication_status":"published","language":[{"iso":"eng"}],"type":"conference","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-319-41540-6_21","_id":"1390","month":"07","publisher":"Springer","scopus_import":1,"citation":{"short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.","ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>","apa":"D’Antoni, L., Samanta, R., &#38; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>.","mla":"D’Antoni, Loris, et al. <i>QLOSE: Program Repair with Quantitative Objectives</i>. Vol. 9780, Springer, 2016, pp. 383–401, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>.","ieee":"L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 383–401."},"intvolume":"      9780","day":"13","status":"public","volume":9780,"abstract":[{"lang":"eng","text":"The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect\r\nto a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating\r\nQlose on programs taken from educational tools such as CodeHunt and edX."}],"quality_controlled":"1","page":"383 - 401","date_created":"2018-12-11T11:51:45Z","year":"2016","date_updated":"2021-01-12T06:50:21Z","ec_funded":1,"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}]},{"doi":"10.1007/978-3-319-41540-6_13","publisher":"Springer","language":[{"iso":"eng"}],"type":"conference","conference":{"location":"Toronto, Canada","end_date":"2016-07-23","name":"CAV: Computer Aided Verification","start_date":"2016-07-17"},"oa_version":"Preprint","date_published":"2016-07-13T00:00:00Z","publist_id":"5818","author":[{"first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","full_name":"Kupriyanov, Andrey","first_name":"Andrey","last_name":"Kupriyanov"}],"year":"2016","date_created":"2018-12-11T11:51:45Z","quality_controlled":"1","page":"230 - 248","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-07T11:58:33Z","volume":9780,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1603.06850"}],"scopus_import":1,"month":"07","_id":"1391","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","oa":1,"title":"Array folds logic","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"ec_funded":1,"status":"public","abstract":[{"text":"We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as &quot;the first array cell contains the array length,&quot; and &quot;the array contains equally many minimal and maximal elements.&quot; These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability.\r\nAFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.","lang":"eng"}],"day":"13","intvolume":"      9780","citation":{"ieee":"P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 230–248.","mla":"Daca, Przemyslaw, et al. <i>Array Folds Logic</i>. Vol. 9780, Springer, 2016, pp. 230–48, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>.","ista":"Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer Aided Verification, LNCS, vol. 9780, 230–248.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds Logic,” 9780:230–48. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>.","apa":"Daca, P., Henzinger, T. A., &#38; Kupriyanov, A. (2016). Array folds logic (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>","ama":"Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer; 2016:230-248. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>","short":"P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248."}},{"publist_id":"5786","author":[{"first_name":"Stanley","full_name":"Bak, Stanley","last_name":"Bak"},{"last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"},{"last_name":"Prakash","first_name":"Pradyot","full_name":"Prakash, Pradyot"}],"conference":{"end_date":"2016-04-14","location":"Vienna, Austria","start_date":"2016-04-12","name":"HSCC 2016: International Conference on Hybrid Systems: Computation and Control"},"oa_version":"None","date_published":"2016-04-11T00:00:00Z","department":[{"_id":"ToHe"}],"title":"Scalable static hybridization methods for analysis of nonlinear systems","language":[{"iso":"eng"}],"publication_status":"published","type":"conference","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1421","doi":"10.1145/2883817.2883837","month":"04","publisher":"Springer","scopus_import":1,"citation":{"ama":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>","short":"S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer, 2016, pp. 155–164.","mla":"Bak, Stanley, et al. <i>Scalable Static Hybridization Methods for Analysis of Nonlinear Systems</i>. Springer, 2016, pp. 155–64, doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>.","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable static hybridization methods for analysis of nonlinear systems,” presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria, 2016, pp. 155–164.","ista":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static hybridization methods for analysis of nonlinear systems. HSCC 2016: International Conference on Hybrid Systems: Computation and Control, 155–164.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear Systems,” 155–64. Springer, 2016. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., &#38; Prakash, P. (2016). Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164). Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>"},"day":"11","status":"public","abstract":[{"lang":"eng","text":"Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Several such recent approaches advocate that only &quot;dynamic&quot; hybridization techniquesi.e., those where the dynamics are abstracted on-The-fly during a reachability computation are effective. In this paper, we demonstrate this is not the case, and create static hybridization methods that are more scalable than earlier approaches. The main insight in our approach is that quick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitions between domains are generally timetriggered, avoiding accumulated error from geometric intersections. We enhance our static technique by combining time-Triggered transitions with occasional space-Triggered transitions, and demonstrate the benefits of the combined approach in what we call mixed-Triggered hybridization. Finally, error modes are inserted to confirm that the reachable states stay within the hybridized regions. The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottleneck for many dynamic hybridization approaches: The nonlinear optimization required for sound dynamics abstraction. We implement our method as a model transformation pass in the HYST tool, and perform reachability analysis and evaluation using an unmodified version of SpaceEx on nonlinear models with up to six dimensions."}],"page":"155 - 164","quality_controlled":"1","date_created":"2018-12-11T11:51:55Z","year":"2016","ec_funded":1,"date_updated":"2021-01-12T06:50:37Z","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}]},{"publisher":"ACM","doi":"10.1145/2837614.2837650","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-01-11T00:00:00Z","conference":{"end_date":"2016-01-22","location":"St. Petersburg, FL, USA","start_date":"2016-01-20","name":"POPL: Principles of Programming Languages"},"oa_version":"Preprint","author":[{"full_name":"Dragoi, Cezara","first_name":"Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"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","full_name":"Zufferey, Damien","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"publist_id":"5759","date_updated":"2021-01-12T06:50:45Z","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"page":"400 - 415","quality_controlled":"1","date_created":"2018-12-11T11:52:01Z","year":"2016","volume":"20-22","scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://hal.inria.fr/hal-01251199/"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1439","month":"01","oa":1,"title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","publication_status":"published","department":[{"_id":"ToHe"}],"acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","alternative_title":["ACM SIGPLAN Notices"],"ec_funded":1,"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. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.","lang":"eng"}],"status":"public","day":"11","citation":{"ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous language for fault-tolerant distributed algorithms,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.","mla":"Dragoi, Cezara, et al. <i>PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms</i>. Vol. 20–22, ACM, 2016, pp. 400–15, doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2016). PSYNC: A partially synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp. 400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>","ista":"Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>.","ama":"Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415."}}]