[{"_id":"3362","day":"01","intvolume":"      6901","publication_status":"published","ddc":["000"],"has_accepted_license":"1","scopus_import":1,"date_created":"2018-12-11T12:02:54Z","conference":{"end_date":"2011-09-09","name":"CONCUR: Concurrency Theory","start_date":"2011-09-06","location":"Aachen, Germany"},"type":"conference","alternative_title":["LNCS"],"status":"public","oa_version":"Submitted Version","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:10Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"7870","date_updated":"2020-07-14T12:46:10Z","file_size":337125,"checksum":"6bf2453d8e52e979ddb58d17325bad26","date_created":"2020-05-19T16:17:48Z","file_name":"2011_CONCUR_Fisher.pdf","creator":"dernst","access_level":"open_access"}],"doi":"10.1007/978-3-642-23217-6_27","citation":{"ama":"Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. Dynamic reactive modules. In: Vol 6901. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2011:404-418. doi:<a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">10.1007/978-3-642-23217-6_27</a>","ista":"Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. 2011. Dynamic reactive modules. CONCUR: Concurrency Theory, LNCS, vol. 6901, 404–418.","apa":"Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., &#38; Vardi, M. (2011). Dynamic reactive modules (Vol. 6901, pp. 404–418). Presented at the CONCUR: Concurrency Theory, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">https://doi.org/10.1007/978-3-642-23217-6_27</a>","short":"J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, A. Singh, M. Vardi, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–418.","mla":"Fisher, Jasmin, et al. <i>Dynamic Reactive Modules</i>. Vol. 6901, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">10.1007/978-3-642-23217-6_27</a>.","chicago":"Fisher, Jasmin, Thomas A Henzinger, Dejan Nickovic, Nir Piterman, Anmol Singh, and Moshe Vardi. “Dynamic Reactive Modules,” 6901:404–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. <a href=\"https://doi.org/10.1007/978-3-642-23217-6_27\">https://doi.org/10.1007/978-3-642-23217-6_27</a>.","ieee":"J. Fisher, T. A. Henzinger, D. Nickovic, N. Piterman, A. Singh, and M. Vardi, “Dynamic reactive modules,” presented at the CONCUR: Concurrency Theory, Aachen, Germany, 2011, vol. 6901, pp. 404–418."},"volume":6901,"article_processing_charge":"No","department":[{"_id":"ToHe"}],"author":[{"first_name":"Jasmin","last_name":"Fisher","full_name":"Fisher, Jasmin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"last_name":"Piterman","first_name":"Nir","full_name":"Piterman, Nir"},{"full_name":"Singh, Anmol","last_name":"Singh","first_name":"Anmol"},{"last_name":"Vardi","first_name":"Moshe","full_name":"Vardi, Moshe"}],"date_published":"2011-01-01T00:00:00Z","publist_id":"3253","title":"Dynamic reactive modules","date_updated":"2021-01-12T07:42:57Z","ec_funded":1,"language":[{"iso":"eng"}],"page":"404 - 418","year":"2011","month":"01","oa":1,"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"lang":"eng","text":"State-transition systems communicating by shared variables have been the underlying model of choice for applications of model checking. Such formalisms, however, have difficulty with modeling process creation or death and communication reconfigurability. Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling formalism that supports dynamic reconfiguration and creation/death of processes. The resulting formalism supports two types of variables, data variables and reference variables. Reference variables enable changing the connectivity between processes and referring to instances of processes. We show how this new formalism supports parallel composition and refinement through trace containment. DRM provide a natural language for modeling (and ultimately reasoning about) biological systems and multiple threads communicating through shared variables."}]},{"type":"preprint","status":"public","oa_version":"Preprint","corr_author":"1","arxiv":1,"date_created":"2018-12-11T12:02:54Z","_id":"3363","day":"01","publication_status":"submitted","article_number":"1104.0127","citation":{"ama":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. doi:<a href=\"https://doi.org/10.48550/arXiv.1104.0127\">10.48550/arXiv.1104.0127</a>","short":"K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.).","ista":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. 1104.0127.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Tracol, M. (n.d.). The decidability frontier for probabilistic automata on infinite words. ArXiv. <a href=\"https://doi.org/10.48550/arXiv.1104.0127\">https://doi.org/10.48550/arXiv.1104.0127</a>","mla":"Chatterjee, Krishnendu, et al. <i>The Decidability Frontier for Probabilistic Automata on Infinite Words</i>. 1104.0127, ArXiv, doi:<a href=\"https://doi.org/10.48550/arXiv.1104.0127\">10.48550/arXiv.1104.0127</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d. <a href=\"https://doi.org/10.48550/arXiv.1104.0127\">https://doi.org/10.48550/arXiv.1104.0127</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier for probabilistic automata on infinite words.” ArXiv."},"doi":"10.48550/arXiv.1104.0127","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Tracol, Mathieu","last_name":"Tracol","first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"main_file_link":[{"url":"https://arxiv.org/abs/1104.0127","open_access":"1"}],"date_published":"2011-04-01T00:00:00Z","publist_id":"3251","title":"The decidability frontier for probabilistic automata on infinite words","date_updated":"2025-06-26T09:19:59Z","external_id":{"arxiv":["1104.0127"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"ArXiv","abstract":[{"text":"We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs for probabilistic finite automata and present a complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words.","lang":"eng"}],"project":[{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa":1,"language":[{"iso":"eng"}],"month":"04","page":"19","year":"2011"},{"external_id":{"isi":["000290078000005"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"author":[{"full_name":"Didier, Frédéric","last_name":"Didier","first_name":"Frédéric"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Maria","last_name":"Mateescu","full_name":"Mateescu, Maria"},{"full_name":"Wolf, Verena","first_name":"Verena","last_name":"Wolf"}],"publist_id":"3249","date_published":"2011-05-06T00:00:00Z","title":"Approximation of event probabilities in noisy cellular processes","date_updated":"2025-09-30T09:03:30Z","issue":"21","publisher":"Elsevier","pubrep_id":"79","abstract":[{"text":"Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.","lang":"eng"}],"language":[{"iso":"eng"}],"isi":1,"year":"2011","month":"05","page":"2128 - 2141","oa":1,"related_material":{"record":[{"status":"public","id":"4535","relation":"earlier_version"}]},"date_created":"2018-12-11T12:02:55Z","type":"journal_article","oa_version":"Submitted Version","publication":"Theoretical Computer Science","status":"public","_id":"3364","intvolume":"       412","day":"06","publication_status":"published","ddc":["000","004"],"has_accepted_license":"1","scopus_import":"1","doi":"10.1016/j.tcs.2010.10.022","citation":{"chicago":"Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf. “Approximation of Event Probabilities in Noisy Cellular Processes.” <i>Theoretical Computer Science</i>. Elsevier, 2011. <a href=\"https://doi.org/10.1016/j.tcs.2010.10.022\">https://doi.org/10.1016/j.tcs.2010.10.022</a>.","ieee":"F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event probabilities in noisy cellular processes,” <i>Theoretical Computer Science</i>, vol. 412, no. 21. Elsevier, pp. 2128–2141, 2011.","mla":"Didier, Frédéric, et al. “Approximation of Event Probabilities in Noisy Cellular Processes.” <i>Theoretical Computer Science</i>, vol. 412, no. 21, Elsevier, 2011, pp. 2128–41, doi:<a href=\"https://doi.org/10.1016/j.tcs.2010.10.022\">10.1016/j.tcs.2010.10.022</a>.","ama":"Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities in noisy cellular processes. <i>Theoretical Computer Science</i>. 2011;412(21):2128-2141. doi:<a href=\"https://doi.org/10.1016/j.tcs.2010.10.022\">10.1016/j.tcs.2010.10.022</a>","apa":"Didier, F., Henzinger, T. A., Mateescu, M., &#38; Wolf, V. (2011). Approximation of event probabilities in noisy cellular processes. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2010.10.022\">https://doi.org/10.1016/j.tcs.2010.10.022</a>","short":"F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, Theoretical Computer Science 412 (2011) 2128–2141.","ista":"Didier F, Henzinger TA, Mateescu M, Wolf V. 2011. Approximation of event probabilities in noisy cellular processes. Theoretical Computer Science. 412(21), 2128–2141."},"volume":412,"quality_controlled":"1","file_date_updated":"2020-07-14T12:46:10Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"access_level":"open_access","date_created":"2018-12-12T10:11:09Z","file_name":"IST-2012-79-v1+1_Approximation_of_event_probabilities_in_noisy_cellular_processes.pdf","creator":"system","date_updated":"2020-07-14T12:46:10Z","file_size":230503,"checksum":"e5503e25ce020d753e06b3431e16841e","relation":"main_file","content_type":"application/pdf","file_id":"4862"}]},{"alternative_title":["LNCS"],"type":"conference","conference":{"end_date":"2011-04-03","location":"Saarbrucken, Germany","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2011-03-26"},"status":"public","oa_version":"Submitted Version","date_created":"2018-12-11T12:02:55Z","has_accepted_license":"1","ddc":["000","005"],"scopus_import":1,"_id":"3365","publication_status":"published","day":"29","intvolume":"      6605","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>QUASY: Quantitative Synthesis Tool</i>. Vol. 6605, Springer, 2011, pp. 267–71, doi:<a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">10.1007/978-3-642-19835-9_24</a>.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis tool. In: Vol 6605. Springer; 2011:267-271. doi:<a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">10.1007/978-3-642-19835-9_24</a>","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011, pp. 267–271.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2011). QUASY: quantitative synthesis tool (Vol. 6605, pp. 267–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">https://doi.org/10.1007/978-3-642-19835-9_24</a>","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2011. QUASY: quantitative synthesis tool. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 6605, 267–271.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-19835-9_24\">https://doi.org/10.1007/978-3-642-19835-9_24</a>.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “QUASY: quantitative synthesis tool,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany, 2011, vol. 6605, pp. 267–271."},"volume":6605,"doi":"10.1007/978-3-642-19835-9_24","file":[{"access_level":"open_access","date_created":"2018-12-12T10:13:37Z","creator":"system","file_name":"IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf","file_size":475661,"date_updated":"2020-07-14T12:46:10Z","checksum":"762e52eb296f6dbfbf2a75d98b8ebaee","content_type":"application/pdf","relation":"main_file","file_id":"5022"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:10Z","publist_id":"3248","date_published":"2011-09-29T00:00:00Z","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"},{"full_name":"Singh, Rohit","last_name":"Singh","first_name":"Rohit"}],"title":"QUASY: quantitative synthesis tool","date_updated":"2021-01-12T07:42:58Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pubrep_id":"77","publisher":"Springer","abstract":[{"lang":"eng","text":"We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. The user can choose between a system that satisfies and optimizes the specifications (a) under all possible environment behaviors or (b) under the most-likely environment behaviors given as a probability distribution on the possible input sequences. Quasy solves these two quantitative synthesis problems by reduction to instances of 2-player games and Markov Decision Processes (MDPs) with quantitative winning objectives. Quasy can also be seen as a game solver for quantitative games. Most notable, it can solve lexicographic mean-payoff games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with mean-payoff parity objectives."}],"oa":1,"language":[{"iso":"eng"}],"page":"267 - 271","month":"09","year":"2011"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373"}],"pubrep_id":"76","publisher":"Springer","abstract":[{"text":"We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized &quot;specification free&quot;, in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures. ","lang":"eng"}],"language":[{"iso":"eng"}],"page":"243 - 259","month":"04","year":"2011","oa":1,"ec_funded":1,"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publist_id":"3247","date_published":"2011-04-21T00:00:00Z","author":[{"full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Singh, Rohit","last_name":"Singh","first_name":"Rohit"}],"date_updated":"2024-10-21T06:03:04Z","title":"Quantitative synthesis for concurrent programs","doi":"10.1007/978-3-642-22110-1_20","volume":6806,"citation":{"ieee":"P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh, “Quantitative synthesis for concurrent programs,” presented at the CAV: Computer Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 243–259.","chicago":"Cerny, Pavol, Krishnendu Chatterjee, Thomas A Henzinger, Arjun Radhakrishna, and Rohit Singh. “Quantitative Synthesis for Concurrent Programs.” edited by Ganesh Gopalakrishnan and Shaz Qadeer, 6806:243–59. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">https://doi.org/10.1007/978-3-642-22110-1_20</a>.","apa":"Cerny, P., Chatterjee, K., Henzinger, T. A., Radhakrishna, A., &#38; Singh, R. (2011). Quantitative synthesis for concurrent programs. In G. Gopalakrishnan &#38; S. Qadeer (Eds.) (Vol. 6806, pp. 243–259). Presented at the CAV: Computer Aided Verification, Snowbird, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">https://doi.org/10.1007/978-3-642-22110-1_20</a>","short":"P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259.","ista":"Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. 2011. Quantitative synthesis for concurrent programs. CAV: Computer Aided Verification, LNCS, vol. 6806, 243–259.","ama":"Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. Quantitative synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806. Springer; 2011:243-259. doi:<a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">10.1007/978-3-642-22110-1_20</a>","mla":"Cerny, Pavol, et al. <i>Quantitative Synthesis for Concurrent Programs</i>. Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp. 243–59, doi:<a href=\"https://doi.org/10.1007/978-3-642-22110-1_20\">10.1007/978-3-642-22110-1_20</a>."},"quality_controlled":"1","file_date_updated":"2020-07-14T12:46:10Z","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"5174","file_size":508946,"date_updated":"2020-07-14T12:46:10Z","checksum":"c033689355f45742dc7c99b5af13ce7a","date_created":"2018-12-12T10:15:51Z","creator":"system","file_name":"IST-2012-76-v1+1_Quantitative_synthesis_for_concurrent_programs.pdf","access_level":"open_access"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","corr_author":"1","related_material":{"record":[{"relation":"earlier_version","id":"5388","status":"public"}]},"date_created":"2018-12-11T12:02:55Z","type":"conference","alternative_title":["LNCS"],"conference":{"end_date":"2011-07-20","location":"Snowbird, USA","name":"CAV: Computer Aided Verification","start_date":"2011-07-14"},"status":"public","oa_version":"Submitted Version","_id":"3366","publication_status":"published","intvolume":"      6806","day":"21","has_accepted_license":"1","editor":[{"first_name":"Ganesh","last_name":"Gopalakrishnan","full_name":"Gopalakrishnan, Ganesh"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"ddc":["000","004"],"scopus_import":"1"},{"volume":22,"citation":{"mla":"Henzinger, Thomas A., et al. “Formalisms for Specifying Markovian Population Models.” <i>IJFCS: International Journal of Foundations of Computer Science</i>, vol. 22, no. 4, World Scientific Publishing, 2011, pp. 823–41, doi:<a href=\"https://doi.org/10.1142/S0129054111008441\">10.1142/S0129054111008441</a>.","ama":"Henzinger TA, Jobstmann B, Wolf V. Formalisms for specifying Markovian population models. <i>IJFCS: International Journal of Foundations of Computer Science</i>. 2011;22(4):823-841. doi:<a href=\"https://doi.org/10.1142/S0129054111008441\">10.1142/S0129054111008441</a>","apa":"Henzinger, T. A., Jobstmann, B., &#38; Wolf, V. (2011). Formalisms for specifying Markovian population models. <i>IJFCS: International Journal of Foundations of Computer Science</i>. World Scientific Publishing. <a href=\"https://doi.org/10.1142/S0129054111008441\">https://doi.org/10.1142/S0129054111008441</a>","ista":"Henzinger TA, Jobstmann B, Wolf V. 2011. Formalisms for specifying Markovian population models. IJFCS: International Journal of Foundations of Computer Science. 22(4), 823–841.","short":"T.A. Henzinger, B. Jobstmann, V. Wolf, IJFCS: International Journal of Foundations of Computer Science 22 (2011) 823–841.","chicago":"Henzinger, Thomas A, Barbara Jobstmann, and Verena Wolf. “Formalisms for Specifying Markovian Population Models.” <i>IJFCS: International Journal of Foundations of Computer Science</i>. World Scientific Publishing, 2011. <a href=\"https://doi.org/10.1142/S0129054111008441\">https://doi.org/10.1142/S0129054111008441</a>.","ieee":"T. A. Henzinger, B. Jobstmann, and V. Wolf, “Formalisms for specifying Markovian population models,” <i>IJFCS: International Journal of Foundations of Computer Science</i>, vol. 22, no. 4. World Scientific Publishing, pp. 823–841, 2011."},"doi":"10.1142/S0129054111008441","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"4707","date_updated":"2020-07-14T12:46:11Z","file_size":222840,"checksum":"df88431872586c773fbcfea37d7b36a2","date_created":"2018-12-12T10:08:45Z","file_name":"IST-2016-628-v1+1_journals-ijfcs-HenzingerJW11.pdf","creator":"system","access_level":"open_access"}],"file_date_updated":"2020-07-14T12:46:11Z","quality_controlled":"1","publication":"IJFCS: International Journal of Foundations of Computer Science","oa_version":"Submitted Version","status":"public","type":"journal_article","date_created":"2018-12-11T12:03:00Z","related_material":{"record":[{"relation":"earlier_version","id":"3841","status":"public"}]},"scopus_import":"1","ddc":["000"],"has_accepted_license":"1","day":"01","intvolume":"        22","publication_status":"published","_id":"3381","abstract":[{"text":"In this survey, we compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. All these languages — matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models — describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, and ease of use. Moreover, they provide different support for checking the well-formedness of a model and for analyzing a model.","lang":"eng"}],"publisher":"World Scientific Publishing","pubrep_id":"628","oa":1,"month":"06","page":"823 - 841","year":"2011","isi":1,"language":[{"iso":"eng"}],"issue":"4","title":"Formalisms for specifying Markovian population models","date_updated":"2025-09-30T08:49:01Z","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"first_name":"Verena","last_name":"Wolf","full_name":"Wolf, Verena"}],"publist_id":"3226","date_published":"2011-06-01T00:00:00Z","department":[{"_id":"ToHe"}],"external_id":{"isi":["000291552600005"]},"article_processing_charge":"No"},{"_id":"3315","publication_status":"published","day":"14","intvolume":"         7","has_accepted_license":"1","ddc":["000","005"],"scopus_import":"1","related_material":{"record":[{"status":"public","id":"3876","relation":"earlier_version"}]},"corr_author":"1","date_created":"2018-12-11T12:02:37Z","type":"journal_article","oa_version":"Published Version","status":"public","publication":"Logical Methods in Computer Science","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:07Z","file":[{"file_name":"IST-2016-86-v2+1_1011.0688_3_.pdf","creator":"system","date_created":"2018-12-12T10:16:42Z","access_level":"open_access","file_id":"5231","relation":"main_file","content_type":"application/pdf","checksum":"3480e1594bbef25ff7462fa93a8a814e","date_updated":"2020-07-14T12:46:07Z","file_size":588863}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.2168/LMCS-7(4:8)2011","license":"https://creativecommons.org/licenses/by-nd/4.0/","volume":7,"citation":{"mla":"Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4, International Federation for Computational Logic, 2011, doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Prabhu, V. (2011). Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science 7 (2011).","ista":"Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 7(4).","ama":"Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. 2011;7(4). doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity and robustness,” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4. International Federation for Computational Logic, 2011.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2011. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>."},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publist_id":"3324","date_published":"2011-12-14T00:00:00Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"issue":"4","title":"Timed parity games: Complexity and robustness","date_updated":"2026-07-06T13:25:39Z","ec_funded":1,"das_tickbox":"1","tmp":{"image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)","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)"},"language":[{"iso":"eng"}],"year":"2011","month":"12","oa":1,"project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"}],"pubrep_id":"506","publisher":"International Federation for Computational Logic","abstract":[{"lang":"eng","text":"We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., not concurrent) finite-state (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers."}]},{"department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_updated":"2026-07-07T06:07:16Z","title":"Static scheduling in clouds","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Singh, Anmol","last_name":"Singh","first_name":"Anmol","id":"72A86902-E99F-11E9-9F62-915534D1B916"},{"id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh","full_name":"Singh, Vasu"},{"full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736"}],"date_published":"2011-06-14T00:00:00Z","publist_id":"3338","das_tickbox":"1","page":"1 - 6","month":"06","year":"2011","language":[{"iso":"eng"}],"oa":1,"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"}],"publisher":"Usenix Association","pubrep_id":"90","day":"14","publication_status":"published","_id":"3302","ddc":["000","005"],"has_accepted_license":"1","date_created":"2018-12-11T12:02:33Z","corr_author":"1","oa_version":"Submitted Version","status":"public","publication":"3rd USENIX Workshop on Hot Topics in Cloud Computing","conference":{"end_date":"2011-06-15","location":"Portland, OR, United States","name":"HotCloud: Workshop on Hot Topics in Cloud Computing","start_date":"2011-06-14"},"type":"conference","file_date_updated":"2020-07-14T12:46:06Z","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"5333","relation":"main_file","content_type":"application/pdf","checksum":"21a461ac004bb535c83320fe79b30375","date_updated":"2020-07-14T12:46:06Z","file_size":232770,"file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","creator":"system","date_created":"2018-12-12T10:18:14Z","access_level":"open_access"}],"citation":{"mla":"Henzinger, Thomas A., et al. “Static Scheduling in Clouds.” <i>3rd USENIX Workshop on Hot Topics in Cloud Computing</i>, Usenix Association, 2011, pp. 1–6.","ista":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. 3rd USENIX Workshop on Hot Topics in Cloud Computing. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.","short":"T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, 3rd USENIX Workshop on Hot Topics in Cloud Computing, Usenix Association, 2011, pp. 1–6.","apa":"Henzinger, T. A., Singh, A., Singh, V., Wies, T., &#38; Zufferey, D. (2011). Static scheduling in clouds. In <i>3rd USENIX Workshop on Hot Topics in Cloud Computing</i> (pp. 1–6). Portland, OR, United States: Usenix Association.","ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: <i>3rd USENIX Workshop on Hot Topics in Cloud Computing</i>. Usenix Association; 2011:1-6.","ieee":"T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” in <i>3rd USENIX Workshop on Hot Topics in Cloud Computing</i>, Portland, OR, United States, 2011, pp. 1–6.","chicago":"Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds.” In <i>3rd USENIX Workshop on Hot Topics in Cloud Computing</i>, 1–6. Usenix Association, 2011."}},{"abstract":[{"text":"There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with \"controlled-accumulation\", allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.","lang":"eng"}],"publisher":"IEEE","pubrep_id":"83","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa":1,"year":"2011","month":"06","isi":1,"language":[{"iso":"eng"}],"ec_funded":1,"date_updated":"2026-07-07T14:01:43Z","title":"Temporal specifications with accumulative values","publist_id":"3259","date_published":"2011-06-21T00:00:00Z","author":[{"last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","external_id":{"isi":["000297350400007"]},"citation":{"chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” IEEE, 2011. <a href=\"https://doi.org/10.1109/LICS.2011.33\">https://doi.org/10.1109/LICS.2011.33</a>.","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” presented at the LICS: Logic in Computer Science, Toronto, Canada, 2011.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. In: IEEE; 2011. doi:<a href=\"https://doi.org/10.1109/LICS.2011.33\">10.1109/LICS.2011.33</a>","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2011). Temporal specifications with accumulative values. Presented at the LICS: Logic in Computer Science, Toronto, Canada: IEEE. <a href=\"https://doi.org/10.1109/LICS.2011.33\">https://doi.org/10.1109/LICS.2011.33</a>","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, in:, IEEE, 2011.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values. LICS: Logic in Computer Science, 5970226.","mla":"Boker, Udi, et al. <i>Temporal Specifications with Accumulative Values</i>. 5970226, IEEE, 2011, doi:<a href=\"https://doi.org/10.1109/LICS.2011.33\">10.1109/LICS.2011.33</a>."},"article_number":"5970226","doi":"10.1109/LICS.2011.33","file":[{"creator":"system","file_name":"IST-2012-83-v1+1_Temporal_specifications_with_accumulative_values.pdf","date_created":"2018-12-12T10:12:42Z","access_level":"open_access","file_id":"4960","content_type":"application/pdf","relation":"main_file","checksum":"792128f5455f0f40f1105f0398e05fa9","file_size":225426,"date_updated":"2020-07-14T12:46:09Z"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file_date_updated":"2020-07-14T12:46:09Z","status":"public","oa_version":"Submitted Version","type":"conference","conference":{"location":"Toronto, Canada","start_date":"2011-06-21","name":"LICS: Logic in Computer Science","end_date":"2011-06-24"},"date_created":"2018-12-11T12:02:52Z","related_material":{"record":[{"relation":"earlier_version","id":"5385","status":"public"},{"status":"public","id":"2038","relation":"later_version"}]},"scopus_import":"1","has_accepted_license":"1","ddc":["000","004"],"publication_status":"published","day":"21","_id":"3356"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2026-07-07T14:01:43Z","title":"Temporal specifications with accumulative values","date_published":"2011-04-04T00:00:00Z","author":[{"full_name":"Boker, Udi","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"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":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"ec_funded":1,"month":"04","year":"2011","page":"14","language":[{"iso":"eng"}],"oa":1,"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"text":"There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”, allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.","lang":"eng"}],"pubrep_id":"21","publisher":"IST Austria","publication_status":"published","day":"04","_id":"5385","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","ddc":["000","004"],"date_created":"2018-12-12T11:39:02Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"3356"},{"relation":"later_version","status":"public","id":"2038"}]},"status":"public","oa_version":"Published Version","type":"technical_report","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:41Z","file":[{"file_size":366281,"date_updated":"2020-07-14T12:46:41Z","checksum":"8491d0d48c4911620ecd5350b413c11e","content_type":"application/pdf","relation":"main_file","file_id":"5461","access_level":"open_access","date_created":"2018-12-12T11:53:00Z","creator":"system","file_name":"IST-2011-0003_IST-2011-0003.pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.15479/AT:IST-2011-0003","citation":{"mla":"Boker, Udi, et al. <i>Temporal Specifications with Accumulative Values</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">10.15479/AT:IST-2011-0003</a>.","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2011). <i>Temporal specifications with accumulative values</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">https://doi.org/10.15479/AT:IST-2011-0003</a>","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values, IST Austria, 14p.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications with Accumulative Values, IST Austria, 2011.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. <i>Temporal Specifications with Accumulative Values</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">10.15479/AT:IST-2011-0003</a>","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, <i>Temporal specifications with accumulative values</i>. IST Austria, 2011.","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. <i>Temporal Specifications with Accumulative Values</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0003\">https://doi.org/10.15479/AT:IST-2011-0003</a>."}},{"ec_funded":1,"das_tickbox":"1","author":[{"full_name":"Tripakis, Stavros","last_name":"Tripakis","first_name":"Stavros"},{"full_name":"Lickly, Ben","last_name":"Lickly","first_name":"Ben"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Lee, Edward","last_name":"Lee","first_name":"Edward"}],"date_published":"2011-07-01T00:00:00Z","publist_id":"3263","date_updated":"2026-07-07T14:03:34Z","title":"A theory of synchronous relational interfaces","issue":"4","external_id":{"isi":["000292766400003"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"publisher":"ACM","pubrep_id":"85","abstract":[{"lang":"eng","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."}],"project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa":1,"isi":1,"language":[{"iso":"eng"}],"year":"2011","month":"07","type":"journal_article","publication":"ACM Transactions on Programming Languages and Systems","oa_version":"Submitted Version","status":"public","date_created":"2018-12-11T12:02:51Z","ddc":["000","005"],"has_accepted_license":"1","scopus_import":"1","_id":"3353","intvolume":"        33","day":"01","publication_status":"published","article_number":"14","citation":{"ama":"Tripakis S, Lickly B, Henzinger TA, Lee E. A theory of synchronous relational interfaces. <i>ACM Transactions on Programming Languages and Systems</i>. 2011;33(4). doi:<a href=\"https://doi.org/10.1145/1985342.1985345\">10.1145/1985342.1985345</a>","apa":"Tripakis, S., Lickly, B., Henzinger, T. A., &#38; Lee, E. (2011). A theory of synchronous relational interfaces. <i>ACM Transactions on Programming Languages and Systems</i>. ACM. <a href=\"https://doi.org/10.1145/1985342.1985345\">https://doi.org/10.1145/1985342.1985345</a>","ista":"Tripakis S, Lickly B, Henzinger TA, Lee E. 2011. A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems. 33(4), 14.","short":"S. Tripakis, B. Lickly, T.A. Henzinger, E. Lee, ACM Transactions on Programming Languages and Systems 33 (2011).","mla":"Tripakis, Stavros, et al. “A Theory of Synchronous Relational Interfaces.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 33, no. 4, 14, ACM, 2011, doi:<a href=\"https://doi.org/10.1145/1985342.1985345\">10.1145/1985342.1985345</a>.","chicago":"Tripakis, Stavros, Ben Lickly, Thomas A Henzinger, and Edward Lee. “A Theory of Synchronous Relational Interfaces.” <i>ACM Transactions on Programming Languages and Systems</i>. ACM, 2011. <a href=\"https://doi.org/10.1145/1985342.1985345\">https://doi.org/10.1145/1985342.1985345</a>.","ieee":"S. Tripakis, B. Lickly, T. A. Henzinger, and E. Lee, “A theory of synchronous relational interfaces,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 33, no. 4. ACM, 2011."},"volume":33,"doi":"10.1145/1985342.1985345","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"5235","file_size":775662,"date_updated":"2020-07-14T12:46:09Z","checksum":"5d44a8aa81e33210649beae507602138","date_created":"2018-12-12T10:16:45Z","creator":"system","file_name":"IST-2012-85-v1+1_A_theory_of_synchronous_relational_interfaces.pdf","access_level":"open_access"}],"quality_controlled":"1","file_date_updated":"2020-07-14T12:46:09Z"},{"year":"2011","month":"07","isi":1,"language":[{"iso":"eng"}],"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"abstract":[{"lang":"eng","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."}],"publisher":"ACM","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000296202300006"]},"issue":"4","title":"Qualitative concurrent parity games","date_updated":"2026-07-07T14:02:38Z","date_published":"2011-07-04T00:00:00Z","publist_id":"3262","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"das_tickbox":"1","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1145/1970398.1970404","volume":12,"citation":{"mla":"Chatterjee, Krishnendu, et al. “Qualitative Concurrent Parity Games.” <i>ACM Transactions on Computational Logic</i>, vol. 12, no. 4, 28, ACM, 2011, doi:<a href=\"https://doi.org/10.1145/1970398.1970404\">10.1145/1970398.1970404</a>.","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Qualitative concurrent parity games. <i>ACM Transactions on Computational Logic</i>. 2011;12(4). doi:<a href=\"https://doi.org/10.1145/1970398.1970404\">10.1145/1970398.1970404</a>","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2011. Qualitative concurrent parity games. ACM Transactions on Computational Logic. 12(4), 28.","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2011). Qualitative concurrent parity games. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/1970398.1970404\">https://doi.org/10.1145/1970398.1970404</a>","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational Logic 12 (2011).","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Qualitative Concurrent Parity Games.” <i>ACM Transactions on Computational Logic</i>. ACM, 2011. <a href=\"https://doi.org/10.1145/1970398.1970404\">https://doi.org/10.1145/1970398.1970404</a>.","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Qualitative concurrent parity games,” <i>ACM Transactions on Computational Logic</i>, vol. 12, no. 4. ACM, 2011."},"article_number":"28","publication_status":"published","intvolume":"        12","day":"04","_id":"3354","scopus_import":"1","date_created":"2018-12-11T12:02:51Z","related_material":{"record":[{"id":"2054","status":"public","relation":"later_version"}]},"corr_author":"1","oa_version":"None","publication":"ACM Transactions on Computational Logic","status":"public","type":"journal_article"},{"date_updated":"2025-09-30T09:51:13Z","series_title":"LNCS","title":"ABC: Algebraic Bound Computation for loops","date_published":"2010-05-01T00:00:00Z","author":[{"full_name":"Blanc, Régis","last_name":"Blanc","first_name":"Régis"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Hottelier, Thibaud","last_name":"Hottelier","first_name":"Thibaud"},{"full_name":"Kovács, Laura","last_name":"Kovács","first_name":"Laura"}],"main_file_link":[{"url":"https://infoscience.epfl.ch/record/186096","open_access":"1"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000309668000007"]},"place":"Berlin, Heidelberg","oa":1,"page":"103-118","month":"05","year":"2010","language":[{"iso":"eng"}],"isi":1,"abstract":[{"lang":"eng","text":"We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts."}],"publisher":"Springer Nature","scopus_import":"1","editor":[{"first_name":"Edmund M","last_name":"Clarke","full_name":"Clarke, Edmund M"},{"full_name":"Voronkov, Andrei","last_name":"Voronkov","first_name":"Andrei"}],"acknowledgement":"This work was supported in part by the Swiss NSF. The fourth author is supported by an FWF Hertha Firnberg Research grant (T425-N23).","publication_status":"published","intvolume":"      6355","day":"01","_id":"10908","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783642175107"],"eisbn":["9783642175114"]},"publication":"Logic for Programming, Artificial Intelligence, and Reasoning","status":"public","oa_version":"Submitted Version","type":"conference","conference":{"end_date":"2010-05-01","start_date":"2010-04-25","name":"LPAR: Logic for Programming, Artificial Intelligence and Reasoning","location":"Dakar, Senegal"},"date_created":"2022-03-21T08:14:35Z","corr_author":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","citation":{"chicago":"Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács. “ABC: Algebraic Bound Computation for Loops.” In <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, 6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>.","ieee":"R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound Computation for loops,” in <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, Dakar, Senegal, 2010, vol. 6355, pp. 103–118.","ama":"Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation for loops. In: Clarke EM, Voronkov A, eds. <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>. Vol 6355. LNCS. Berlin, Heidelberg: Springer Nature; 2010:103-118. doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>","short":"R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer Nature, Berlin, Heidelberg, 2010, pp. 103–118.","ista":"Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning. LPAR: Logic for Programming, Artificial Intelligence and ReasoningLNCS vol. 6355, 103–118.","apa":"Blanc, R., Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2010). ABC: Algebraic Bound Computation for loops. In E. M. Clarke &#38; A. Voronkov (Eds.), <i>Logic for Programming, Artificial Intelligence, and Reasoning</i> (Vol. 6355, pp. 103–118). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>","mla":"Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>."},"volume":6355,"doi":"10.1007/978-3-642-17511-4_7"},{"language":[{"iso":"eng"}],"year":"2010","page":"94 - 108","month":"03","oa":1,"pubrep_id":"50","publisher":"Springer","abstract":[{"text":"Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems.","lang":"eng"}],"department":[{"_id":"ToHe"}],"publist_id":"1099","date_published":"2010-03-01T00:00:00Z","author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas"},{"last_name":"Zufferey","orcid":"0000-0002-3197-8736","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"title":"Forward analysis of depth-bounded processes","date_updated":"2026-04-09T14:35:23Z","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:27Z","file":[{"access_level":"open_access","creator":"system","file_name":"IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf","date_created":"2018-12-12T10:08:17Z","checksum":"3e610de84937d821316362658239134a","file_size":240766,"date_updated":"2020-07-14T12:46:27Z","file_id":"4677","content_type":"application/pdf","relation":"main_file"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-642-12032-9_8","volume":6014,"citation":{"chicago":"Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>.","ieee":"T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded processes,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.","ama":"Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes. In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>","ista":"Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.","apa":"Wies, T., Zufferey, D., &#38; Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>","short":"T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108.","mla":"Wies, Thomas, et al. <i>Forward Analysis of Depth-Bounded Processes</i>. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>."},"_id":"4361","publication_status":"published","intvolume":"      6014","day":"01","editor":[{"last_name":"Ong","first_name":"Luke","full_name":"Ong, Luke"}],"has_accepted_license":"1","ddc":["004"],"scopus_import":1,"related_material":{"record":[{"status":"public","id":"1405","relation":"dissertation_contains"}]},"corr_author":"1","date_created":"2018-12-11T12:08:27Z","alternative_title":["LNCS"],"type":"conference","conference":{"location":"Paphos, Cyprus","name":"FoSSaCS: Foundations of Software Science and Computation Structures","start_date":"2010-03-20","end_date":"2010-03-28"},"status":"public","oa_version":"Submitted Version"},{"publist_id":"1096","editor":[{"full_name":"Sokolsky, Oleg","last_name":"Sokolsky","first_name":"Oleg"},{"full_name":"Rosu, Grigore","last_name":"Rosu","first_name":"Grigore"},{"full_name":"Tilmann, Nikolai","first_name":"Nikolai","last_name":"Tilmann"},{"full_name":"Barringer, Howard","last_name":"Barringer","first_name":"Howard"},{"full_name":"Falcone, Ylies","last_name":"Falcone","first_name":"Ylies"},{"last_name":"Finkbeiner","first_name":"Bernd","full_name":"Finkbeiner, Bernd"},{"full_name":"Havelund, Klaus","last_name":"Havelund","first_name":"Klaus"},{"full_name":"Lee, Insup","first_name":"Insup","last_name":"Lee"},{"full_name":"Pace, Gordon","last_name":"Pace","first_name":"Gordon"}],"date_published":"2010-01-01T00:00:00Z","author":[{"full_name":"Singh, Vasu","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"}],"scopus_import":1,"title":"Runtime verification for software transactional memories","date_updated":"2024-10-09T20:54:01Z","_id":"4362","publication_status":"published","day":"01","department":[{"_id":"ToHe"}],"intvolume":"      6418","type":"conference","alternative_title":["LNCS"],"conference":{"start_date":"2010-11-01","name":"RV: International Conference on Runtime Verification","location":"St. Julians, Malta","end_date":"2010-11-04"},"status":"public","oa_version":"None","corr_author":"1","date_created":"2018-12-11T12:08:28Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","language":[{"iso":"eng"}],"page":"421 - 435","year":"2010","month":"01","publisher":"Springer","volume":6418,"citation":{"chicago":"Singh, Vasu. “Runtime Verification for Software Transactional Memories.” edited by Oleg Sokolsky, Grigore Rosu, Nikolai Tilmann, Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, and Gordon Pace, 6418:421–35. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-16612-9_32\">https://doi.org/10.1007/978-3-642-16612-9_32</a>.","ieee":"V. Singh, “Runtime verification for software transactional memories,” presented at the RV: International Conference on Runtime Verification, St. Julians, Malta, 2010, vol. 6418, pp. 421–435.","ama":"Singh V. Runtime verification for software transactional memories. In: Sokolsky O, Rosu G, Tilmann N, et al., eds. Vol 6418. Springer; 2010:421-435. doi:<a href=\"https://doi.org/10.1007/978-3-642-16612-9_32\">10.1007/978-3-642-16612-9_32</a>","apa":"Singh, V. (2010). Runtime verification for software transactional memories. In O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner, … G. Pace (Eds.) (Vol. 6418, pp. 421–435). Presented at the RV: International Conference on Runtime Verification, St. Julians, Malta: Springer. <a href=\"https://doi.org/10.1007/978-3-642-16612-9_32\">https://doi.org/10.1007/978-3-642-16612-9_32</a>","short":"V. Singh, in:, O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund, I. Lee, G. Pace (Eds.), Springer, 2010, pp. 421–435.","ista":"Singh V. 2010. Runtime verification for software transactional memories. RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.","mla":"Singh, Vasu. <i>Runtime Verification for Software Transactional Memories</i>. Edited by Oleg Sokolsky et al., vol. 6418, Springer, 2010, pp. 421–35, doi:<a href=\"https://doi.org/10.1007/978-3-642-16612-9_32\">10.1007/978-3-642-16612-9_32</a>."},"abstract":[{"text":"Software transactional memories (STMs) promise simple and efficient concurrent programming. Several correctness properties have been proposed for STMs. Based on a bounded conflict graph algorithm for verifying correctness of STMs, we develop TRACER, a tool for runtime verification of STM implementations. The novelty of TRACER lies in the way it combines coarse and precise runtime analyses to guarantee sound and complete verification in an efficient manner. We implement TRACER in the TL2 STM implementation. We evaluate the performance of TRACER on STAMP benchmarks. While a precise runtime verification technique based on conflict graphs results in an average slowdown of 60x, the two-level approach of TRACER performs complete verification with an average slowdown of around 25x across different benchmarks.","lang":"eng"}],"doi":"10.1007/978-3-642-16612-9_32"},{"date_updated":"2024-10-09T20:54:01Z","title":"From MTL to deterministic timed automata","author":[{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic"},{"full_name":"Piterman, Nir","first_name":"Nir","last_name":"Piterman"}],"publist_id":"1090","date_published":"2010-09-08T00:00:00Z","department":[{"_id":"ToHe"}],"ec_funded":1,"oa":1,"year":"2010","month":"09","page":"152 - 167","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"In this paper we propose a novel technique for constructing timed automata from properties expressed in the logic mtl, under bounded-variability assumptions. We handle full mtl and include all future operators. Our construction is based on separation of the continuous time monitoring of the input sequence and discrete predictions regarding the future. The separation of the continuous from the discrete allows us to determinize our automata in an exponential construction that does not increase the number of clocks. This leads to a doubly exponential construction from mtl to deterministic timed automata, compared with triply exponential using existing approaches. We offer an alternative to the existing approach to linear real-time model checking, which has never been implemented. It further offers a unified framework for model checking, runtime monitoring, and synthesis, in an approach that can reuse tools, implementations, and insights from the discrete setting."}],"publisher":"Springer","pubrep_id":"49","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543"},{"name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"scopus_import":1,"ddc":["004"],"has_accepted_license":"1","editor":[{"full_name":"Henzinger, Thomas A.","last_name":"Henzinger","first_name":"Thomas A."},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"intvolume":"      6246","day":"08","publication_status":"published","_id":"4369","status":"public","oa_version":"Submitted Version","conference":{"end_date":"2010-09-10","start_date":"2010-09-08","name":"FORMATS: Formal Modeling and Analysis of Timed Systems","location":"Klosterneuburg, Austria"},"alternative_title":["LNCS"],"type":"conference","date_created":"2018-12-11T12:08:30Z","corr_author":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"IST-2012-49-v1+1_From_MTL_to_deterministic_timed_automata.pdf","creator":"system","date_created":"2018-12-12T10:13:43Z","access_level":"open_access","file_id":"5028","relation":"main_file","content_type":"application/pdf","checksum":"b0ca5f5fbe8a3d20ccbc6f51a344a459","date_updated":"2020-07-14T12:46:27Z","file_size":249789}],"file_date_updated":"2020-07-14T12:46:27Z","quality_controlled":"1","volume":6246,"citation":{"ieee":"D. Nickovic and N. Piterman, “From MTL to deterministic timed automata,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg, Austria, 2010, vol. 6246, pp. 152–167.","chicago":"Nickovic, Dejan, and Nir Piterman. “From MTL to Deterministic Timed Automata.” edited by Thomas A. Henzinger and Krishnendu Chatterjee, 6246:152–67. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">https://doi.org/10.1007/978-3-642-15297-9_13</a>.","mla":"Nickovic, Dejan, and Nir Piterman. <i>From MTL to Deterministic Timed Automata</i>. Edited by Thomas A. Henzinger and Krishnendu Chatterjee, vol. 6246, Springer, 2010, pp. 152–67, doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">10.1007/978-3-642-15297-9_13</a>.","ista":"Nickovic D, Piterman N. 2010. From MTL to deterministic timed automata. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 6246, 152–167.","short":"D. Nickovic, N. Piterman, in:, T.A. Henzinger, K. Chatterjee (Eds.), Springer, 2010, pp. 152–167.","apa":"Nickovic, D., &#38; Piterman, N. (2010). From MTL to deterministic timed automata. In T. A. Henzinger &#38; K. Chatterjee (Eds.) (Vol. 6246, pp. 152–167). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">https://doi.org/10.1007/978-3-642-15297-9_13</a>","ama":"Nickovic D, Piterman N. From MTL to deterministic timed automata. In: Henzinger TA, Chatterjee K, eds. Vol 6246. Springer; 2010:152-167. doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9_13\">10.1007/978-3-642-15297-9_13</a>"},"doi":"10.1007/978-3-642-15297-9_13"},{"quality_controlled":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-642-11319-2_6","volume":5944,"citation":{"chicago":"Kuncak, Viktor, Ruzica Piskac, Philippe Suter, and Thomas Wies. “Building a Calculus of Data Structures.” edited by Gilles Barthe and Manuel Hermenegildo, 5944:26–44. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">https://doi.org/10.1007/978-3-642-11319-2_6</a>.","ieee":"V. Kuncak, R. Piskac, P. Suter, and T. Wies, “Building a calculus of data structures,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 26–44.","ama":"Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures. In: Barthe G, Hermenegildo M, eds. Vol 5944. Springer; 2010:26-44. doi:<a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">10.1007/978-3-642-11319-2_6</a>","ista":"Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 26–44.","short":"V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo (Eds.), Springer, 2010, pp. 26–44.","apa":"Kuncak, V., Piskac, R., Suter, P., &#38; Wies, T. (2010). Building a calculus of data structures. In G. Barthe &#38; M. Hermenegildo (Eds.) (Vol. 5944, pp. 26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">https://doi.org/10.1007/978-3-642-11319-2_6</a>","mla":"Kuncak, Viktor, et al. <i>Building a Calculus of Data Structures</i>. Edited by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44, doi:<a href=\"https://doi.org/10.1007/978-3-642-11319-2_6\">10.1007/978-3-642-11319-2_6</a>."},"_id":"4378","day":"01","intvolume":"      5944","publication_status":"published","editor":[{"full_name":"Barthe, Gilles","last_name":"Barthe","first_name":"Gilles"},{"full_name":"Hermenegildo, Manuel","first_name":"Manuel","last_name":"Hermenegildo"}],"scopus_import":1,"date_created":"2018-12-11T12:08:33Z","conference":{"end_date":"2010-01-19","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2010-01-17","location":"Madrid, Spain"},"alternative_title":["LNCS"],"type":"conference","status":"public","oa_version":"Submitted Version","language":[{"iso":"eng"}],"page":"26 - 44","month":"01","year":"2010","oa":1,"publisher":"Springer","abstract":[{"text":"Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets, multisets, algebraic data types, or graphs. Consequently, formulas generated from verification also involve such data structures. To automate the proofs of such formulas we propose a logic (a “calculus”) of such data structures. We build the calculus by starting from decidable logics of individual data structures, and connecting them through functions and sets, in ways that go beyond the frameworks such as Nelson-Oppen. The result are new decidable logics that can simultaneously specify properties of different kinds of data structures and overcome the limitations of the individual logics. Several of our decidable logics include abstraction functions that map a data structure into its more abstract view (a tree into a multiset, a multiset into a set), into a numerical quantity (the size or the height), or into the truth value of a candidate data structure invariant (sortedness, or the heap property). For algebraic data types, we identify an asymptotic many-to-one condition on the abstraction function that guarantees the existence of a decision procedure. In addition to the combination based on abstraction functions, we can combine multiple data structure theories if they all reduce to the same data structure logic. As an instance of this approach, we describe a decidable logic whose formulas are propositional combinations of formulas in: weak monadic second-order logic of two successors, two-variable logic with counting, multiset algebra with Presburger arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the logic of algebraic data types with the set content function. The subformulas in this combination can share common variables that refer to sets of objects along with the common set algebra operations. Such sound and complete combination is possible because the relations on sets definable in the component logics are all expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic and its new extensions play an important role in our decidability results. In several cases, when we combine logics that belong to NP, we can prove the satisfiability for the combined logic is still in NP.","lang":"eng"}],"department":[{"_id":"ToHe"}],"author":[{"first_name":"Viktor","last_name":"Kuncak","full_name":"Kuncak, Viktor"},{"first_name":"Ruzica","last_name":"Piskac","full_name":"Piskac, Ruzica"},{"first_name":"Philippe","last_name":"Suter","full_name":"Suter, Philippe"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas"}],"main_file_link":[{"url":"https://infoscience.epfl.ch/record/161290/","open_access":"1"}],"publist_id":"1081","date_published":"2010-01-01T00:00:00Z","title":"Building a calculus of data structures","date_updated":"2021-01-12T07:56:31Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-12T10:09:42Z","creator":"system","file_name":"IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_id":"4767","file_size":222626,"date_updated":"2020-07-14T12:46:28Z","checksum":"7680dd24016810710f7c977bc94f85e9"}],"quality_controlled":"1","file_date_updated":"2020-07-14T12:46:28Z","citation":{"ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud resources. In: ACM; 2010:1-8. doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>","mla":"Henzinger, Thomas A., et al. <i>A Marketplace for Cloud Resources</i>. ACM, 2010, pp. 1–8, doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>.","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “A Marketplace for Cloud Resources,” 1–8. ACM, 2010. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>.","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA, 2010, pp. 1–8."},"doi":"10.1145/1879021.1879022","ddc":["005"],"has_accepted_license":"1","scopus_import":1,"_id":"4380","day":"24","publication_status":"published","conference":{"end_date":"2010-10-29","location":"Arizona, USA","name":"EMSOFT: Embedded Software ","start_date":"2010-10-24"},"type":"conference","status":"public","oa_version":"Submitted Version","corr_author":"1","date_created":"2018-12-11T12:08:33Z","oa":1,"language":[{"iso":"eng"}],"year":"2010","month":"10","page":"1 - 8","pubrep_id":"48","publisher":"ACM","abstract":[{"lang":"eng","text":"Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context."}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Tomar, Anmol","last_name":"Tomar","first_name":"Anmol","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","full_name":"Wies, Thomas"},{"last_name":"Zufferey","orcid":"0000-0002-3197-8736","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien"}],"publist_id":"1078","date_published":"2010-10-24T00:00:00Z","title":"A marketplace for cloud resources","date_updated":"2024-10-09T20:54:01Z","department":[{"_id":"ToHe"}]},{"oa_version":"Submitted Version","status":"public","type":"conference","conference":{"name":"CLOUD: Cloud Computing","start_date":"2010-07-05","location":"Miami, USA","end_date":"2010-07-10"},"date_created":"2018-12-11T12:08:33Z","corr_author":"1","scopus_import":1,"has_accepted_license":"1","ddc":["004"],"publication_status":"published","day":"26","_id":"4381","citation":{"mla":"Henzinger, Thomas A., et al. <i>FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment</i>. IEEE, 2010, pp. 83–90, doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.","ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning of resources in a cloud environment. In: IEEE; 2010:83-90. doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE: Flexible provisioning of resources in a cloud environment,” presented at the CLOUD: Cloud Computing, Miami, USA, 2010, pp. 83–90.","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,” 83–90. IEEE, 2010. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>."},"doi":"10.1109/CLOUD.2010.71","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"5188","date_updated":"2020-07-14T12:46:28Z","file_size":467436,"checksum":"98e534675339a8e2beca08890d048145","date_created":"2018-12-12T10:16:03Z","file_name":"IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf","creator":"system","access_level":"open_access"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:46:28Z","quality_controlled":"1","title":"FlexPRICE: Flexible provisioning of resources in a cloud environment","date_updated":"2024-10-09T20:54:00Z","date_published":"2010-08-26T00:00:00Z","publist_id":"1077","author":[{"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":"Tomar, Anmol","first_name":"Anmol","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87","last_name":"Tomar"},{"last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu"},{"last_name":"Wies","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","abstract":[{"text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases.","lang":"eng"}],"publisher":"IEEE","pubrep_id":"47","oa":1,"year":"2010","month":"08","page":"83 - 90","language":[{"iso":"eng"}]},{"department":[{"_id":"ToHe"}],"title":"Transactions in the jungle","date_updated":"2024-10-21T06:03:05Z","author":[{"full_name":"Guerraoui, Rachid","last_name":"Guerraoui","first_name":"Rachid"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kapalka, Michal","first_name":"Michal","last_name":"Kapalka"},{"full_name":"Singh, Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu"}],"date_published":"2010-06-13T00:00:00Z","publist_id":"1076","abstract":[{"text":"Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to the given underlying memory model. We investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of practical relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows developing more efficient TM implementations.","lang":"eng"}],"pubrep_id":"46","publisher":"ACM","page":"263 - 272","month":"06","year":"2010","language":[{"iso":"eng"}],"oa":1,"date_created":"2018-12-11T12:08:34Z","status":"public","oa_version":"Submitted Version","conference":{"location":"Santorini, Greece","start_date":"2010-06-13","name":"SPAA: ACM Symposium on Parallel Algorithms and Architectures","end_date":"2010-06-15"},"type":"conference","day":"13","publication_status":"published","_id":"4382","scopus_import":"1","ddc":["005"],"has_accepted_license":"1","doi":"10.1145/1810479.1810529","citation":{"ama":"Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle. In: ACM; 2010:263-272. doi:<a href=\"https://doi.org/10.1145/1810479.1810529\">10.1145/1810479.1810529</a>","short":"R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272.","ista":"Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.","apa":"Guerraoui, R., Henzinger, T. A., Kapalka, M., &#38; Singh, V. (2010). Transactions in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece: ACM. <a href=\"https://doi.org/10.1145/1810479.1810529\">https://doi.org/10.1145/1810479.1810529</a>","mla":"Guerraoui, Rachid, et al. <i>Transactions in the Jungle</i>. ACM, 2010, pp. 263–72, doi:<a href=\"https://doi.org/10.1145/1810479.1810529\">10.1145/1810479.1810529</a>.","chicago":"Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh. “Transactions in the Jungle,” 263–72. ACM, 2010. <a href=\"https://doi.org/10.1145/1810479.1810529\">https://doi.org/10.1145/1810479.1810529</a>.","ieee":"R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece, 2010, pp. 263–272."},"file_date_updated":"2020-07-14T12:46:28Z","quality_controlled":"1","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"IST-2012-46-v1+1_Transactions_in_the_jungle.pdf","creator":"system","date_created":"2018-12-12T10:14:28Z","access_level":"open_access","file_id":"5080","relation":"main_file","content_type":"application/pdf","checksum":"f2ad6c00a6304da34bf21bcdcfd36c4b","date_updated":"2020-07-14T12:46:28Z","file_size":246409}]}]