[{"citation":{"apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","short":"A. Fellner, (2015).","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>."},"has_accepted_license":"1","oa_version":"Published Version","related_material":{"record":[{"status":"public","relation":"popular_science","id":"1603"}]},"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","oa":1,"author":[{"last_name":"Fellner","full_name":"Fellner, Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"license":"https://creativecommons.org/publicdomain/zero/1.0/","article_processing_charge":"No","_id":"5549","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"month":"08","publisher":"Institute of Science and Technology Austria","type":"research_data","datarep_id":"28","day":"13","status":"public","file":[{"creator":"system","access_level":"open_access","date_updated":"2020-07-14T12:47:00Z","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","file_size":49557109,"file_id":"5597","checksum":"b8bcb43c0893023cda66c1b69c16ac62","relation":"main_file","date_created":"2018-12-12T13:02:31Z","content_type":"application/zip"}],"file_date_updated":"2020-07-14T12:47:00Z","contributor":[{"first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"}],"abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"ec_funded":1,"doi":"10.15479/AT:ISTA:28","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png"},"date_updated":"2025-09-23T08:23:15Z","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"}],"ddc":["004"],"date_published":"2015-08-13T00:00:00Z","year":"2015","publist_id":"5564","date_created":"2018-12-12T12:31:29Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"file":[{"file_size":399462,"date_updated":"2020-07-14T12:45:22Z","file_name":"IST-2015-317-v1+1_author_version.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","date_created":"2018-12-12T10:17:56Z","relation":"main_file","checksum":"f0d4395b600f410a191256ac0b73af32","file_id":"5314"}],"file_date_updated":"2020-07-14T12:45:22Z","doi":"10.1145/2676726.2677008","abstract":[{"text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.","lang":"eng"}],"department":[{"_id":"ToHe"}],"publication_status":"published","conference":{"name":"POPL: Principles of Programming Languages","end_date":"2015-01-17","start_date":"2015-01-15","location":"Mumbai, India"},"date_updated":"2025-03-07T08:44:29Z","ddc":["005"],"date_published":"2015-01-15T00:00:00Z","date_created":"2018-12-11T11:55:05Z","year":"2015","publist_id":"5091","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","pubrep_id":"317","citation":{"apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>."},"scopus_import":"1","oa_version":"Submitted Version","title":"Succinct representation of concurrent trace sets","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun"},{"first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","full_name":"Samanta, Roopsha"},{"full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","first_name":"Thorsten"}],"oa":1,"language":[{"iso":"eng"}],"_id":"1992","article_processing_charge":"No","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publisher":"ACM","month":"01","quality_controlled":"1","status":"public","page":"433 - 444","type":"conference","day":"15"},{"date_published":"2015-06-10T00:00:00Z","project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"ddc":["000","570"],"date_updated":"2025-04-15T06:50:01Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"volume":3,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2022-02-25T11:42:25Z","year":"2015","file_date_updated":"2022-02-25T11:55:26Z","intvolume":"         3","file":[{"date_created":"2022-02-25T11:55:26Z","success":1,"content_type":"application/pdf","file_id":"10795","checksum":"26c222487564e1be02a11d688d6f769d","relation":"main_file","access_level":"open_access","date_updated":"2022-02-25T11:55:26Z","file_name":"2015_FrontiersEnvironmScience_Parise.pdf","file_size":1371201,"creator":"dernst"}],"publication":"Frontiers in Environmental Science","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publication_status":"published","doi":"10.3389/fenvs.2015.00042","ec_funded":1,"abstract":[{"text":"Mathematical models are of fundamental importance in the understanding of complex population dynamics. For instance, they can be used to predict the population evolution starting from different initial conditions or to test how a system responds to external perturbations. For this analysis to be meaningful in real applications, however, it is of paramount importance to choose an appropriate model structure and to infer the model parameters from measured data. While many parameter inference methods are available for models based on deterministic ordinary differential equations, the same does not hold for more detailed individual-based models. Here we consider, in particular, stochastic models in which the time evolution of the species abundances is described by a continuous-time Markov chain. These models are governed by a master equation that is typically difficult to solve. Consequently, traditional inference methods that rely on iterative evaluation of parameter likelihoods are computationally intractable. The aim of this paper is to present recent advances in parameter inference for continuous-time Markov chain models, based on a moment closure approximation of the parameter likelihood, and to investigate how these results can help in understanding, and ultimately controlling, complex systems in ecology. Specifically, we illustrate through an agricultural pest case study how parameters of a stochastic individual-based model can be identified from measured data and how the resulting model can be used to solve an optimal control problem in a stochastic setting. In particular, we show how the matter of determining the optimal combination of two different pest control methods can be formulated as a chance constrained optimization problem where the control action is modeled as a state reset, leading to a hybrid system formulation.","lang":"eng"}],"_id":"10794","corr_author":"1","keyword":["General Environmental Science"],"article_type":"original","article_processing_charge":"No","license":"https://creativecommons.org/licenses/by/4.0/","author":[{"first_name":"Francesca","full_name":"Parise, Francesca","last_name":"Parise"},{"last_name":"Lygeros","full_name":"Lygeros, John","first_name":"John"},{"first_name":"Jakob","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282","full_name":"Ruess, Jakob","last_name":"Ruess"}],"oa":1,"language":[{"iso":"eng"}],"status":"public","day":"10","type":"journal_article","publisher":"Frontiers","publication_identifier":{"issn":["2296-665X"]},"article_number":"42","month":"06","quality_controlled":"1","has_accepted_license":"1","citation":{"short":"F. Parise, J. Lygeros, J. Ruess, Frontiers in Environmental Science 3 (2015).","ieee":"F. Parise, J. Lygeros, and J. Ruess, “Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study,” <i>Frontiers in Environmental Science</i>, vol. 3. Frontiers, 2015.","ama":"Parise F, Lygeros J, Ruess J. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. 2015;3. doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>","apa":"Parise, F., Lygeros, J., &#38; Ruess, J. (2015). Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. Frontiers. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>","ista":"Parise F, Lygeros J, Ruess J. 2015. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. 3, 42.","chicago":"Parise, Francesca, John Lygeros, and Jakob Ruess. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>. Frontiers, 2015. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>.","mla":"Parise, Francesca, et al. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>, vol. 3, 42, Frontiers, 2015, doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>."},"title":"Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study","oa_version":"Published Version","acknowledgement":"The authors would like to acknowledge contributions from Baptiste Mottet who performed preliminary analysis regarding parameter inference for the considered case study in a student project (Mottet, 2014/2015).\r\nThe research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement No. [291734] and from SystemsX under the project SignalX.","scopus_import":"1"},{"OA_place":"repository","status":"public","page":"180 - 197","day":"01","type":"conference","publisher":"Springer","quality_controlled":"1","month":"07","_id":"1729","article_processing_charge":"No","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Edmund","full_name":"Clarke, Edmund","last_name":"Clarke"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun"},{"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"},{"first_name":"Thorsten","full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"oa":1,"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","related_material":{"record":[{"relation":"later_version","status":"public","id":"1338"},{"relation":"dissertation_contains","status":"public","id":"1130"}]},"isi":1,"OA_type":"green","scopus_import":"1","oa_version":"Submitted Version","has_accepted_license":"1","pubrep_id":"336","citation":{"mla":"Cerny, Pavol, et al. <i>From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis</i>. Vol. 9207, Springer, 2015, pp. 180–97, doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</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.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.","ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. 2015;9207:180-197. doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using synchronization synthesis. Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2015. From non-preemptive to preemptive scheduling using synchronization synthesis. 9207, 180–197."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T11:53:42Z","publist_id":"5398","year":"2015","date_published":"2015-07-01T00:00:00Z","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"ddc":["000"],"conference":{"start_date":"2015-07-18","location":"San Francisco, CA, United States","name":"CAV: Computer Aided Verification","end_date":"2015-07-24"},"date_updated":"2026-04-09T10:54:00Z","series_title":"Lecture Notes in Computer Science","volume":9207,"department":[{"_id":"ToHe"}],"external_id":{"isi":["000491470400011"]},"publication_status":"published","doi":"10.1007/978-3-319-21668-3_11","alternative_title":["LNCS"],"abstract":[{"lang":"eng","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 such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. 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, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions."}],"ec_funded":1,"file_date_updated":"2025-06-26T07:12:35Z","intvolume":"      9207","file":[{"checksum":"6ff58ac220e2f20cb001ba35d4924495","file_id":"4715","relation":"main_file","date_created":"2018-12-12T10:08:53Z","content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2015-336-v1+1_long_version.pdf","date_updated":"2025-06-26T07:12:35Z","file_size":481922}]},{"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques"},{"name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"date_published":"2015-12-01T00:00:00Z","volume":245,"date_updated":"2025-09-23T10:32:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","main_file_link":[{"url":"http://arxiv.org/abs/1006.0673","open_access":"1"}],"date_created":"2018-12-11T11:53:42Z","year":"2015","publist_id":"5395","intvolume":"       245","publication":"Information and Computation","external_id":{"isi":["000368899100002"],"arxiv":["1006.0673"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","doi":"10.1016/j.ic.2015.06.003","ec_funded":1,"abstract":[{"lang":"eng","text":"We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (both players interact simultaneously); and (b) turn-based (both players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. In this work we present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. "}],"issue":"12","_id":"1731","corr_author":"1","article_processing_charge":"No","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"last_name":"Gimbert","full_name":"Gimbert, Hugo","first_name":"Hugo"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"oa":1,"page":"3 - 16","status":"public","type":"journal_article","day":"01","publisher":"Elsevier","quality_controlled":"1","month":"12","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>.","mla":"Chatterjee, Krishnendu, et al. “Randomness for Free.” <i>Information and Computation</i>, vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” <i>Information and Computation</i>, vol. 245, no. 12. Elsevier, pp. 3–16, 2015.","short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","ama":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. <i>Information and Computation</i>. 2015;245(12):3-16. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2015). Randomness for free. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16."},"arxiv":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"3856"}]},"title":"Randomness for free","isi":1,"oa_version":"Preprint","scopus_import":"1"},{"citation":{"ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>","short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015).","apa":"Gupta, A., &#38; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>","ista":"Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 25(2), 7.","mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 7, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>."},"publication":"ACM Transactions on Modeling and Computer Simulation","intvolume":"        25","isi":1,"doi":"10.1145/2745799","scopus_import":"1","oa_version":"None","external_id":{"isi":["000354789200001"]},"department":[{"_id":"ToHe"}],"title":"Guest editors' introduction to special issue on computational methods in systems biology","publication_status":"published","author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"}],"language":[{"iso":"eng"}],"volume":25,"date_updated":"2025-09-23T09:11:51Z","_id":"1808","issue":"2","article_processing_charge":"No","date_published":"2015-05-01T00:00:00Z","article_number":"7","publisher":"ACM","date_created":"2018-12-11T11:54:07Z","year":"2015","publist_id":"5302","quality_controlled":"1","month":"05","status":"public","type":"journal_article","day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"external_id":{"arxiv":["1410.7704"]},"publication_status":"published","doi":"10.1007/978-3-662-46681-0_47","alternative_title":["LNCS"],"ec_funded":1,"abstract":[{"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 logics. 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.","lang":"eng"}],"intvolume":"      9035","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:54:16Z","main_file_link":[{"url":"http://arxiv.org/abs/1410.7704","open_access":"1"}],"publist_id":"5267","year":"2015","date_published":"2015-04-01T00:00:00Z","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091","call_identifier":"FP7","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation"},{"call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation"},{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"}],"conference":{"location":"London, United Kingdom","start_date":"2015-04-11","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2015-04-18"},"date_updated":"2025-07-10T11:50:42Z","series_title":"Lecture Notes in Computer Science","volume":9035,"title":"Model checking gene regulatory networks","related_material":{"record":[{"id":"1351","status":"public","relation":"later_version"}]},"acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","oa_version":"Preprint","scopus_import":"1","arxiv":1,"citation":{"ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>.","mla":"Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol. 9035, Springer, 2015, pp. 469–83, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>."},"page":"469 - 483","status":"public","day":"01","type":"conference","publisher":"Springer","quality_controlled":"1","month":"04","_id":"1835","article_processing_charge":"No","author":[{"last_name":"Giacobbe","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet","first_name":"Calin C"},{"first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Tiago","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","full_name":"Paixao, Tiago","orcid":"0000-0003-2361-3953","last_name":"Paixao"},{"first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"language":[{"iso":"eng"}]},{"status":"public","page":"105 - 131","type":"conference","day":"01","publisher":"Springer","month":"04","quality_controlled":"1","_id":"1836","article_processing_charge":"No","author":[{"first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","last_name":"Cerny"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Kovács","full_name":"Kovács, Laura","first_name":"Laura"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zwirchmayr","full_name":"Zwirchmayr, Jakob","first_name":"Jakob"}],"language":[{"iso":"eng"}],"title":"Segment abstraction for worst-case execution time analysis","isi":1,"oa_version":"None","scopus_import":"1","citation":{"apa":"Cerny, P., Henzinger, T. A., Kovács, L., Radhakrishna, A., &#38; Zwirchmayr, J. (2015). Segment abstraction for worst-case execution time analysis. Presented at the ESOP: European Symposium on Programming, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>","ista":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. 2015. Segment abstraction for worst-case execution time analysis. 9032, 105–131.","ama":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. Segment abstraction for worst-case execution time analysis. 2015;9032:105-131. doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>","ieee":"P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr, “Segment abstraction for worst-case execution time analysis,” vol. 9032. Springer, pp. 105–131, 2015.","short":"P. Cerny, T.A. Henzinger, L. Kovács, A. Radhakrishna, J. Zwirchmayr, 9032 (2015) 105–131.","chicago":"Cerny, Pavol, Thomas A Henzinger, Laura Kovács, Arjun Radhakrishna, and Jakob Zwirchmayr. “Segment Abstraction for Worst-Case Execution Time Analysis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>.","mla":"Cerny, Pavol, et al. <i>Segment Abstraction for Worst-Case Execution Time Analysis</i>. Vol. 9032, Springer, 2015, pp. 105–31, doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T11:54:16Z","year":"2015","publist_id":"5266","project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_published":"2015-04-01T00:00:00Z","conference":{"name":"ESOP: European Symposium on Programming","end_date":"2015-04-18","location":"London, United Kingdom","start_date":"2015-04-11"},"volume":9032,"series_title":"Lecture Notes in Computer Science","date_updated":"2025-09-23T10:42:04Z","external_id":{"isi":["000361751400005"]},"department":[{"_id":"ToHe"}],"publication_status":"published","alternative_title":["LNCS"],"doi":"10.1007/978-3-662-46669-8_5","ec_funded":1,"abstract":[{"text":"In the standard framework for worst-case execution time (WCET) analysis of programs, the main data structure is a single instance of integer linear programming (ILP) that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate forWCET, and it must be refined if the estimate is not tight.We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework to obtain parametric estimates of WCET. We experimentally evaluate our approach on a set of examples from WCET benchmark suites and linear-algebra packages. We show that our analysis, with comparable effort, provides WCET estimates that in many cases significantly improve those computed by existing tools.","lang":"eng"}],"intvolume":"      9032"},{"article_processing_charge":"No","issue":"4","_id":"1840","oa":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Bernhard","full_name":"Geiger, Bernhard","last_name":"Geiger"},{"orcid":"0000-0002-9041-0905","full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana"},{"first_name":"Gernot","last_name":"Kubin","full_name":"Kubin, Gernot"},{"last_name":"Koeppl","full_name":"Koeppl, Heinz","first_name":"Heinz"}],"type":"journal_article","day":"01","status":"public","page":"1010 - 1022","month":"04","quality_controlled":"1","publication_identifier":{"issn":["0018-9286"]},"publisher":"IEEE","citation":{"mla":"Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4, IEEE, 2015, pp. 1010–22, doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>.","chicago":"Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>.","apa":"Geiger, B., Petrov, T., Kubin, G., &#38; Koeppl, H. (2015). Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>","ista":"Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.","ieee":"B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation via information bottleneck,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4. IEEE, pp. 1010–1022, 2015.","ama":"Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. 2015;60(4):1010-1022. doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>","short":"B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic Control 60 (2015) 1010–1022."},"arxiv":1,"title":"Optimal Kullback-Leibler aggregation via information bottleneck","oa_version":"Preprint","acknowledgement":"This work was supported by the Austrian Research Association under Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2 128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n","scopus_import":"1","isi":1,"date_published":"2015-04-01T00:00:00Z","volume":60,"date_updated":"2025-09-23T09:45:33Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015","publist_id":"5262","main_file_link":[{"url":"http://arxiv.org/abs/1304.6603","open_access":"1"}],"date_created":"2018-12-11T11:54:18Z","intvolume":"        60","publication":"IEEE Transactions on Automatic Control","publication_status":"published","external_id":{"isi":["000351731600009"],"arxiv":["1304.6603"]},"department":[{"_id":"CaGu"},{"_id":"ToHe"}],"abstract":[{"text":"In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions.","lang":"eng"}],"doi":"10.1109/TAC.2014.2364971"},{"oa":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Soham","last_name":"Chakraborty","full_name":"Chakraborty, Soham"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Sezgin","full_name":"Sezgin, Ali","first_name":"Ali"},{"last_name":"Vafeiadis","full_name":"Vafeiadis, Viktor","first_name":"Viktor"}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","article_type":"original","article_processing_charge":"No","issue":"1","_id":"1832","corr_author":"1","quality_controlled":"1","month":"04","article_number":"20","publisher":"International Federation for Computational Logic","type":"journal_article","day":"01","status":"public","citation":{"mla":"Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1, 20, International Federation for Computational Logic, 2015, doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>.","chicago":"Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2015. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>.","ista":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20.","apa":"Chakraborty, S., Henzinger, T. A., Sezgin, A., &#38; Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>","short":"S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015).","ama":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. 2015;11(1). doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>","ieee":"S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1. International Federation for Computational Logic, 2015."},"has_accepted_license":"1","pubrep_id":"390","oa_version":"Published Version","scopus_import":"1","isi":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2328"}]},"title":"Aspect-oriented linearizability proofs","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)"},"volume":11,"date_updated":"2026-07-06T13:24:05Z","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"}],"ddc":["000"],"date_published":"2015-04-01T00:00:00Z","year":"2015","publist_id":"5271","date_created":"2018-12-11T11:54:15Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Logical Methods in Computer Science","intvolume":"        11","file":[{"creator":"system","date_updated":"2020-07-14T12:45:17Z","file_size":380203,"file_name":"IST-2015-390-v1+1_1502.07639.pdf","access_level":"open_access","relation":"main_file","checksum":"7370e164d0a731f442424a92669efc34","file_id":"4881","content_type":"application/pdf","date_created":"2018-12-12T10:11:27Z"}],"file_date_updated":"2020-07-14T12:45:17Z","ec_funded":1,"abstract":[{"text":"Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. ","lang":"eng"}],"doi":"10.2168/LMCS-11(1:20)2015","das_tickbox":"1","publication_status":"published","external_id":{"isi":["000353193000019"]},"department":[{"_id":"ToHe"}]},{"volume":9135,"date_updated":"2026-07-06T13:27:53Z","conference":{"name":"ICALP: Automata, Languages and Programming","end_date":"2015-07-10","start_date":"2015-07-06","location":"Kyoto, Japan"},"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_published":"2015-07-01T00:00:00Z","year":"2015","publist_id":"5556","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"date_created":"2018-12-11T11:53:01Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"42nd International Colloquium on Automata, Languages, and Programming","intvolume":"      9135","abstract":[{"lang":"eng","text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k."}],"ec_funded":1,"alternative_title":["LNCS"],"doi":"10.1007/978-3-662-47666-6_10","publication_status":"published","external_id":{"isi":["000364317900010"],"arxiv":["1504.08259"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"oa":1,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"article_processing_charge":"No","issue":"Part II","_id":"1610","month":"07","quality_controlled":"1","publication_identifier":{"isbn":["978-3-662-47665-9"]},"publisher":"Springer Nature","type":"conference","day":"01","status":"public","page":"121 - 133","OA_place":"repository","citation":{"ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium on Automata, Languages, and Programming</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium on Automata, Languages, and Programming</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium on Automata, Languages, and Programming, Springer Nature, 2015, pp. 121–133.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium on Automata, Languages, and Programming</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium on Automata, Languages, and Programming</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium on Automata, Languages, and Programming</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>."},"arxiv":1,"pubrep_id":"321","oa_version":"Preprint","scopus_import":"1","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects\r\nS11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499-\r\nN23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph\r\nGames), and MSR faculty fellows award.","OA_type":"green","isi":1,"title":"Edit distance for pushdown automata","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5438"},{"status":"public","relation":"later_version","id":"465"}]}},{"OA_type":"green","isi":1,"acknowledgement":"A Technical Report of this paper is available at DOI: 10.15479/AT:IST-2015-318-v1-1\r\n","oa_version":"Preprint","scopus_import":"1","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","related_material":{"record":[{"id":"5429","status":"public","relation":"earlier_version"},{"id":"5435","relation":"earlier_version","status":"public"},{"id":"466","status":"public","relation":"later_version"}]},"citation":{"ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","apa":"Chatterjee, K., Komárková, Z., &#38; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>","short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IEEE, 2015, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>.","chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>."},"publisher":"IEEE","month":"07","quality_controlled":"1","OA_place":"repository","status":"public","page":"244 - 256","day":"01","type":"conference","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Zuzana","full_name":"Komárková, Zuzana","last_name":"Komárková"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"language":[{"iso":"eng"}],"oa":1,"_id":"1657","article_processing_charge":"No","doi":"10.1109/LICS.2015.32","alternative_title":["LICS"],"ec_funded":1,"abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"external_id":{"isi":["000380427100024"]},"publication_status":"published","date_created":"2018-12-11T11:53:18Z","main_file_link":[{"url":"https://doi.org/10.15479/AT:IST-2015-318-v1-1","open_access":"1"}],"publist_id":"5493","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10","name":"LICS: Logic in Computer Science"},"date_updated":"2026-07-06T13:26:26Z","series_title":"LICS","date_published":"2015-07-01T00:00:00Z","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"}]},{"title":"Nested weighted automata","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5415"},{"id":"5436","relation":"earlier_version","status":"public"},{"id":"467","status":"public","relation":"later_version"}]},"oa_version":"Preprint","scopus_import":"1","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","OA_type":"green","isi":1,"arxiv":1,"citation":{"mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>"},"day":"31","type":"conference","OA_place":"repository","status":"public","quality_controlled":"1","month":"07","publisher":"IEEE","article_number":"7174926","article_processing_charge":"No","corr_author":"1","_id":"1656","language":[{"iso":"eng"}],"oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"external_id":{"isi":["000380427100064"],"arxiv":["1606.03598"]},"ec_funded":1,"abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"doi":"10.1109/LICS.2015.72","publication":"Proceedings - Symposium on Logic in Computer Science","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publist_id":"5494","year":"2015","date_created":"2018-12-11T11:53:17Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1606.03598","open_access":"1"}],"date_published":"2015-07-31T00:00:00Z","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"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_updated":"2026-07-07T14:01:10Z","volume":"2015-July","conference":{"location":"Kyoto, Japan","start_date":"2015-07-06","name":"LICS: Logic in Computer Science","end_date":"2015-07-10"}},{"related_material":{"record":[{"id":"5415","status":"public","relation":"earlier_version"},{"status":"public","relation":"later_version","id":"1656"},{"status":"public","relation":"later_version","id":"467"}]},"title":"Nested weighted automata","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time.\r\nIn nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"doi":"10.15479/AT:IST-2015-170-v2-2","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:54Z","file":[{"checksum":"3c402f47d3669c28d04d1af405a08e3f","file_id":"5541","relation":"main_file","date_created":"2018-12-12T11:54:19Z","content_type":"application/pdf","creator":"system","access_level":"open_access","date_updated":"2020-07-14T12:46:54Z","file_size":569991,"file_name":"IST-2015-170-v2+2_report.pdf"}],"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2015.","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p."},"pubrep_id":"331","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"24","type":"technical_report","status":"public","page":"29","month":"04","year":"2015","date_created":"2018-12-12T11:39:19Z","publication_identifier":{"issn":["2664-1690"]},"publisher":"IST Austria","date_published":"2015-04-24T00:00:00Z","ddc":["000"],"_id":"5436","date_updated":"2026-07-07T14:01:10Z","oa":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}]},{"publication":"Proceedings of the 17th international conference on Hybrid systems: computation and control","department":[{"_id":"ToHe"}],"publication_status":"published","doi":"10.1145/2562059.2562130","abstract":[{"lang":"eng","text":"As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.\r\n\r\nThe contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem."}],"ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_published":"2014-04-01T00:00:00Z","conference":{"location":"Berlin, Germany","start_date":"2014-04-15","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2014-04-17"},"date_updated":"2025-06-26T08:32:32Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://doi.org/10.15479/AT:IST-2014-171-v1-1","open_access":"1"}],"date_created":"2018-12-11T11:56:23Z","year":"2014","publist_id":"4751","citation":{"apa":"Henzinger, T. A., &#38; Otop, J. (2014). Model measuring for hybrid systems. In <i>Proceedings of the 17th international conference on Hybrid systems: computation and control</i> (pp. 213–222). Berlin, Germany: Springer. <a href=\"https://doi.org/10.1145/2562059.2562130\">https://doi.org/10.1145/2562059.2562130</a>","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems. Proceedings of the 17th international conference on Hybrid systems: computation and control. HSCC: Hybrid Systems - Computation and Control, 213–222.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for hybrid systems,” in <i>Proceedings of the 17th international conference on Hybrid systems: computation and control</i>, Berlin, Germany, 2014, pp. 213–222.","short":"T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.","ama":"Henzinger TA, Otop J. Model measuring for hybrid systems. In: <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>. Springer; 2014:213-222. doi:<a href=\"https://doi.org/10.1145/2562059.2562130\">10.1145/2562059.2562130</a>","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Hybrid Systems.” <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>, Springer, 2014, pp. 213–22, doi:<a href=\"https://doi.org/10.1145/2562059.2562130\">10.1145/2562059.2562130</a>.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Hybrid Systems.” In <i>Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control</i>, 213–22. Springer, 2014. <a href=\"https://doi.org/10.1145/2562059.2562130\">https://doi.org/10.1145/2562059.2562130</a>."},"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5416"}]},"title":"Model measuring for hybrid systems","OA_type":"green","acknowledgement":"This  work  was  supported  in  part  by  the  Austrian  Science Fund  NFN  RiSE  (Rigorous  Systems  Engineering)  and  by the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).\r\nA Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/171","scopus_import":"1","oa_version":"Preprint","_id":"2217","article_processing_charge":"No","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"language":[{"iso":"eng"}],"oa":1,"status":"public","page":"213 - 222","OA_place":"repository","type":"conference","day":"01","publisher":"Springer","month":"04","quality_controlled":"1"},{"citation":{"ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &#38; Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">https://doi.org/10.1007/978-3-319-08867-9_38</a>","ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">10.1007/978-3-319-08867-9_38</a>","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free synthesis for concurrency,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 568–584.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.","chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">https://doi.org/10.1007/978-3-319-08867-9_38</a>.","mla":"Cerny, Pavol, et al. <i>Regression-Free Synthesis for Concurrency</i>. Vol. 8559, Springer, 2014, pp. 568–84, doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">10.1007/978-3-319-08867-9_38</a>."},"has_accepted_license":"1","pubrep_id":"297","oa_version":"Submitted Version","scopus_import":"1","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1130"}]},"title":"Regression-free synthesis for concurrency","language":[{"iso":"eng"}],"oa":1,"author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ryzhyk, Leonid","last_name":"Ryzhyk","first_name":"Leonid"},{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","full_name":"Tarrach, Thorsten","last_name":"Tarrach","first_name":"Thorsten"}],"_id":"2218","quality_controlled":"1","month":"07","publication_identifier":{"isbn":["978-331908866-2"]},"publisher":"Springer","type":"conference","day":"22","status":"public","page":"568 - 584","file":[{"file_id":"4995","checksum":"a631d3105509f239724644e77a1212e2","relation":"main_file","date_created":"2018-12-12T10:13:14Z","content_type":"application/pdf","creator":"system","access_level":"open_access","file_size":416732,"file_name":"IST-2014-297-v1+1_cav14-final.pdf","date_updated":"2020-07-14T12:45:33Z"},{"creator":"system","file_name":"IST-2014-297-v2+1_cav14-final2.pdf","file_size":616293,"date_updated":"2020-07-14T12:45:33Z","access_level":"open_access","relation":"main_file","file_id":"4996","checksum":"f8b0f748cc9fa697ca992cc56c87bc4e","content_type":"application/pdf","date_created":"2018-12-12T10:13:15Z"}],"intvolume":"      8559","file_date_updated":"2020-07-14T12:45:33Z","abstract":[{"text":"While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.","lang":"eng"}],"ec_funded":1,"alternative_title":["LNCS"],"doi":"10.1007/978-3-319-08867-9_38","publication_status":"published","department":[{"_id":"ToHe"}],"volume":8559,"date_updated":"2026-04-09T10:54:00Z","conference":{"name":"CAV: Computer Aided Verification","end_date":"2014-07-22","start_date":"2014-07-18","location":"Vienna, Austria"},"project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"}],"ddc":["000"],"date_published":"2014-07-22T00:00:00Z","year":"2014","publist_id":"4749","main_file_link":[{"open_access":"1","url":"https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38"}],"date_created":"2018-12-11T11:56:23Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"language":[{"iso":"eng"}],"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","full_name":"Boker, Udi","first_name":"Udi"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"issue":"1","_id":"2239","month":"01","quality_controlled":"1","publication_identifier":{"isbn":["978-145032544-8"]},"publisher":"ACM","type":"conference","day":"13","status":"public","page":"595 - 606","citation":{"apa":"Boker, U., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM. <a href=\"https://doi.org/10.1145/2535838.2535875\">https://doi.org/10.1145/2535838.2535875</a>","ista":"Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems. POPL: Principles of Programming Languages vol. 49, 595–606.","short":"U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.","ama":"Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol 49. ACM; 2014:595-606. doi:<a href=\"https://doi.org/10.1145/2535838.2535875\">10.1145/2535838.2535875</a>","ieee":"U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,” presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014, vol. 49, no. 1, pp. 595–606.","mla":"Boker, Udi, et al. <i>Battery Transition Systems</i>. Vol. 49, no. 1, ACM, 2014, pp. 595–606, doi:<a href=\"https://doi.org/10.1145/2535838.2535875\">10.1145/2535838.2535875</a>.","chicago":"Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition Systems,” 49:595–606. ACM, 2014. <a href=\"https://doi.org/10.1145/2535838.2535875\">https://doi.org/10.1145/2535838.2535875</a>."},"oa_version":"None","scopus_import":1,"title":"Battery transition systems","volume":49,"date_updated":"2021-01-12T06:56:13Z","conference":{"location":"San Diego, USA","start_date":"2014-01-22","name":"POPL: Principles of Programming Languages","end_date":"2014-01-24"},"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"date_published":"2014-01-13T00:00:00Z","year":"2014","publist_id":"4722","date_created":"2018-12-11T11:56:30Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","intvolume":"        49","ec_funded":1,"abstract":[{"text":"The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots.","lang":"eng"}],"doi":"10.1145/2535838.2535875","publication_status":"published","department":[{"_id":"ToHe"}]},{"oa_version":"Preprint","scopus_import":"1","isi":1,"title":"Compositional specifications for IOCO testing","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5411"},{"id":"1155","status":"public","relation":"dissertation_contains"}]},"citation":{"apa":"Daca, P., Henzinger, T. A., Krenn, W., &#38; Nickovic, D. (2014). Compositional specifications for IOCO testing. In <i>IEEE 7th International Conference on Software Testing, Verification and Validation</i>. Cleveland, USA: IEEE. <a href=\"https://doi.org/10.1109/ICST.2014.50\">https://doi.org/10.1109/ICST.2014.50</a>","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing. IEEE 7th International Conference on Software Testing, Verification and Validation. ICST: International Conference on Software Testing, Verification and Validation, 6823899.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International Conference on Software Testing, Verification and Validation, IEEE, 2014.","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, “Compositional specifications for IOCO testing,” in <i>IEEE 7th International Conference on Software Testing, Verification and Validation</i>, Cleveland, USA, 2014.","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional specifications for IOCO testing. In: <i>IEEE 7th International Conference on Software Testing, Verification and Validation</i>. IEEE; 2014. doi:<a href=\"https://doi.org/10.1109/ICST.2014.50\">10.1109/ICST.2014.50</a>","mla":"Daca, Przemyslaw, et al. “Compositional Specifications for IOCO Testing.” <i>IEEE 7th International Conference on Software Testing, Verification and Validation</i>, 6823899, IEEE, 2014, doi:<a href=\"https://doi.org/10.1109/ICST.2014.50\">10.1109/ICST.2014.50</a>.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. “Compositional Specifications for IOCO Testing.” In <i>IEEE 7th International Conference on Software Testing, Verification and Validation</i>. IEEE, 2014. <a href=\"https://doi.org/10.1109/ICST.2014.50\">https://doi.org/10.1109/ICST.2014.50</a>."},"arxiv":1,"month":"03","quality_controlled":"1","article_number":"6823899","publication_identifier":{"isbn":["978-1-4799-2255-0"],"issn":["2159-4848"]},"publisher":"IEEE","type":"conference","day":"01","status":"public","oa":1,"language":[{"iso":"eng"}],"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Krenn, Willibald","last_name":"Krenn","first_name":"Willibald"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"article_processing_charge":"No","_id":"2167","abstract":[{"text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing. In this paper, we study compositional properties of the ioco-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the ioco conformance relation, the resulting methodology can be applied to a broader class of systems.","lang":"eng"}],"ec_funded":1,"doi":"10.1109/ICST.2014.50","publication_status":"published","external_id":{"arxiv":["1904.07083"],"isi":["000355985000040"]},"department":[{"_id":"ToHe"}],"publication":"IEEE 7th International Conference on Software Testing, Verification and Validation","year":"2014","publist_id":"4817","main_file_link":[{"url":"https://arxiv.org/abs/1904.07083","open_access":"1"}],"date_created":"2018-12-11T11:56:06Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2026-04-15T10:02:12Z","conference":{"name":"ICST: International Conference on Software Testing, Verification and Validation","end_date":"2014-04-04","start_date":"2014-03-31","location":"Cleveland, USA"},"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"date_published":"2014-03-01T00:00:00Z"},{"article_processing_charge":"No","article_type":"original","_id":"2187","issue":"3-4","language":[{"iso":"eng"}],"oa":1,"author":[{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Karin","full_name":"Greimel, Karin","last_name":"Greimel"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Georg","full_name":"Hofferek, Georg","last_name":"Hofferek"},{"last_name":"Jobstmann","full_name":"Jobstmann, Barbara","first_name":"Barbara"},{"last_name":"Könighofer","full_name":"Könighofer, Bettina","first_name":"Bettina"},{"first_name":"Robert","last_name":"Könighofer","full_name":"Könighofer, Robert"}],"type":"journal_article","day":"01","status":"public","page":"193 - 220","quality_controlled":"1","month":"06","publisher":"Springer","citation":{"mla":"Bloem, Roderick, et al. “Synthesizing Robust Systems.” <i>Acta Informatica</i>, vol. 51, no. 3–4, Springer, 2014, pp. 193–220, doi:<a href=\"https://doi.org/10.1007/s00236-013-0191-5\">10.1007/s00236-013-0191-5</a>.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. “Synthesizing Robust Systems.” <i>Acta Informatica</i>. Springer, 2014. <a href=\"https://doi.org/10.1007/s00236-013-0191-5\">https://doi.org/10.1007/s00236-013-0191-5</a>.","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann, B., … Könighofer, R. (2014). Synthesizing robust systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-013-0191-5\">https://doi.org/10.1007/s00236-013-0191-5</a>","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer B, Könighofer R. 2014. Synthesizing robust systems. Acta Informatica. 51(3–4), 193–220.","ieee":"R. Bloem <i>et al.</i>, “Synthesizing robust systems,” <i>Acta Informatica</i>, vol. 51, no. 3–4. Springer, pp. 193–220, 2014.","ama":"Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. <i>Acta Informatica</i>. 2014;51(3-4):193-220. doi:<a href=\"https://doi.org/10.1007/s00236-013-0191-5\">10.1007/s00236-013-0191-5</a>","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, G. Hofferek, B. Jobstmann, B. Könighofer, R. Könighofer, Acta Informatica 51 (2014) 193–220."},"has_accepted_license":"1","pubrep_id":"71","title":"Synthesizing robust systems","scopus_import":"1","oa_version":"Submitted Version","isi":1,"ddc":["621"],"project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_published":"2014-06-01T00:00:00Z","volume":51,"date_updated":"2025-09-29T11:32:51Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2014","publist_id":"4787","date_created":"2018-12-11T11:56:13Z","file_date_updated":"2020-07-14T12:45:31Z","intvolume":"        51","file":[{"creator":"system","access_level":"open_access","date_updated":"2020-07-14T12:45:31Z","file_name":"IST-2012-71-v1+1_Synthesizing_robust_systems.pdf","file_size":169523,"file_id":"5234","checksum":"d7f560f3d923f0f00aa10a0652f83273","relation":"main_file","date_created":"2018-12-12T10:16:44Z","content_type":"application/pdf"}],"publication":"Acta Informatica","publication_status":"published","external_id":{"isi":["000335981500004"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"text":"Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results.","lang":"eng"}],"doi":"10.1007/s00236-013-0191-5"},{"alternative_title":["LNCS"],"doi":"10.1007/978-3-319-08867-9_13","abstract":[{"lang":"eng","text":"We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods."}],"ec_funded":1,"external_id":{"arxiv":["1402.3388"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication_status":"published","intvolume":"      8559","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1402.3388"}],"date_created":"2018-12-11T11:56:14Z","year":"2014","publist_id":"4784","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CAV: Computer Aided Verification"},"volume":8559,"date_updated":"2025-06-11T08:01:04Z","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms"}],"date_published":"2014-01-01T00:00:00Z","oa_version":"Submitted Version","acknowledgement":"The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061.","scopus_import":"1","title":"From LTL to deterministic automata: A safraless compositional approach","citation":{"mla":"Esparza, Javier, and Jan Kretinsky. <i>From LTL to Deterministic Automata: A Safraless Compositional Approach</i>. Vol. 8559, Springer, 2014, pp. 192–208, doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_13\">10.1007/978-3-319-08867-9_13</a>.","chicago":"Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_13\">https://doi.org/10.1007/978-3-319-08867-9_13</a>.","ista":"Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.","apa":"Esparza, J., &#38; Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_13\">https://doi.org/10.1007/978-3-319-08867-9_13</a>","short":"J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.","ama":"Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_13\">10.1007/978-3-319-08867-9_13</a>","ieee":"J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208."},"arxiv":1,"publisher":"Springer","month":"01","quality_controlled":"1","page":"192 - 208","status":"public","type":"conference","day":"01","author":[{"last_name":"Esparza","full_name":"Esparza, Javier","first_name":"Javier"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan"}],"oa":1,"language":[{"iso":"eng"}],"corr_author":"1","_id":"2190","article_processing_charge":"No"}]