[{"year":"2012","acknowledgement":"This research was supported in part by the European Research Council (ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF) project S11402-N23.","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","related_material":{"record":[{"id":"1405","status":"public","relation":"dissertation_contains"}]},"author":[{"last_name":"Zufferey","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien"},{"full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"volume":7148,"date_updated":"2023-09-07T11:36:36Z","date_created":"2018-12-11T12:02:16Z","ec_funded":1,"publist_id":"3406","file_date_updated":"2020-07-14T12:46:05Z","oa":1,"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"quality_controlled":"1","doi":"10.1007/978-3-642-27940-9_29","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2012-01-22","location":"Philadelphia, PA, USA","end_date":"2012-01-24"},"language":[{"iso":"eng"}],"month":"01","_id":"3251","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","intvolume":" 7148","status":"public","title":"Ideal abstractions for well structured transition systems","ddc":["000","005"],"pubrep_id":"100","file":[{"file_size":217104,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","date_updated":"2020-07-14T12:46:05Z","date_created":"2018-12-12T10:09:35Z","relation":"main_file","file_id":"4759"}],"oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system."}],"citation":{"ama":"Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition systems. In: Vol 7148. Springer; 2012:445-460. doi:10.1007/978-3-642-27940-9_29","apa":"Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29","ieee":"D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured transition systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460.","ista":"Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.","short":"D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.","mla":"Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.","chicago":"Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_29."},"page":"445 - 460","date_published":"2012-01-01T00:00:00Z","has_accepted_license":"1","day":"01"},{"date_created":"2018-12-11T12:02:20Z","date_updated":"2021-01-12T07:42:15Z","volume":7078,"oa_version":"None","author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"title":"Solving recursion-free Horn clauses over LI+UIF","status":"public","publication_status":"published","publisher":"Springer","intvolume":" 7078","editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"department":[{"_id":"ToHe"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3264","year":"2011","abstract":[{"lang":"eng","text":"Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms."}],"publist_id":"3383","ec_funded":1,"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"conference":{"start_date":"2011-12-05","location":"Kenting, Taiwan","end_date":"2011-12-07","name":"APLAS: Asian Symposium on Programming Languages and Systems"},"date_published":"2011-12-05T00:00:00Z","doi":"10.1007/978-3-642-25318-8_16","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"page":"188 - 203","citation":{"ama":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:10.1007/978-3-642-25318-8_16","ista":"Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS, vol. 7078, 188–203.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2011). Solving recursion-free Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan: Springer. https://doi.org/10.1007/978-3-642-25318-8_16","mla":"Gupta, Ashutosh, et al. Solving Recursion-Free Horn Clauses over LI+UIF. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:10.1007/978-3-642-25318-8_16.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011. https://doi.org/10.1007/978-3-642-25318-8_16."},"day":"05","month":"12"},{"month":"06","day":"14","has_accepted_license":"1","oa":1,"citation":{"mla":"Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6.","short":"T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.","chicago":"Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011.","ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.","ista":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.","apa":"Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.","ieee":"T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, 2011, pp. 1–6."},"quality_controlled":"1","page":"1 - 6","conference":{"name":"HotCloud: Workshop on Hot Topics in Cloud Computing","start_date":"2011-06-14","end_date":"2011-06-15"},"date_published":"2011-06-14T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","abstract":[{"text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:06Z","publist_id":"3338","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3302","year":"2011","ddc":["000","005"],"publication_status":"published","title":"Static scheduling in clouds","status":"public","publisher":"USENIX","department":[{"_id":"ToHe"}],"author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Singh, Anmol","first_name":"Anmol","last_name":"Singh","id":"72A86902-E99F-11E9-9F62-915534D1B916"},{"last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"},{"id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736","first_name":"Damien","last_name":"Zufferey","full_name":"Zufferey, Damien"}],"pubrep_id":"90","date_created":"2018-12-11T12:02:33Z","date_updated":"2021-01-12T07:42:31Z","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","file_size":232770,"content_type":"application/pdf","creator":"system","relation":"main_file","file_id":"5333","checksum":"21a461ac004bb535c83320fe79b30375","date_updated":"2020-07-14T12:46:06Z","date_created":"2018-12-12T10:18:14Z"}]},{"oa_version":"Submitted Version","file":[{"creator":"system","content_type":"application/pdf","file_size":240820,"file_name":"IST-2012-91-v1+1_Tail_approximation_for_the_chemical_master_equation.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:06Z","date_created":"2018-12-12T10:18:12Z","checksum":"aa4d7a832a5419e6c0090650ebff2b9a","file_id":"5331","relation":"main_file"}],"date_created":"2018-12-11T12:02:33Z","date_updated":"2021-01-12T07:42:30Z","pubrep_id":"91","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Mateescu","first_name":"Maria","full_name":"Mateescu, Maria"}],"publisher":"Tampere International Center for Signal Processing","department":[{"_id":"ToHe"}],"ddc":["005","570"],"status":"public","title":"Tail approximation for the chemical master equation","publication_status":"published","_id":"3301","year":"2011","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"3339","file_date_updated":"2020-07-14T12:46:06Z","abstract":[{"lang":"eng","text":"The chemical master equation is a differential equation describing the time evolution of the probability distribution over the possible “states” of a biochemical system. The solution of this equation is of interest within the systems biology field ever since the importance of the molec- ular noise has been acknowledged. Unfortunately, most of the systems do not have analytical solutions, and numerical solutions suffer from the course of dimensionality and therefore need to be approximated. Here, we introduce the concept of tail approximation, which retrieves an approximation of the probabilities in the tail of a distribution from the total probability of the tail and its conditional expectation. This approximation method can then be used to numerically compute the solution of the chemical master equation on a subset of the state space, thus fighting the explosion of the state space, for which this problem is renowned."}],"type":"conference","language":[{"iso":"eng"}],"date_published":"2011-01-01T00:00:00Z","conference":{"name":"WCSB: Workshop on Computational Systems Biology (TICSP)"},"quality_controlled":"1","oa":1,"citation":{"mla":"Henzinger, Thomas A., and Maria Mateescu. Tail Approximation for the Chemical Master Equation. Tampere International Center for Signal Processing, 2011.","short":"T.A. Henzinger, M. Mateescu, in:, Tampere International Center for Signal Processing, 2011.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Tail Approximation for the Chemical Master Equation.” Tampere International Center for Signal Processing, 2011.","ama":"Henzinger TA, Mateescu M. Tail approximation for the chemical master equation. In: Tampere International Center for Signal Processing; 2011.","ista":"Henzinger TA, Mateescu M. 2011. Tail approximation for the chemical master equation. WCSB: Workshop on Computational Systems Biology (TICSP).","ieee":"T. A. Henzinger and M. Mateescu, “Tail approximation for the chemical master equation,” presented at the WCSB: Workshop on Computational Systems Biology (TICSP), 2011.","apa":"Henzinger, T. A., & Mateescu, M. (2011). Tail approximation for the chemical master equation. Presented at the WCSB: Workshop on Computational Systems Biology (TICSP), Tampere International Center for Signal Processing."},"has_accepted_license":"1","month":"01","day":"01"},{"month":"09","quality_controlled":"1","oa":1,"language":[{"iso":"eng"}],"doi":"10.1145/2037509.2037510","conference":{"location":"Paris, France","start_date":"2011-09-21","end_date":"2011-09-23","name":"CMSB: Computational Methods in Systems Biology"},"publist_id":"3341","file_date_updated":"2020-07-14T12:46:06Z","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2011","date_created":"2018-12-11T12:02:32Z","date_updated":"2021-01-12T07:42:29Z","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Mateescu, Maria","first_name":"Maria","last_name":"Mateescu"}],"scopus_import":1,"has_accepted_license":"1","day":"21","page":"1 - 3","citation":{"mla":"Henzinger, Thomas A., and Maria Mateescu. Propagation Models for Computing Biochemical Reaction Networks. Springer, 2011, pp. 1–3, doi:10.1145/2037509.2037510.","short":"T.A. Henzinger, M. Mateescu, in:, Springer, 2011, pp. 1–3.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Propagation Models for Computing Biochemical Reaction Networks,” 1–3. Springer, 2011. https://doi.org/10.1145/2037509.2037510.","ama":"Henzinger TA, Mateescu M. Propagation models for computing biochemical reaction networks. In: Springer; 2011:1-3. doi:10.1145/2037509.2037510","ista":"Henzinger TA, Mateescu M. 2011. Propagation models for computing biochemical reaction networks. CMSB: Computational Methods in Systems Biology, 1–3.","apa":"Henzinger, T. A., & Mateescu, M. (2011). Propagation models for computing biochemical reaction networks (pp. 1–3). Presented at the CMSB: Computational Methods in Systems Biology, Paris, France: Springer. https://doi.org/10.1145/2037509.2037510","ieee":"T. A. Henzinger and M. Mateescu, “Propagation models for computing biochemical reaction networks,” presented at the CMSB: Computational Methods in Systems Biology, Paris, France, 2011, pp. 1–3."},"date_published":"2011-09-21T00:00:00Z","type":"conference","abstract":[{"text":"We introduce propagation models, a formalism designed to support general and efficient data structures for the transient analysis of biochemical reaction networks. We give two use cases for propagation abstract data types: the uniformization method and numerical integration. We also sketch an implementation of a propagation abstract data type, which uses abstraction to approximate states.","lang":"eng"}],"ddc":["000","004"],"title":"Propagation models for computing biochemical reaction networks","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3299","oa_version":"Submitted Version","file":[{"checksum":"7f5c65509db1a9fb049abedd9663ed06","date_updated":"2020-07-14T12:46:06Z","date_created":"2018-12-12T10:07:50Z","relation":"main_file","file_id":"4649","file_size":255780,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2012-92-v1+1_Propagation_models_for_computing_biochemical_reaction_networks.pdf"}],"pubrep_id":"92"},{"article_processing_charge":"No","day":"14","scopus_import":1,"date_published":"2011-07-14T00:00:00Z","citation":{"ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: 6th IEEE International Symposium on Industrial and Embedded Systems. IEEE; 2011:176-185. doi:10.1109/SIES.2011.5953660","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in 6th IEEE International Symposium on Industrial and Embedded Systems, Vasteras, Sweden, 2011, pp. 176–185.","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann, B. (2011). Specification-centered robustness. In 6th IEEE International Symposium on Industrial and Embedded Systems (pp. 176–185). Vasteras, Sweden: IEEE. https://doi.org/10.1109/SIES.2011.5953660","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems. SIES: International Symposium on Industrial Embedded Systems, 176–185.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185.","mla":"Bloem, Roderick, et al. “Specification-Centered Robustness.” 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–85, doi:10.1109/SIES.2011.5953660.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In 6th IEEE International Symposium on Industrial and Embedded Systems, 176–85. IEEE, 2011. https://doi.org/10.1109/SIES.2011.5953660."},"publication":"6th IEEE International Symposium on Industrial and Embedded Systems","page":"176 - 185","abstract":[{"lang":"eng","text":"In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates."}],"type":"conference","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3316","title":"Specification-centered robustness","status":"public","month":"07","doi":"10.1109/SIES.2011.5953660","conference":{"end_date":"2011-06-17","start_date":"2011-06-15","location":"Vasteras, Sweden","name":" SIES: International Symposium on Industrial Embedded Systems"},"language":[{"iso":"eng"}],"oa":1,"main_file_link":[{"open_access":"1","url":"https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse"}],"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","publist_id":"3323","ec_funded":1,"author":[{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Greimel, Karin","first_name":"Karin","last_name":"Greimel"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"}],"date_created":"2018-12-11T12:02:38Z","date_updated":"2021-01-12T07:42:36Z","year":"2011","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","publication_status":"published"},{"publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","citation":{"chicago":"Tripakis, Stavros, Ben Lickly, Thomas A Henzinger, and Edward Lee. “A Theory of Synchronous Relational Interfaces.” ACM Transactions on Programming Languages and Systems (TOPLAS). ACM, 2011. https://doi.org/10.1145/1985342.1985345.","mla":"Tripakis, Stavros, et al. “A Theory of Synchronous Relational Interfaces.” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 33, no. 4, 14, ACM, 2011, doi:10.1145/1985342.1985345.","short":"S. Tripakis, B. Lickly, T.A. Henzinger, E. Lee, ACM Transactions on Programming Languages and Systems (TOPLAS) 33 (2011).","ista":"Tripakis S, Lickly B, Henzinger TA, Lee E. 2011. A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). 33(4), 14.","ieee":"S. Tripakis, B. Lickly, T. A. Henzinger, and E. Lee, “A theory of synchronous relational interfaces,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 33, no. 4. ACM, 2011.","apa":"Tripakis, S., Lickly, B., Henzinger, T. A., & Lee, E. (2011). A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). ACM. https://doi.org/10.1145/1985342.1985345","ama":"Tripakis S, Lickly B, Henzinger TA, Lee E. A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). 2011;33(4). doi:10.1145/1985342.1985345"},"date_published":"2011-07-01T00:00:00Z","scopus_import":1,"day":"01","has_accepted_license":"1","ddc":["000","005"],"status":"public","title":"A theory of synchronous relational interfaces","intvolume":" 33","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3353","file":[{"date_created":"2018-12-12T10:16:45Z","date_updated":"2020-07-14T12:46:09Z","checksum":"5d44a8aa81e33210649beae507602138","file_id":"5235","relation":"main_file","creator":"system","content_type":"application/pdf","file_size":775662,"file_name":"IST-2012-85-v1+1_A_theory_of_synchronous_relational_interfaces.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","pubrep_id":"85","type":"journal_article","abstract":[{"text":"Compositional theories are crucial when designing large and complex systems from smaller components. In this work we propose such a theory for synchronous concurrent systems. Our approach follows so-called interface theories, which use game-theoretic interpretations of composition and refinement. These are appropriate for systems with distinct inputs and outputs, and explicit conditions on inputs that must be enforced during composition. Our interfaces model systems that execute in an infinite sequence of synchronous rounds. At each round, a contract must be satisfied. The contract is simply a relation specifying the set of valid input/output pairs. Interfaces can be composed by parallel, serial or feedback composition. A refinement relation between interfaces is defined, and shown to have two main properties: (1) it is preserved by composition, and (2) it is equivalent to substitutability, namely, the ability to replace an interface by another one in any context. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.","lang":"eng"}],"issue":"4","quality_controlled":"1","project":[{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543"},{"name":"Design for Embedded Systems","call_identifier":"FP7","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"oa":1,"language":[{"iso":"eng"}],"doi":"10.1145/1985342.1985345","month":"07","publication_status":"published","publisher":"ACM","department":[{"_id":"ToHe"}],"year":"2011","date_created":"2018-12-11T12:02:51Z","date_updated":"2021-01-12T07:42:52Z","volume":33,"author":[{"first_name":"Stavros","last_name":"Tripakis","full_name":"Tripakis, Stavros"},{"full_name":"Lickly, Ben","last_name":"Lickly","first_name":"Ben"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Edward","last_name":"Lee","full_name":"Lee, Edward"}],"article_number":"14","file_date_updated":"2020-07-14T12:46:09Z","publist_id":"3263","ec_funded":1},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3355","ddc":["000","004"],"status":"public","title":"Quantitative evaluation of BFT protocols","pubrep_id":"84","file":[{"date_updated":"2020-07-14T12:46:09Z","date_created":"2018-12-12T10:07:49Z","checksum":"4dc8750ab7921f51de992000b13d1b01","relation":"main_file","file_id":"4648","content_type":"application/pdf","file_size":272017,"creator":"system","file_name":"IST-2012-84-v1+1_Quantitative_evaluation_of_BFT_protocols.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","type":"conference","abstract":[{"lang":"eng","text":"Byzantine Fault Tolerant (BFT) protocols aim to improve the reliability of distributed systems. They enable systems to tolerate arbitrary failures in a bounded number of nodes. BFT protocols are usually proven correct for certain safety and liveness properties. However, recent studies have shown that the performance of state-of-the-art BFT protocols decreases drastically in the presence of even a single malicious node. This motivates a formal quantitative analysis of BFT protocols to investigate their performance characteristics under different scenarios. We present HyPerf, a new hybrid methodology based on model checking and simulation techniques for evaluating the performance of BFT protocols. We build a transition system corresponding to a BFT protocol and systematically explore the set of behaviors allowed by the protocol. We associate certain timing information with different operations in the protocol, like cryptographic operations and message transmission. After an elaborate state exploration, we use the time information to evaluate the performance characteristics of the protocol using simulation techniques. We integrate our framework in Mace, a tool for building and verifying distributed systems. We evaluate the performance of PBFT using our framework. We describe two different use-cases of our methodology. For the benign operation of the protocol, we use the time information as random variables to compute the probability distribution of the execution times. In the presence of faults, we estimate the worst-case performance of the protocol for various attacks that can be employed by malicious nodes. Our results show the importance of hybrid techniques in systematically analyzing the performance of large-scale systems."}],"citation":{"apa":"Halalai, R., Henzinger, T. A., & Singh, V. (2011). Quantitative evaluation of BFT protocols (pp. 255–264). Presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany: IEEE. https://doi.org/10.1109/QEST.2011.40","ieee":"R. Halalai, T. A. Henzinger, and V. Singh, “Quantitative evaluation of BFT protocols,” presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany, 2011, pp. 255–264.","ista":"Halalai R, Henzinger TA, Singh V. 2011. Quantitative evaluation of BFT protocols. QEST: Quantitative Evaluation of Systems, 255–264.","ama":"Halalai R, Henzinger TA, Singh V. Quantitative evaluation of BFT protocols. In: IEEE; 2011:255-264. doi:10.1109/QEST.2011.40","chicago":"Halalai, Raluca, Thomas A Henzinger, and Vasu Singh. “Quantitative Evaluation of BFT Protocols,” 255–64. IEEE, 2011. https://doi.org/10.1109/QEST.2011.40.","short":"R. Halalai, T.A. Henzinger, V. Singh, in:, IEEE, 2011, pp. 255–264.","mla":"Halalai, Raluca, et al. Quantitative Evaluation of BFT Protocols. IEEE, 2011, pp. 255–64, doi:10.1109/QEST.2011.40."},"page":"255 - 264","date_published":"2011-10-13T00:00:00Z","scopus_import":1,"day":"13","has_accepted_license":"1","year":"2011","publication_status":"published","publisher":"IEEE","department":[{"_id":"ToHe"}],"author":[{"full_name":"Halalai, Raluca","last_name":"Halalai","first_name":"Raluca","id":"584C6850-E996-11E9-805B-F01764644770"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh"}],"date_updated":"2021-01-12T07:42:53Z","date_created":"2018-12-11T12:02:51Z","file_date_updated":"2020-07-14T12:46:09Z","publist_id":"3260","oa":1,"quality_controlled":"1","conference":{"location":"Aachen, Germany","start_date":"2011-09-05","end_date":"2011-09-08","name":"QEST: Quantitative Evaluation of Systems"},"doi":"10.1109/QEST.2011.40","language":[{"iso":"eng"}],"month":"10"},{"year":"2011","_id":"3354","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Qualitative concurrent parity games","publication_status":"published","intvolume":" 12","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"ACM","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"related_material":{"record":[{"id":"2054","relation":"later_version","status":"public"}]},"date_created":"2018-12-11T12:02:51Z","date_updated":"2023-02-23T10:26:18Z","oa_version":"None","volume":12,"article_number":"28","type":"journal_article","abstract":[{"text":"We consider two-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We consider ω-regular winning conditions specified as parity objectives. Both players are allowed to use randomization when choosing their moves. We study the computation of the limit-winning set of states, consisting of the states where the sup-inf value of the game for player 1 is 1: in other words, a state is limit-winning if player 1 can ensure a probability of winning arbitrarily close to 1. We show that the limit-winning set can be computed in O(n2d+2) time, where n is the size of the game structure and 2d is the number of priorities (or colors). The membership problem of whether a state belongs to the limit-winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games. This is because concurrent games do not satisfy two of the most fundamental properties of turn-based parity games. First, in concurrent games limit-winning strategies require randomization; and second, they require infinite memory.","lang":"eng"}],"issue":"4","publist_id":"3262","publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"apa":"Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2011). Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/1970398.1970404","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Qualitative concurrent parity games,” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4. ACM, 2011.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2011. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 12(4), 28.","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 2011;12(4). doi:10.1145/1970398.1970404","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL). ACM, 2011. https://doi.org/10.1145/1970398.1970404.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational Logic (TOCL) 12 (2011).","mla":"Chatterjee, Krishnendu, et al. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4, 28, ACM, 2011, doi:10.1145/1970398.1970404."},"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1145/1970398.1970404","date_published":"2011-07-04T00:00:00Z","language":[{"iso":"eng"}],"scopus_import":1,"day":"04","month":"07"},{"issue":"10","publist_id":"3267","ec_funded":1,"abstract":[{"lang":"eng","text":"Exploring the connection of biology with reactive systems to better understand living systems."}],"type":"journal_article","volume":54,"oa_version":"None","date_created":"2018-12-11T12:02:50Z","date_updated":"2021-01-12T07:42:52Z","author":[{"last_name":"Fisher","first_name":"Jasmin","full_name":"Fisher, Jasmin"},{"first_name":"David","last_name":"Harel","full_name":"Harel, David"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"publisher":"ACM","department":[{"_id":"ToHe"}],"intvolume":" 54","title":"Biology as reactivity","publication_status":"published","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3352","year":"2011","day":"01","month":"10","language":[{"iso":"eng"}],"doi":"10.1145/2001269.2001289","date_published":"2011-10-01T00:00:00Z","page":"72 - 82","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"quality_controlled":"1","citation":{"mla":"Fisher, Jasmin, et al. “Biology as Reactivity.” Communications of the ACM, vol. 54, no. 10, ACM, 2011, pp. 72–82, doi:10.1145/2001269.2001289.","short":"J. Fisher, D. Harel, T.A. Henzinger, Communications of the ACM 54 (2011) 72–82.","chicago":"Fisher, Jasmin, David Harel, and Thomas A Henzinger. “Biology as Reactivity.” Communications of the ACM. ACM, 2011. https://doi.org/10.1145/2001269.2001289.","ama":"Fisher J, Harel D, Henzinger TA. Biology as reactivity. Communications of the ACM. 2011;54(10):72-82. doi:10.1145/2001269.2001289","ista":"Fisher J, Harel D, Henzinger TA. 2011. Biology as reactivity. Communications of the ACM. 54(10), 72–82.","ieee":"J. Fisher, D. Harel, and T. A. Henzinger, “Biology as reactivity,” Communications of the ACM, vol. 54, no. 10. ACM, pp. 72–82, 2011.","apa":"Fisher, J., Harel, D., & Henzinger, T. A. (2011). Biology as reactivity. Communications of the ACM. ACM. https://doi.org/10.1145/2001269.2001289"},"publication":"Communications of the ACM"}]