[{"citation":{"mla":"Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments. IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1","ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1"},"oa":1,"page":"11","doi":"10.15479/AT:IST-2013-130-v1-1","date_published":"2013-07-08T00:00:00Z","language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"07","day":"08","year":"2013","_id":"5406","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IST Austria","ddc":["005"],"publication_status":"published","status":"public","title":"Distributed synthesis for LTL Fragments","related_material":{"record":[{"relation":"later_version","status":"public","id":"1376"}]},"pubrep_id":"130","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"oa_version":"Published Version","file":[{"file_name":"IST-2013-130-v1+1_Distributed_Synthesis.pdf","access_level":"open_access","creator":"system","file_size":467895,"content_type":"application/pdf","file_id":"5540","relation":"main_file","date_created":"2018-12-12T11:54:18Z","date_updated":"2020-07-14T12:46:45Z","checksum":"855513ebaf6f72228800c5fdb522f93c"}],"date_created":"2018-12-12T11:39:09Z","date_updated":"2023-02-21T17:01:26Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:45Z"},{"date_published":"2013-08-01T00:00:00Z","page":"273 - 287","citation":{"chicago":"Henzinger, Thomas A, and Jan Otop. “From Model Checking to Model Measuring.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_20.","mla":"Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring. Vol. 8052, Springer, 2013, pp. 273–87, doi:10.1007/978-3-642-40184-8_20.","short":"T.A. Henzinger, J. Otop, 8052 (2013) 273–287.","ista":"Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052, 273–287.","ieee":"T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol. 8052. Springer, pp. 273–287, 2013.","apa":"Henzinger, T. A., & Otop, J. (2013). From model checking to model measuring. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Springer. https://doi.org/10.1007/978-3-642-40184-8_20","ama":"Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287. doi:10.1007/978-3-642-40184-8_20"},"has_accepted_license":"1","day":"01","series_title":"Lecture Notes in Computer Science","file":[{"creator":"system","content_type":"application/pdf","file_size":378587,"file_name":"IST-2013-129-v1+1_concur.pdf","access_level":"open_access","date_created":"2018-12-12T10:17:45Z","date_updated":"2020-07-14T12:45:38Z","checksum":"4c04695c4bfdf2119cd4f5d1babc3e8a","file_id":"5301","relation":"main_file"}],"oa_version":"Submitted Version","pubrep_id":"129","intvolume":" 8052","title":"From model checking to model measuring","status":"public","ddc":["005","000"],"_id":"2327","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M′ within distance ρ from M satisfy (or violate) φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata. The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification, and robustness problems that measure how much a model can be perturbed without violating the specification. We show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved. We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications."}],"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-40184-8_20","conference":{"location":"Buenos Aires, Argentina","start_date":"2013-08-27","end_date":"2013-08-30","name":"CONCUR: Concurrency Theory"},"quality_controlled":"1","oa":1,"month":"08","volume":8052,"date_created":"2018-12-11T11:57:00Z","date_updated":"2023-02-23T12:25:26Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5417"}]},"author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2013","publist_id":"4599","file_date_updated":"2020-07-14T12:45:38Z"},{"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"06","day":"13","oa":1,"citation":{"chicago":"Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1.","short":"T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.","mla":"Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1.","ieee":"T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013.","apa":"Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria. https://doi.org/10.15479/AT:IST-2013-124-v1-1","ista":"Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p.","ama":"Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1"},"page":"23","date_published":"2013-06-13T00:00:00Z","doi":"10.15479/AT:IST-2013-124-v1-1","language":[{"iso":"eng"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:47:30Z","abstract":[{"text":"In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations.","lang":"eng"}],"_id":"6440","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2013","department":[{"_id":"ToHe"}],"publisher":"IST Austria","title":"Replacing competition with cooperation to achieve scalable lock-free FIFO queues ","publication_status":"published","ddc":["000","005"],"status":"public","pubrep_id":"124","author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Payer, Hannes","first_name":"Hannes","last_name":"Payer"},{"first_name":"Ali","last_name":"Sezgin","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali"}],"oa_version":"Published Version","file":[{"file_name":"2013_TechRep_Henzinger.pdf","access_level":"open_access","file_size":549684,"content_type":"application/pdf","creator":"dernst","relation":"main_file","file_id":"6441","date_created":"2019-05-13T14:11:39Z","date_updated":"2020-07-14T12:47:30Z","checksum":"a219ba4eada6cd62befed52262ee15d4"}],"date_created":"2019-05-13T14:13:27Z","date_updated":"2020-07-14T23:06:19Z"},{"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642397981","9783642397998"]},"oa":1,"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"quality_controlled":"1","doi":"10.1007/978-3-642-39799-8_11","conference":{"end_date":"2013-07-19","location":"Saint Petersburg, Russia","start_date":"2013-07-13","name":"CAV 2013"},"language":[{"iso":"eng"}],"place":"Berlin, Heidelberg","ec_funded":1,"file_date_updated":"2020-07-14T12:47:10Z","year":"2013","publisher":"Springer Berlin Heidelberg","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","last_name":"Dragoi","first_name":"Cezara"},{"first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"volume":8044,"date_updated":"2023-09-05T14:16:07Z","date_created":"2018-12-18T13:10:21Z","scopus_import":"1","series_title":"CAV","article_processing_charge":"No","has_accepted_license":"1","citation":{"ieee":"C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates,” in Computer Aided Verification, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.","apa":"Dragoi, C., Gupta, A., & Henzinger, T. A. (2013). Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_11","ista":"Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. vol. 8044, 174–190.","ama":"Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. Vol 8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:10.1007/978-3-642-39799-8_11","chicago":"Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” In Computer Aided Verification, 8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. https://doi.org/10.1007/978-3-642-39799-8_11.","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.","mla":"Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” Computer Aided Verification, vol. 8044, Springer Berlin Heidelberg, 2013, pp. 174–90, doi:10.1007/978-3-642-39799-8_11."},"publication":"Computer Aided Verification","page":"174-190","date_published":"2013-01-01T00:00:00Z","type":"book_chapter","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"5747","intvolume":" 8044","title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","ddc":["005"],"status":"public","pubrep_id":"195","oa_version":"None","file":[{"access_level":"open_access","file_name":"2013_CAV_Dragoi.pdf","file_size":236480,"content_type":"application/pdf","creator":"dernst","relation":"main_file","file_id":"5748","checksum":"a901cc6b71db08b61c0d4c0cbacc6287","date_updated":"2020-07-14T12:47:10Z","date_created":"2018-12-18T13:13:33Z"}]},{"type":"dissertation","alternative_title":["ISTA Thesis"],"abstract":[{"lang":"eng","text":"Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. we present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency.\r\n\r\nFirst, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the PICASSO tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point."}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1405","status":"public","title":"Analysis of dynamic message passing programs","ddc":["000"],"oa_version":"Published Version","file":[{"file_name":"2013_Zufferey_thesis_final.pdf","access_level":"open_access","creator":"dernst","file_size":1514906,"content_type":"application/pdf","file_id":"9176","relation":"main_file","date_updated":"2021-02-22T11:28:36Z","date_created":"2021-02-22T11:28:36Z","success":1,"checksum":"ed2d7b52933d134e8dc69d569baa284e"},{"checksum":"cecc4c4b14225bee973d32e3dba91a55","date_created":"2021-11-16T14:42:52Z","date_updated":"2021-11-17T13:47:58Z","relation":"main_file","file_id":"10298","file_size":1378313,"content_type":"application/pdf","creator":"cchlebak","access_level":"closed","file_name":"2013_Zufferey_thesis_final_pdfa.pdf"}],"has_accepted_license":"1","article_processing_charge":"No","day":"05","citation":{"ieee":"D. Zufferey, “Analysis of dynamic message passing programs,” Institute of Science and Technology Austria, 2013.","apa":"Zufferey, D. (2013). Analysis of dynamic message passing programs. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:1405","ista":"Zufferey D. 2013. Analysis of dynamic message passing programs. Institute of Science and Technology Austria.","ama":"Zufferey D. Analysis of dynamic message passing programs. 2013. doi:10.15479/at:ista:1405","chicago":"Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute of Science and Technology Austria, 2013. https://doi.org/10.15479/at:ista:1405.","short":"D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science and Technology Austria, 2013.","mla":"Zufferey, Damien. Analysis of Dynamic Message Passing Programs. Institute of Science and Technology Austria, 2013, doi:10.15479/at:ista:1405."},"page":"134","date_published":"2013-09-05T00:00:00Z","ec_funded":1,"publist_id":"5802","file_date_updated":"2021-11-17T13:47:58Z","acknowledgement":"This work was supported in part by the Austrian Science Fund NFN RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative Reactve Modeling).\r\nChapter 2, 3, and 4 are joint work with Thomas A. Henzinger and Thomas Wies. Chapter 2 was published in FoSSaCS 2010 as “Forward Analysis of Depth-Bounded Processes” [112]. Chapter 3 was published in VMCAI 2012 as “Ideal Abstractions for Well-Structured Transition Systems” [114]. Chap- ter 5.1 is joint work with Kshitij Bansal, Eric Koskinen, and Thomas Wies. It was published in TACAS 2013 as “Structural Counter Abstraction” [13]. The author’s contribution in this part is mostly related to the implementation. The theory required to understand the method and its implementation is quickly recalled to make the thesis self-contained, but should not be considered as a contribution. For the details of the methods, we refer the reader to the orig- inal publication [13] and the corresponding technical report [14]. Chapter 5.2 is ongoing work with Shahram Esmaeilsabzali, Rupak Majumdar, and Thomas Wies. I also would like to thank the people who supported over the past 4 years. My advisor Thomas A. Henzinger who gave me a lot of freedom to work on projects I was interested in. My collaborators, especially Thomas Wies with whom I worked since the beginning. The members of my thesis committee, Viktor Kun- cak and Rupak Majumdar, who also agreed to advise me. Simon Aeschbacher, Pavol Cerny, Cezara Dragoi, Arjun Radhakrishna, my family, friends and col- leagues who created an enjoyable environment. ","year":"2013","publisher":"Institute of Science and Technology Austria","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"publication_status":"published","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"2847"},{"relation":"part_of_dissertation","status":"public","id":"3251"},{"status":"public","relation":"part_of_dissertation","id":"4361"}]},"author":[{"first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien"}],"date_created":"2018-12-11T11:51:50Z","date_updated":"2023-09-07T11:36:37Z","publication_identifier":{"issn":["2663-337X"]},"month":"09","oa":1,"main_file_link":[{"url":"http://dzufferey.github.io/files/2013_thesis.pdf"}],"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"doi":"10.15479/at:ista:1405","language":[{"iso":"eng"}],"supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"degree_awarded":"PhD"},{"quality_controlled":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"oa":1,"main_file_link":[{"open_access":"1","url":"http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf"}],"language":[{"iso":"eng"}],"conference":{"end_date":"2013-03-24","start_date":"2013-03-16","location":"Rome, Italy","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"doi":"10.1007/978-3-642-36742-7_5","month":"03","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"editor":[{"full_name":"Piterman, Nir","first_name":"Nir","last_name":"Piterman"},{"full_name":"Smolka, Scott","first_name":"Scott","last_name":"Smolka"}],"year":"2013","date_created":"2018-12-11T11:59:54Z","date_updated":"2023-09-07T11:36:36Z","volume":7795,"author":[{"first_name":"Kshitij","last_name":"Bansal","full_name":"Bansal, Kshitij"},{"last_name":"Koskinen","first_name":"Eric","full_name":"Koskinen, Eric"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas"},{"full_name":"Zufferey, Damien","last_name":"Zufferey","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"1405"}]},"ec_funded":1,"publist_id":"3947","page":"62 - 77","citation":{"ama":"Bansal K, Koskinen E, Wies T, Zufferey D. Structural Counter Abstraction. Piterman N, Smolka S, eds. 2013;7795:62-77. doi:10.1007/978-3-642-36742-7_5","apa":"Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman & S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. https://doi.org/10.1007/978-3-642-36742-7_5","ieee":"K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,” vol. 7795. Springer, pp. 62–77, 2013.","ista":"Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman & S. Smolka). 7795, 62–77.","short":"K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.","mla":"Bansal, Kshitij, et al. Structural Counter Abstraction. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:10.1007/978-3-642-36742-7_5.","chicago":"Bansal, Kshitij, Eric Koskinen, Thomas Wies, and Damien Zufferey. “Structural Counter Abstraction.” Edited by Nir Piterman and Scott Smolka. Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-36742-7_5."},"date_published":"2013-03-01T00:00:00Z","series_title":"Lecture Notes in Computer Science","scopus_import":1,"day":"01","status":"public","title":"Structural Counter Abstraction","intvolume":" 7795","_id":"2847","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.","lang":"eng"}]},{"month":"07","oa":1,"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"quality_controlled":"1","doi":"10.1007/978-3-642-39799-8_68","conference":{"name":"CAV: Computer Aided Verification","end_date":"2013-07-19","start_date":"2013-07-13","location":"St. Petersburg, Russia"},"language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"4458","file_date_updated":"2020-07-14T12:45:40Z","year":"2013","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","related_material":{"record":[{"id":"1130","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun"},{"last_name":"Ryzhyk","first_name":"Leonid","full_name":"Ryzhyk, Leonid"},{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","first_name":"Thorsten","last_name":"Tarrach","full_name":"Tarrach, Thorsten"}],"volume":8044,"date_created":"2018-12-11T11:57:42Z","date_updated":"2023-09-07T11:57:01Z","scopus_import":1,"has_accepted_license":"1","day":"01","citation":{"ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Efficient synthesis for concurrency by semantics-preserving transformations. In: Vol 8044. Springer; 2013:951-967. doi:10.1007/978-3-642-39799-8_68","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2013). Efficient synthesis for concurrency by semantics-preserving transformations (Vol. 8044, pp. 951–967). Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_68","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Efficient synthesis for concurrency by semantics-preserving transformations,” presented at the CAV: Computer Aided Verification, St. Petersburg, Russia, 2013, vol. 8044, pp. 951–967.","ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2013. Efficient synthesis for concurrency by semantics-preserving transformations. CAV: Computer Aided Verification, LNCS, vol. 8044, 951–967.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2013, pp. 951–967.","mla":"Cerny, Pavol, et al. Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. Vol. 8044, Springer, 2013, pp. 951–67, doi:10.1007/978-3-642-39799-8_68.","chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Efficient Synthesis for Concurrency by Semantics-Preserving Transformations,” 8044:951–67. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_68."},"page":"951 - 967","date_published":"2013-07-01T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.","lang":"eng"}],"_id":"2445","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 8044","ddc":["000","004"],"status":"public","title":"Efficient synthesis for concurrency by semantics-preserving transformations","pubrep_id":"199","file":[{"file_id":"5158","relation":"main_file","checksum":"70c70ca5487faba82262c63e1b678a27","date_created":"2018-12-12T10:15:37Z","date_updated":"2020-07-14T12:45:40Z","access_level":"open_access","file_name":"IST-2014-199-v1+1_cav2013-final.pdf","creator":"system","content_type":"application/pdf","file_size":365548}],"oa_version":"Submitted Version"},{"article_number":"57","publist_id":"5826","ec_funded":1,"acknowledgement":"This research was supported by the Canadian NSERC grant RGPIN 341819-07, the ERC Advanced Grant QUAREM, and the Austrian Science Fund NFN RiSE.","year":"2012","department":[{"_id":"ToHe"}],"publisher":"ACM","publication_status":"published","author":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Keremoglu, Mehmet","first_name":"Mehmet","last_name":"Keremoglu"},{"last_name":"Wendler","first_name":"Philipp","full_name":"Wendler, Philipp"}],"date_created":"2018-12-11T11:51:42Z","date_updated":"2021-01-12T06:50:18Z","month":"11","main_file_link":[{"url":"http://arxiv.org/abs/1109.6926","open_access":"1"}],"oa":1,"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1145/2393596.2393664","conference":{"location":"Cary, NC, USA","start_date":"2012-11-11","end_date":"2012-11-16","name":"FSE: Foundations of Software Engineering"},"language":[{"iso":"eng"}],"type":"conference","abstract":[{"lang":"eng","text":"Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ - usually a state predicate - such that the program satisfies the specification under the condition Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before."}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1384","title":"Conditional model checking: A technique to pass information between verifiers","status":"public","oa_version":"Preprint","scopus_import":1,"day":"01","citation":{"ama":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking: A technique to pass information between verifiers. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. ACM; 2012. doi:10.1145/2393596.2393664","ista":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking: A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. FSE: Foundations of Software Engineering, 57.","ieee":"D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model checking: A technique to pass information between verifiers,” in Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, Cary, NC, USA, 2012.","apa":"Beyer, D., Henzinger, T. A., Keremoglu, M., & Wendler, P. (2012). Conditional model checking: A technique to pass information between verifiers. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. Cary, NC, USA: ACM. https://doi.org/10.1145/2393596.2393664","mla":"Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, 57, ACM, 2012, doi:10.1145/2393596.2393664.","short":"D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, ACM, 2012.","chicago":"Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. ACM, 2012. https://doi.org/10.1145/2393596.2393664."},"publication":"Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering","date_published":"2012-11-01T00:00:00Z"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"2302","intvolume":" 10","status":"public","title":"The propagation approach for computing biochemical reaction networks","oa_version":"None","type":"journal_article","issue":"2","abstract":[{"lang":"eng","text":"We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only "significant" mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables."}],"citation":{"apa":"Henzinger, T. A., & Mateescu, M. (2012). The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE. https://doi.org/10.1109/TCBB.2012.91","ieee":"T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical reaction networks,” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2. IEEE, pp. 310–322, 2012.","ista":"Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 10(2), 310–322.","ama":"Henzinger TA, Mateescu M. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 2012;10(2):310-322. doi:10.1109/TCBB.2012.91","chicago":"Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics. IEEE, 2012. https://doi.org/10.1109/TCBB.2012.91.","short":"T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322.","mla":"Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:10.1109/TCBB.2012.91."},"publication":"IEEE ACM Transactions on Computational Biology and Bioinformatics","page":"310 - 322","date_published":"2012-07-03T00:00:00Z","scopus_import":1,"day":"03","pmid":1,"year":"2012","publisher":"IEEE","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"publication_status":"published","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Mateescu, Maria","first_name":"Maria","last_name":"Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"}],"volume":10,"date_updated":"2021-01-12T06:56:38Z","date_created":"2018-12-11T11:56:52Z","publist_id":"4625","ec_funded":1,"external_id":{"pmid":["22778152"]},"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"quality_controlled":"1","doi":"10.1109/TCBB.2012.91","language":[{"iso":"eng"}],"month":"07"},{"page":"161 - 173","publication":"Journal of Theoretical Biology","citation":{"ama":"Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 2012;301:161-173. doi:10.1016/j.jtbi.2012.02.021","ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 161–173.","apa":"Chatterjee, K., Zufferey, D., & Nowak, M. (2012). Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2012.02.021","ieee":"K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations with different learners,” Journal of Theoretical Biology, vol. 301. Elsevier, pp. 161–173, 2012.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with Different Learners.” Journal of Theoretical Biology, vol. 301, Elsevier, 2012, pp. 161–73, doi:10.1016/j.jtbi.2012.02.021.","short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","chicago":"Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary Game Dynamics in Populations with Different Learners.” Journal of Theoretical Biology. Elsevier, 2012. https://doi.org/10.1016/j.jtbi.2012.02.021."},"date_published":"2012-05-21T00:00:00Z","scopus_import":1,"day":"21","status":"public","title":"Evolutionary game dynamics in populations with different learners","intvolume":" 301","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"2848","oa_version":"Submitted Version","type":"journal_article","abstract":[{"lang":"eng","text":"We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics."}],"quality_controlled":"1","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"external_id":{"pmid":["22394652"]},"oa":1,"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/"}],"language":[{"iso":"eng"}],"doi":"10.1016/j.jtbi.2012.02.021","month":"05","publication_status":"published","publisher":"Elsevier","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2012","pmid":1,"date_updated":"2021-01-12T07:00:12Z","date_created":"2018-12-11T11:59:55Z","volume":301,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736","first_name":"Damien","last_name":"Zufferey"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"ec_funded":1,"publist_id":"3946"},{"scopus_import":1,"has_accepted_license":"1","day":"01","citation":{"short":"U. Boker, T.A. Henzinger, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–373.","mla":"Boker, Udi, and Thomas A. Henzinger. “Approximate Determinization of Quantitative Automata.” Leibniz International Proceedings in Informatics, vol. 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–73, doi:10.4230/LIPIcs.FSTTCS.2012.362.","chicago":"Boker, Udi, and Thomas A Henzinger. “Approximate Determinization of Quantitative Automata.” In Leibniz International Proceedings in Informatics, 18:362–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362.","ama":"Boker U, Henzinger TA. Approximate determinization of quantitative automata. In: Leibniz International Proceedings in Informatics. Vol 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:362-373. doi:10.4230/LIPIcs.FSTTCS.2012.362","ieee":"U. Boker and T. A. Henzinger, “Approximate determinization of quantitative automata,” in Leibniz International Proceedings in Informatics, Hyderabad, India, 2012, vol. 18, pp. 362–373.","apa":"Boker, U., & Henzinger, T. A. (2012). Approximate determinization of quantitative automata. In Leibniz International Proceedings in Informatics (Vol. 18, pp. 362–373). Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362","ista":"Boker U, Henzinger TA. 2012. Approximate determinization of quantitative automata. Leibniz International Proceedings in Informatics. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 362–373."},"publication":"Leibniz International Proceedings in Informatics","page":"362 - 373","date_published":"2012-12-01T00:00:00Z","type":"conference","alternative_title":["LIPIcs"],"abstract":[{"text":"Quantitative automata are nondeterministic finite automata with edge weights. They value a\r\nrun by some function from the sequence of visited weights to the reals, and value a word by its\r\nminimal/maximal run. They generalize boolean automata, and have gained much attention in\r\nrecent years. Unfortunately, important automaton classes, such as sum, discounted-sum, and\r\nlimit-average automata, cannot be determinized. Yet, the quantitative setting provides the potential\r\nof approximate determinization. We define approximate determinization with respect to\r\na distance function, and investigate this potential.\r\nWe show that sum automata cannot be determinized approximately with respect to any\r\ndistance function. However, restricting to nonnegative weights allows for approximate determinization\r\nwith respect to some distance functions.\r\nDiscounted-sum automata allow for approximate determinization, as the influence of a word’s\r\nsuffix is decaying. However, the naive approach, of unfolding the automaton computations up\r\nto a sufficient level, is shown to be doubly exponential in the discount factor. We provide an\r\nalternative construction that is singly exponential in the discount factor, in the precision, and\r\nin the number of states. We prove matching lower bounds, showing exponential dependency on\r\neach of these three parameters.\r\nAverage and limit-average automata are shown to prohibit approximate determinization with\r\nrespect to any distance function, and this is the case even for two weights, 0 and 1.","lang":"eng"}],"_id":"2891","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","intvolume":" 18","title":"Approximate determinization of quantitative automata","status":"public","ddc":["004"],"pubrep_id":"805","file":[{"file_id":"4826","relation":"main_file","checksum":"88da18d3e2cb2e5011d7d10ce38a3864","date_created":"2018-12-12T10:10:37Z","date_updated":"2020-07-14T12:45:52Z","access_level":"open_access","file_name":"IST-2017-805-v1+1_34.pdf","creator":"system","content_type":"application/pdf","file_size":559069}],"oa_version":"Published Version","month":"12","oa":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.FSTTCS.2012.362","conference":{"name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2012-12-17","start_date":"2012-12-15","location":"Hyderabad, India"},"language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"3867","file_date_updated":"2020-07-14T12:45:52Z","acknowledgement":"We thank Laurent Doyen for great ideas and valuable help in analyzing discounted-sum automata.","year":"2012","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"volume":18,"date_created":"2018-12-11T12:00:10Z","date_updated":"2021-01-12T07:00:31Z"},{"scopus_import":1,"day":"01","month":"10","publication":"Proceedings of the tenth ACM international conference on Embedded software","citation":{"chicago":"Cerny, Pavol, Sivakanth Gopi, Thomas A Henzinger, Arjun Radhakrishna, and Nishant Totla. “Synthesis from Incompatible Specifications.” In Proceedings of the Tenth ACM International Conference on Embedded Software, 53–62. ACM, 2012. https://doi.org/10.1145/2380356.2380371.","short":"P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 53–62.","mla":"Cerny, Pavol, et al. “Synthesis from Incompatible Specifications.” Proceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 53–62, doi:10.1145/2380356.2380371.","ieee":"P. Cerny, S. Gopi, T. A. Henzinger, A. Radhakrishna, and N. Totla, “Synthesis from incompatible specifications,” in Proceedings of the tenth ACM international conference on Embedded software, Tampere, Finland, 2012, pp. 53–62.","apa":"Cerny, P., Gopi, S., Henzinger, T. A., Radhakrishna, A., & Totla, N. (2012). Synthesis from incompatible specifications. In Proceedings of the tenth ACM international conference on Embedded software (pp. 53–62). Tampere, Finland: ACM. https://doi.org/10.1145/2380356.2380371","ista":"Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. 2012. Synthesis from incompatible specifications. Proceedings of the tenth ACM international conference on Embedded software. EMSOFT: Embedded Software , 53–62.","ama":"Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. Synthesis from incompatible specifications. In: Proceedings of the Tenth ACM International Conference on Embedded Software. ACM; 2012:53-62. doi:10.1145/2380356.2380371"},"quality_controlled":"1","page":"53 - 62","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"EMSOFT: Embedded Software ","start_date":"2012-10-07","location":"Tampere, Finland","end_date":"2012-10-12"},"doi":"10.1145/2380356.2380371","date_published":"2012-10-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","abstract":[{"lang":"eng","text":"Systems are often specified using multiple requirements on their behavior. In practice, these requirements can be contradictory. The classical approach to specification, verification, and synthesis demands more detailed specifications that resolve any contradictions in the requirements. These detailed specifications are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative frameworks allow the formalization of the intuitive idea that what is desired is an implementation that comes "closest" to satisfying the mutually incompatible requirements, according to a measure of fit that can be defined by the requirements engineer. One flexible framework for quantifying how "well" an implementation satisfies a specification is offered by simulation distances that are parameterized by an error model. We introduce this framework, study its properties, and provide an algorithmic solution for the following quantitative synthesis question: given two (or more) behavioral requirements specified by possibly incompatible finite-state machines, and an error model, find the finite-state implementation that minimizes the maximal simulation distance to the given requirements. Furthermore, we generalize the framework to handle infinite alphabets (for example, realvalued domains). We also demonstrate how quantitative specifications based on simulation distances might lead to smaller and easier to modify specifications. Finally, we illustrate our approach using case studies on error correcting codes and scheduler synthesis."}],"ec_funded":1,"publist_id":"3868","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"2890","year":"2012","publication_status":"published","status":"public","title":"Synthesis from incompatible specifications","department":[{"_id":"ToHe"}],"publisher":"ACM","author":[{"last_name":"Cerny","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"first_name":"Sivakanth","last_name":"Gopi","full_name":"Gopi, Sivakanth"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Radhakrishna, Arjun","first_name":"Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Totla","first_name":"Nishant","full_name":"Totla, Nishant"}],"date_updated":"2021-01-12T07:00:30Z","date_created":"2018-12-11T12:00:10Z","oa_version":"None"},{"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"quality_controlled":"1","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-33666-9_1","conference":{"end_date":"2012-10-05","start_date":"2012-09-30","location":"Innsbruck, Austria","name":"MODELS: Model-driven Engineering Languages and Systems"},"month":"09","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2012","volume":7590,"date_created":"2018-12-11T12:00:09Z","date_updated":"2021-01-12T07:00:29Z","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"ec_funded":1,"publist_id":"3870","page":"1 - 2","citation":{"short":"T.A. Henzinger, in:, Conference Proceedings MODELS 2012, Springer, 2012, pp. 1–2.","mla":"Henzinger, Thomas A. “Quantitative Reactive Models.” Conference Proceedings MODELS 2012, vol. 7590, Springer, 2012, pp. 1–2, doi:10.1007/978-3-642-33666-9_1.","chicago":"Henzinger, Thomas A. “Quantitative Reactive Models.” In Conference Proceedings MODELS 2012, 7590:1–2. Springer, 2012. https://doi.org/10.1007/978-3-642-33666-9_1.","ama":"Henzinger TA. Quantitative reactive models. In: Conference Proceedings MODELS 2012. Vol 7590. Springer; 2012:1-2. doi:10.1007/978-3-642-33666-9_1","ieee":"T. A. Henzinger, “Quantitative reactive models,” in Conference proceedings MODELS 2012, Innsbruck, Austria, 2012, vol. 7590, pp. 1–2.","apa":"Henzinger, T. A. (2012). Quantitative reactive models. In Conference proceedings MODELS 2012 (Vol. 7590, pp. 1–2). Innsbruck, Austria: Springer. https://doi.org/10.1007/978-3-642-33666-9_1","ista":"Henzinger TA. 2012. Quantitative reactive models. Conference proceedings MODELS 2012. MODELS: Model-driven Engineering Languages and Systems, LNCS, vol. 7590, 1–2."},"publication":"Conference proceedings MODELS 2012","date_published":"2012-09-01T00:00:00Z","scopus_import":1,"day":"01","intvolume":" 7590","title":"Quantitative reactive models","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"2888","oa_version":"None","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria."}]},{"type":"conference","abstract":[{"lang":"eng","text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a quantitative measure for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intu- itively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, and that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies."}],"status":"public","title":"Interface Simulation Distances","intvolume":" 96","_id":"2916","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","scopus_import":1,"day":"07","page":"29 - 42","publication":"Electronic Proceedings in Theoretical Computer Science","citation":{"ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface Simulation Distances,” in Electronic Proceedings in Theoretical Computer Science, Napoli, Italy, 2012, vol. 96, pp. 29–42.","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., & Radhakrishna, A. (2012). Interface Simulation Distances. In Electronic Proceedings in Theoretical Computer Science (Vol. 96, pp. 29–42). Napoli, Italy: EPTCS. https://doi.org/10.4204/EPTCS.96.3","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2012. Interface Simulation Distances. Electronic Proceedings in Theoretical Computer Science. GandALF: Games, Automata, Logic, and Formal Verification vol. 96, 29–42.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface Simulation Distances. In: Electronic Proceedings in Theoretical Computer Science. Vol 96. EPTCS; 2012:29-42. doi:10.4204/EPTCS.96.3","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” In Electronic Proceedings in Theoretical Computer Science, 96:29–42. EPTCS, 2012. https://doi.org/10.4204/EPTCS.96.3.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, 2012, pp. 29–42.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” Electronic Proceedings in Theoretical Computer Science, vol. 96, EPTCS, 2012, pp. 29–42, doi:10.4204/EPTCS.96.3."},"date_published":"2012-10-07T00:00:00Z","ec_funded":1,"publist_id":"3827","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"EPTCS","year":"2012","date_updated":"2023-02-23T10:12:05Z","date_created":"2018-12-11T12:00:19Z","volume":96,"author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","last_name":"Radhakrishna"}],"related_material":{"record":[{"id":"1733","status":"public","relation":"later_version"}]},"month":"10","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"external_id":{"arxiv":["1210.2450"]},"main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"oa":1,"language":[{"iso":"eng"}],"conference":{"location":"Napoli, Italy","start_date":"2012-09-06","end_date":"2012-09-08","name":"GandALF: Games, Automata, Logic, and Formal Verification"},"doi":"10.4204/EPTCS.96.3"},{"scopus_import":1,"day":"01","page":"43 - 52","publication":"roceedings of the tenth ACM international conference on Embedded software","citation":{"apa":"Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2012). Finite automata with time delay blocks. In roceedings of the tenth ACM international conference on Embedded software (pp. 43–52). Tampere, Finland: ACM. https://doi.org/10.1145/2380356.2380370","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Finite automata with time delay blocks,” in roceedings of the tenth ACM international conference on Embedded software, Tampere, Finland, 2012, pp. 43–52.","ista":"Chatterjee K, Henzinger TA, Prabhu V. 2012. Finite automata with time delay blocks. roceedings of the tenth ACM international conference on Embedded software. EMSOFT: Embedded Software , 43–52.","ama":"Chatterjee K, Henzinger TA, Prabhu V. Finite automata with time delay blocks. In: Roceedings of the Tenth ACM International Conference on Embedded Software. ACM; 2012:43-52. doi:10.1145/2380356.2380370","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Finite Automata with Time Delay Blocks.” In Roceedings of the Tenth ACM International Conference on Embedded Software, 43–52. ACM, 2012. https://doi.org/10.1145/2380356.2380370.","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, in:, Roceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 43–52.","mla":"Chatterjee, Krishnendu, et al. “Finite Automata with Time Delay Blocks.” Roceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 43–52, doi:10.1145/2380356.2380370."},"date_published":"2012-10-01T00:00:00Z","type":"conference","abstract":[{"lang":"eng","text":"The notion of delays arises naturally in many computational models, such as, in the design of circuits, control systems, and dataflow languages. In this work, we introduce automata with delay blocks (ADBs), extending finite state automata with variable time delay blocks, for deferring individual transition output symbols, in a discrete-time setting. We show that the ADB languages strictly subsume the regular languages, and are incomparable in expressive power to the context-free languages. We show that ADBs are closed under union, concatenation and Kleene star, and under intersection with regular languages, but not closed under complementation and intersection with other ADB languages. We show that the emptiness and the membership problems are decidable in polynomial time for ADBs, whereas the universality problem is undecidable. Finally we consider the linear-time model checking problem, i.e., whether the language of an ADB is contained in a regular language, and show that the model checking problem is PSPACE-complete. Copyright 2012 ACM."}],"title":"Finite automata with time delay blocks","status":"public","_id":"2936","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","month":"10","quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1207.7019"}],"language":[{"iso":"eng"}],"conference":{"name":"EMSOFT: Embedded Software ","end_date":"2012-10-12","location":"Tampere, Finland","start_date":"2012-10-07"},"doi":"10.1145/2380356.2380370","publist_id":"3799","ec_funded":1,"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"ACM","acknowledgement":"This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOPTILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); Microsoft faculty fellows award; ERC Advanced grant QUAREM; and FWF Grant No S11403-N23 (RiSE).","year":"2012","date_updated":"2021-01-12T07:39:53Z","date_created":"2018-12-11T12:00:26Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Vinayak","last_name":"Prabhu","full_name":"Prabhu, Vinayak"}]},{"publist_id":"3791","ec_funded":1,"date_created":"2018-12-11T12:00:28Z","date_updated":"2021-01-12T07:39:56Z","volume":7539,"author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Nickovic","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2012","acknowledgement":"ERC Advanced Grant QUAREM (Quantitative Reactive Modeling), FWF National Research Network RISE (Rigorous Systems Engineering)","month":"09","language":[{"iso":"eng"}],"conference":{"name":"Monterey Workshop 2012","end_date":"2012-03-21","location":"Oxford, UK","start_date":"2012-03-19"},"doi":"10.1007/978-3-642-34059-8_20","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"abstract":[{"text":"Interface theories provide a formal framework for component-based development of software and hardware which supports the incremental design of systems and the independent implementability of components. These capabilities are ensured through mathematical properties of the parallel composition operator and the refinement relation for components. More recently, a conjunction operation was added to interface theories in order to provide support for handling multiple viewpoints, requirements engineering, and component reuse. Unfortunately, the conjunction operator does not allow independent implementability in general. In this paper, we study conditions that need to be imposed on interface models in order to enforce independent implementability with respect to conjunction. We focus on multiple viewpoint specifications and propose a new compatibility criterion between two interfaces, which we call orthogonality. We show that orthogonal interfaces can be refined separately, while preserving both orthogonality and composability with other interfaces. We illustrate the independent implementability of different viewpoints with a FIFO buffer example.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","oa_version":"None","status":"public","title":"Independent implementability of viewpoints","intvolume":" 7539","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"2942","day":"16","scopus_import":1,"date_published":"2012-09-16T00:00:00Z","page":"380 - 395","publication":" Conference proceedings Monterey Workshop 2012","citation":{"ama":"Henzinger TA, Nickovic D. Independent implementability of viewpoints. In: Conference Proceedings Monterey Workshop 2012. Vol 7539. Springer; 2012:380-395. doi:10.1007/978-3-642-34059-8_20","apa":"Henzinger, T. A., & Nickovic, D. (2012). Independent implementability of viewpoints. In Conference proceedings Monterey Workshop 2012 (Vol. 7539, pp. 380–395). Oxford, UK: Springer. https://doi.org/10.1007/978-3-642-34059-8_20","ieee":"T. A. Henzinger and D. Nickovic, “Independent implementability of viewpoints,” in Conference proceedings Monterey Workshop 2012, Oxford, UK, 2012, vol. 7539, pp. 380–395.","ista":"Henzinger TA, Nickovic D. 2012. Independent implementability of viewpoints. Conference proceedings Monterey Workshop 2012. Monterey Workshop 2012, LNCS, vol. 7539, 380–395.","short":"T.A. Henzinger, D. Nickovic, in:, Conference Proceedings Monterey Workshop 2012, Springer, 2012, pp. 380–395.","mla":"Henzinger, Thomas A., and Dejan Nickovic. “Independent Implementability of Viewpoints.” Conference Proceedings Monterey Workshop 2012, vol. 7539, Springer, 2012, pp. 380–95, doi:10.1007/978-3-642-34059-8_20.","chicago":"Henzinger, Thomas A, and Dejan Nickovic. “Independent Implementability of Viewpoints.” In Conference Proceedings Monterey Workshop 2012, 7539:380–95. Springer, 2012. https://doi.org/10.1007/978-3-642-34059-8_20."}},{"scopus_import":1,"month":"07","day":"01","citation":{"short":"C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer, 2012, pp. 294–309.","mla":"Guet, Calin C., et al. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits. Vol. 7358, Springer, 2012, pp. 294–309, doi:10.1007/978-3-642-31424-7_24.","chicago":"Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,” 7358:294–309. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_24.","ama":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309. doi:10.1007/978-3-642-31424-7_24","ieee":"C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed continuous time Markov chains for genetic regulatory circuits,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.","apa":"Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., & Sezgin, A. (2012). Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358, pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_24","ista":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification, LNCS, vol. 7358, 294–309."},"quality_controlled":"1","page":"294 - 309","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"conference":{"location":"Berkeley, CA, USA","start_date":"2012-07-07","end_date":"2012-07-13","name":"CAV: Computer Aided Verification"},"doi":"10.1007/978-3-642-31424-7_24","date_published":"2012-07-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event's initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag.","lang":"eng"}],"ec_funded":1,"publist_id":"3561","year":"2012","_id":"3136","acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","title":"Delayed continuous time Markov chains for genetic regulatory circuits","publication_status":"published","status":"public","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"publisher":"Springer","author":[{"orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","first_name":"Calin C","full_name":"Guet, Calin C"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"id":"3B43276C-F248-11E8-B48F-1D18A9856A87","last_name":"Mateescu","first_name":"Maria","full_name":"Mateescu, Maria"},{"full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","last_name":"Sezgin","first_name":"Ali"}],"date_updated":"2021-01-12T07:41:18Z","date_created":"2018-12-11T12:01:36Z","volume":"7358 ","oa_version":"None"},{"file_date_updated":"2020-07-14T12:46:01Z","publist_id":"3525","year":"2012","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","author":[{"full_name":"Asarin, Eugene","last_name":"Asarin","first_name":"Eugene"},{"last_name":"Donzé","first_name":"Alexandre","full_name":"Donzé, Alexandre"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"date_updated":"2021-01-12T07:41:29Z","date_created":"2018-12-11T12:01:45Z","volume":7186,"month":"01","oa":1,"quality_controlled":"1","conference":{"end_date":"2011-09-30","location":"San Francisco, CA, United States","start_date":"2011-09-27","name":"RV: Runtime Verification"},"doi":"10.1007/978-3-642-29860-8_12","language":[{"iso":"eng"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"Given a dense-time real-valued signal and a parameterized temporal logic formula with both magnitude and timing parameters, we compute the subset of the parameter space that renders the formula satisfied by the trace. We provide two preliminary implementations, one which follows the exact semantics and attempts to compute the validity domain by quantifier elimination in linear arithmetics and one which conducts adaptive search in the parameter space.","lang":"eng"}],"_id":"3162","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Parametric identification of temporal properties","ddc":["000"],"status":"public","intvolume":" 7186","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"2012_RV_Asarin.pdf","content_type":"application/pdf","file_size":374726,"creator":"dernst","relation":"main_file","file_id":"7862","checksum":"ba4a75287008fc64b8fbf78a7476ec32","date_updated":"2020-07-14T12:46:01Z","date_created":"2020-05-15T12:50:15Z"}],"scopus_import":1,"day":"01","article_processing_charge":"No","has_accepted_license":"1","citation":{"ama":"Asarin E, Donzé A, Maler O, Nickovic D. Parametric identification of temporal properties. In: Vol 7186. Springer; 2012:147-160. doi:10.1007/978-3-642-29860-8_12","ista":"Asarin E, Donzé A, Maler O, Nickovic D. 2012. Parametric identification of temporal properties. RV: Runtime Verification, LNCS, vol. 7186, 147–160.","ieee":"E. Asarin, A. Donzé, O. Maler, and D. Nickovic, “Parametric identification of temporal properties,” presented at the RV: Runtime Verification, San Francisco, CA, United States, 2012, vol. 7186, pp. 147–160.","apa":"Asarin, E., Donzé, A., Maler, O., & Nickovic, D. (2012). Parametric identification of temporal properties (Vol. 7186, pp. 147–160). Presented at the RV: Runtime Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-642-29860-8_12","mla":"Asarin, Eugene, et al. Parametric Identification of Temporal Properties. Vol. 7186, Springer, 2012, pp. 147–60, doi:10.1007/978-3-642-29860-8_12.","short":"E. Asarin, A. Donzé, O. Maler, D. Nickovic, in:, Springer, 2012, pp. 147–160.","chicago":"Asarin, Eugene, Alexandre Donzé, Oded Maler, and Dejan Nickovic. “Parametric Identification of Temporal Properties,” 7186:147–60. Springer, 2012. https://doi.org/10.1007/978-3-642-29860-8_12."},"page":"147 - 160","date_published":"2012-01-01T00:00:00Z"},{"_id":"3253","acknowledgement":"This work was partly supported by the French National Research Agency (ANR) project Veridyc (ANR-09-SEGI-016).","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","year":"2012","status":"public","title":"Abstract domains for automated reasoning about list manipulating programs with infinite data","publication_status":"published","department":[{"_id":"ToHe"}],"intvolume":" 7148","publisher":"Springer","author":[{"full_name":"Bouajjani, Ahmed","last_name":"Bouajjani","first_name":"Ahmed"},{"full_name":"Dragoi, Cezara","first_name":"Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Enea, Constantin","last_name":"Enea","first_name":"Constantin"},{"full_name":"Sighireanu, Mihaela","last_name":"Sighireanu","first_name":"Mihaela"}],"date_created":"2018-12-11T12:02:17Z","date_updated":"2021-01-12T07:42:09Z","volume":7148,"oa_version":"None","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs."}],"publist_id":"3404","citation":{"mla":"Bouajjani, Ahmed, et al. Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data. Vol. 7148, Springer, 2012, pp. 1–22, doi:10.1007/978-3-642-27940-9_1.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp. 1–22.","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data,” 7148:1–22. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_1.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer; 2012:1-22. doi:10.1007/978-3-642-27940-9_1","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated reasoning about list manipulating programs with infinite data. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.","apa":"Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Abstract domains for automated reasoning about list manipulating programs with infinite data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_1","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for automated reasoning about list manipulating programs with infinite data,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 1–22."},"quality_controlled":"1","page":"1 - 22","conference":{"end_date":"2012-01-24","location":"Philadelphia, PA, USA","start_date":"2012-01-22","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"date_published":"2012-02-26T00:00:00Z","doi":"10.1007/978-3-642-27940-9_1","language":[{"iso":"eng"}],"month":"02","day":"26"},{"abstract":[{"lang":"eng","text":"The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk."}],"publist_id":"3515","type":"journal_article","date_created":"2018-12-11T12:01:47Z","date_updated":"2023-02-23T11:39:40Z","volume":431,"oa_version":"None","author":[{"last_name":"Feret","first_name":"Jérôme","full_name":"Feret, Jérôme"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Heinz","last_name":"Koeppl","full_name":"Koeppl, Heinz"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","first_name":"Tatjana","last_name":"Petrov","full_name":"Petrov, Tatjana"}],"pubrep_id":"73","related_material":{"record":[{"id":"3719","status":"public","relation":"earlier_version"}]},"status":"public","publication_status":"published","title":"Lumpability abstractions of rule based systems","intvolume":" 431","publisher":"Elsevier","department":[{"_id":"ToHe"}],"_id":"3168","year":"2012","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","acknowledgement":"We would like to thank the anonymous reviewers for their comments on the different versions of the paper. We would also like to thank Ferdinanda Camporesi for her careful reading and the useful insights that she gave us about the paper.\r\nJérôme Feret’s contribution was partially supported by the AbstractCell ANR-Chair of Excellence. Heinz Koeppl’s research is supported by the Swiss National Science Foundation, grant no. 200020-117975/1. Tatjana Petrov’s research is supported by SystemsX.ch (the Swiss Initiative in Systems Biology).","day":"04","month":"05","scopus_import":1,"language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2011.12.059","date_published":"2012-05-04T00:00:00Z","quality_controlled":"1","page":"137 - 164","publication":"Theoretical Computer Science","citation":{"mla":"Feret, Jérôme, et al. “Lumpability Abstractions of Rule Based Systems.” Theoretical Computer Science, vol. 431, Elsevier, 2012, pp. 137–64, doi:10.1016/j.tcs.2011.12.059.","short":"J. Feret, T.A. Henzinger, H. Koeppl, T. Petrov, Theoretical Computer Science 431 (2012) 137–164.","chicago":"Feret, Jérôme, Thomas A Henzinger, Heinz Koeppl, and Tatjana Petrov. “Lumpability Abstractions of Rule Based Systems.” Theoretical Computer Science. Elsevier, 2012. https://doi.org/10.1016/j.tcs.2011.12.059.","ama":"Feret J, Henzinger TA, Koeppl H, Petrov T. Lumpability abstractions of rule based systems. Theoretical Computer Science. 2012;431:137-164. doi:10.1016/j.tcs.2011.12.059","ista":"Feret J, Henzinger TA, Koeppl H, Petrov T. 2012. Lumpability abstractions of rule based systems. Theoretical Computer Science. 431, 137–164.","ieee":"J. Feret, T. A. Henzinger, H. Koeppl, and T. Petrov, “Lumpability abstractions of rule based systems,” Theoretical Computer Science, vol. 431. Elsevier, pp. 137–164, 2012.","apa":"Feret, J., Henzinger, T. A., Koeppl, H., & Petrov, T. (2012). Lumpability abstractions of rule based systems. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2011.12.059"}},{"publist_id":"2341","file_date_updated":"2020-07-14T12:46:17Z","volume":78,"date_created":"2018-12-11T12:05:29Z","date_updated":"2022-05-24T08:00:54Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"publisher":"Elsevier","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","year":"2012","acknowledgement":"This research was supported in part by the ONR grant N00014-02-1-0671, by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610.","month":"03","language":[{"iso":"eng"}],"doi":"10.1016/j.jcss.2011.05.002","quality_controlled":"1","oa":1,"main_file_link":[{"url":"https://doi.org/10.1016/j.jcss.2011.05.002","open_access":"1"}],"issue":"2","abstract":[{"lang":"eng","text":"We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications."}],"type":"journal_article","file":[{"file_name":"a_survey_of_stochastic_omega-regular_games.pdf","access_level":"open_access","file_size":336450,"content_type":"application/pdf","creator":"kschuh","relation":"main_file","file_id":"5897","date_updated":"2020-07-14T12:46:17Z","date_created":"2019-01-29T10:54:28Z","checksum":"241b939deb4517cdd4426d49c67e3fa2"}],"oa_version":"Submitted Version","intvolume":" 78","status":"public","title":"A survey of stochastic ω regular games","ddc":["000"],"_id":"3846","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","article_processing_charge":"No","day":"02","scopus_import":"1","date_published":"2012-03-02T00:00:00Z","page":"394 - 413","article_type":"original","citation":{"apa":"Chatterjee, K., & Henzinger, T. A. (2012). A survey of stochastic ω regular games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2011.05.002","ieee":"K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,” Journal of Computer and System Sciences, vol. 78, no. 2. Elsevier, pp. 394–413, 2012.","ista":"Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 78(2), 394–413.","ama":"Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 2012;78(2):394-413. doi:10.1016/j.jcss.2011.05.002","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic ω Regular Games.” Journal of Computer and System Sciences. Elsevier, 2012. https://doi.org/10.1016/j.jcss.2011.05.002.","short":"K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78 (2012) 394–413.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω Regular Games.” Journal of Computer and System Sciences, vol. 78, no. 2, Elsevier, 2012, pp. 394–413, doi:10.1016/j.jcss.2011.05.002."},"publication":"Journal of Computer and System Sciences"},{"scopus_import":1,"has_accepted_license":"1","day":"01","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design. Springer, 2012. https://doi.org/10.1007/s10703-012-0164-2.","mla":"Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design, vol. 43, no. 2, Springer, 2012, pp. 268–84, doi:10.1007/s10703-012-0164-2.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 43(2), 268–284.","apa":"Chatterjee, K., Doyen, L., & Henzinger, T. A. (2012). A survey of partial-observation stochastic parity games. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0164-2","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation stochastic parity games,” Formal Methods in System Design, vol. 43, no. 2. Springer, pp. 268–284, 2012.","ama":"Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 2012;43(2):268-284. doi:10.1007/s10703-012-0164-2"},"publication":"Formal Methods in System Design","page":"268 - 284","date_published":"2012-10-01T00:00:00Z","type":"journal_article","issue":"2","abstract":[{"text":"We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational). ","lang":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"3128","intvolume":" 43","title":"A survey of partial-observation stochastic parity games","status":"public","ddc":["005"],"pubrep_id":"303","oa_version":"Submitted Version","file":[{"file_id":"4882","relation":"main_file","date_updated":"2020-07-14T12:46:00Z","date_created":"2018-12-12T10:11:27Z","checksum":"dd3d590f383bb2ac6cfda1489ac1c42a","file_name":"IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf","access_level":"open_access","creator":"system","file_size":163983,"content_type":"application/pdf"}],"month":"10","oa":1,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1007/s10703-012-0164-2","language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"3570","file_date_updated":"2020-07-14T12:46:00Z","year":"2012","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"volume":43,"date_updated":"2021-01-12T07:41:15Z","date_created":"2018-12-11T12:01:33Z"},{"conference":{"end_date":"2012-06-16","start_date":"2012-06-13","location":"Stockholm, Sweden","name":"FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems "},"doi":"10.1007/978-3-642-30793-5_13","language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","month":"06","author":[{"full_name":"Delahaye, Benoît","first_name":"Benoît","last_name":"Delahaye"},{"full_name":"Fahrenberg, Uli","first_name":"Uli","last_name":"Fahrenberg"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Legay","first_name":"Axel","full_name":"Legay, Axel"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"date_created":"2018-12-11T12:01:43Z","date_updated":"2021-01-12T07:41:26Z","volume":7273,"acknowledgement":"Research partially supported by the Danish-Chinese Center for Cyber Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.","year":"2012","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:01Z","publist_id":"3539","date_published":"2012-06-01T00:00:00Z","citation":{"ama":"Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218. doi:10.1007/978-3-642-30793-5_13","ieee":"B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous interface theories and time triggered scheduling,” presented at the FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273, pp. 203–218.","apa":"Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., & Nickovic, D. (2012). Synchronous interface theories and time triggered scheduling (Vol. 7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden: Springer. https://doi.org/10.1007/978-3-642-30793-5_13","ista":"Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous interface theories and time triggered scheduling. FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , LNCS, vol. 7273, 203–218.","short":"B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer, 2012, pp. 203–218.","mla":"Delahaye, Benoît, et al. Synchronous Interface Theories and Time Triggered Scheduling. Vol. 7273, Springer, 2012, pp. 203–18, doi:10.1007/978-3-642-30793-5_13.","chicago":"Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18. Springer, 2012. https://doi.org/10.1007/978-3-642-30793-5_13."},"page":"203 - 218","day":"01","has_accepted_license":"1","scopus_import":1,"pubrep_id":"88","oa_version":"Submitted Version","file":[{"relation":"main_file","file_id":"4879","date_created":"2018-12-12T10:11:25Z","date_updated":"2020-07-14T12:46:01Z","checksum":"feae2e07f2d9a59843f8ddabf25d179f","file_name":"IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf","access_level":"open_access","file_size":493198,"content_type":"application/pdf","creator":"system"}],"_id":"3155","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","title":"Synchronous interface theories and time triggered scheduling","status":"public","ddc":["004"],"intvolume":" 7273","abstract":[{"text":"We propose synchronous interfaces, a new interface theory for discrete-time systems. We use an application to time-triggered scheduling to drive the design choices for our formalism; in particular, additionally to deriving useful mathematical properties, we focus on providing a syntax which is adapted to natural high-level system modeling. As a result, we develop an interface model that relies on a guarded-command based language and is equipped with shared variables and explicit discrete-time clocks. We define all standard interface operations: compatibility checking, composition, refinement, and shared refinement. Apart from the synchronous interface model, the contribution of this paper is the establishment of a formal relation between interface theories and real-time scheduling, where we demonstrate a fully automatic framework for the incremental computation of time-triggered schedules.","lang":"eng"}],"type":"conference","alternative_title":["LNCS"]},{"scopus_import":1,"month":"02","day":"01","citation":{"chicago":"Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming. Elsevier, 2012. https://doi.org/10.1016/j.scico.2010.06.004.","mla":"Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming, vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:10.1016/j.scico.2010.06.004.","short":"A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli, Science of Computer Programming 77 (2012) 96–112.","ista":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 77(2), 96–112.","apa":"Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., & Sangiovanni Vincentelli, A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. Elsevier. https://doi.org/10.1016/j.scico.2010.06.004","ieee":"A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli, “Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code,” Science of Computer Programming, vol. 77, no. 2. Elsevier, pp. 96–112, 2012.","ama":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 2012;77(2):96-112. doi:10.1016/j.scico.2010.06.004"},"publication":"Science of Computer Programming","page":"96 - 112","quality_controlled":"1","doi":"10.1016/j.scico.2010.06.004","date_published":"2012-02-01T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","issue":"2","publist_id":"2370","abstract":[{"lang":"eng","text":"Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order."}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"3836","year":"2012","intvolume":" 77","publisher":"Elsevier","department":[{"_id":"ToHe"}],"publication_status":"published","status":"public","title":"Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code","author":[{"first_name":"Arkadeb","last_name":"Ghosal","full_name":"Ghosal, Arkadeb"},{"first_name":"Daniel","last_name":"Iercan","full_name":"Iercan, Daniel"},{"full_name":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Alberto","last_name":"Sangiovanni Vincentelli","full_name":"Sangiovanni Vincentelli, Alberto"}],"oa_version":"None","volume":77,"date_created":"2018-12-11T12:05:26Z","date_updated":"2021-01-12T07:52:32Z"},{"type":"journal_article","abstract":[{"lang":"eng","text":"For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) PSPACE-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words."}],"issue":"3","_id":"2967","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Algorithmic analysis of array-accessing programs","intvolume":" 13","oa_version":"None","scopus_import":1,"day":"01","publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"ieee":"R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3. ACM, 2012.","apa":"Alur, R., Cerny, P., & Weinstein, S. (2012). Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2287718.2287727","ista":"Alur R, Cerny P, Weinstein S. 2012. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 13(3), 27.","ama":"Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 2012;13(3). doi:10.1145/2287718.2287727","chicago":"Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL). ACM, 2012. https://doi.org/10.1145/2287718.2287727.","short":"R. Alur, P. Cerny, S. Weinstein, ACM Transactions on Computational Logic (TOCL) 13 (2012).","mla":"Alur, Rajeev, et al. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3, 27, ACM, 2012, doi:10.1145/2287718.2287727."},"date_published":"2012-08-01T00:00:00Z","article_number":"27","ec_funded":1,"publist_id":"3748","year":"2012","acknowledgement":"This research was supported in part by the NSF Cybertrust award CNS 0524059, by the European Research Council (ERC) Advanced Investigator Grant QUAREM, and by the Austrian Science Fund (FWF) project S11402-N23.","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"ACM","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Scott","last_name":"Weinstein","full_name":"Weinstein, Scott"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"4403"}]},"date_created":"2018-12-11T12:00:36Z","date_updated":"2023-02-23T12:09:43Z","volume":13,"month":"08","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"doi":"10.1145/2287718.2287727","language":[{"iso":"eng"}]},{"publication":"ACM Transactions on Computational Logic (TOCL)","citation":{"chicago":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL). ACM, 2012. https://doi.org/10.1145/2362355.2362357.","short":"U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13 (2012).","mla":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4, 29, ACM, 2012, doi:10.1145/2362355.2362357.","ieee":"U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and useful,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4. ACM, 2012.","apa":"Boker, U., & Kupferman, O. (2012). Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2362355.2362357","ista":"Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29.","ama":"Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 2012;13(4). doi:10.1145/2362355.2362357"},"quality_controlled":"1","date_published":"2012-10-01T00:00:00Z","doi":"10.1145/2362355.2362357","language":[{"iso":"eng"}],"scopus_import":1,"day":"01","month":"10","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"494","year":"2012","status":"public","publication_status":"published","title":"Translating to Co-Büchi made tight, unified, and useful","publisher":"ACM","intvolume":" 13","department":[{"_id":"ToHe"}],"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"date_updated":"2021-01-12T08:01:03Z","date_created":"2018-12-11T11:46:47Z","volume":13,"oa_version":"None","article_number":"29","type":"journal_article","abstract":[{"text":"We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata.","lang":"eng"}],"publist_id":"7326","issue":"4"},{"month":"01","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7"},{"name":"Design for Embedded Systems","call_identifier":"FP7","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"doi":"10.1016/j.tcs.2011.08.002","language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"3408","year":"2012","acknowledgement":"This work was partially supported by the ERC Advanced Grant QUAREM, the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the European Network of Excellence Artist Design.","publication_status":"published","publisher":"Elsevier","department":[{"_id":"ToHe"}],"author":[{"last_name":"Cerny","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"4393"},{"relation":"earlier_version","status":"public","id":"5389"}]},"date_created":"2018-12-11T12:02:15Z","date_updated":"2023-02-23T12:24:04Z","volume":413,"scopus_import":1,"day":"06","publication":"Theoretical Computer Science","citation":{"chicago":"Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.” Theoretical Computer Science. Elsevier, 2012. https://doi.org/10.1016/j.tcs.2011.08.002.","mla":"Cerny, Pavol, et al. “Simulation Distances.” Theoretical Computer Science, vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:10.1016/j.tcs.2011.08.002.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413 (2012) 21–35.","ista":"Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical Computer Science. 413(1), 21–35.","apa":"Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2012). Simulation distances. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2011.08.002","ieee":"P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” Theoretical Computer Science, vol. 413, no. 1. Elsevier, pp. 21–35, 2012.","ama":"Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. Theoretical Computer Science. 2012;413(1):21-35. doi:10.1016/j.tcs.2011.08.002"},"page":"21 - 35","date_published":"2012-01-06T00:00:00Z","type":"journal_article","abstract":[{"text":"Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.","lang":"eng"}],"issue":"1","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"3249","status":"public","title":"Simulation distances","intvolume":" 413","pubrep_id":"42","oa_version":"None"},{"author":[{"last_name":"Bouajjani","first_name":"Ahmed","full_name":"Bouajjani, Ahmed"},{"full_name":"Dragoi, Cezara","first_name":"Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Enea","first_name":"Constantin","full_name":"Enea, Constantin"},{"first_name":"Mihaela","last_name":"Sighireanu","full_name":"Sighireanu, Mihaela"}],"date_updated":"2023-09-05T14:07:24Z","date_created":"2022-03-21T07:58:39Z","volume":7561,"year":"2012","acknowledgement":"This work has been partially supported by the French ANR project Veridyc","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"place":"Berlin, Heidelberg","conference":{"end_date":"2012-10-06","location":"Thiruvananthapuram, India","start_date":"2012-10-03","name":"ATVA: Automated Technology for Verification and Analysis"},"doi":"10.1007/978-3-642-33386-6_14","language":[{"iso":"eng"}],"quality_controlled":"1","month":"10","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642333866"],"eissn":["1611-3349"],"isbn":["9783642333859"]},"oa_version":"None","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"10903","title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","status":"public","intvolume":" 7561","abstract":[{"text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.","lang":"eng"}],"type":"conference","alternative_title":["LNCS"],"date_published":"2012-10-15T00:00:00Z","publication":"Automated Technology for Verification and Analysis","citation":{"ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182.","apa":"Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:10.1007/978-3-642-33386-6_14","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In Automated Technology for Verification and Analysis, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” Automated Technology for Verification and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182."},"page":"167-182","day":"15","article_processing_charge":"No","scopus_import":"1","series_title":"LNCS"},{"alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}],"intvolume":" 7214","title":"HSF(C): A software verifier based on Horn clauses","status":"public","_id":"10906","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Published Version","series_title":"LNCS","scopus_import":"1","article_processing_charge":"No","day":"01","page":"549-551","citation":{"ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46","ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46."},"publication":"Tools and Algorithms for the Construction and Analysis of Systems","date_published":"2012-04-01T00:00:00Z","place":"Berlin, Heidelberg","editor":[{"first_name":"Cormac","last_name":"Flanagan","full_name":"Flanagan, Cormac"},{"full_name":"König, Barbara","first_name":"Barbara","last_name":"König"}],"publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2012","volume":7214,"date_updated":"2023-09-05T14:09:54Z","date_created":"2022-03-21T08:03:30Z","author":[{"last_name":"Grebenshchikov","first_name":"Sergey","full_name":"Grebenshchikov, Sergey"},{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lopes, Nuno P.","first_name":"Nuno P.","last_name":"Lopes"},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"}],"publication_identifier":{"isbn":["9783642287558"],"eissn":["1611-3349"],"eisbn":["9783642287565"],"issn":["0302-9743"]},"month":"04","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-28756-5_46","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2012-03-24","location":"Tallinn, Estonia","end_date":"2012-04-01"}},{"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642333859","9783642333866"],"issn":["0302-9743"]},"quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"oa":1,"language":[{"iso":"eng"}],"conference":{"start_date":"2012-10-03","location":"Thiruvananthapuram, Kerala, India","end_date":"2012-10-06","name":"ATVA 2012"},"doi":"10.1007/978-3-642-33386-6_10","place":"Berlin, Heidelberg","file_date_updated":"2020-07-14T12:47:10Z","ec_funded":1,"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer Berlin Heidelberg","year":"2012","date_updated":"2023-09-05T14:15:29Z","date_created":"2018-12-18T13:01:46Z","volume":7561,"author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"}],"series_title":"LNCS","has_accepted_license":"1","article_processing_charge":"No","page":"107-121","publication":"Automated Technology for Verification and Analysis","citation":{"ista":"Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.","apa":"Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_10","ieee":"A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in Automated Technology for Verification and Analysis, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.","ama":"Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:10.1007/978-3-642-33386-6_10","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In Automated Technology for Verification and Analysis, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” Automated Technology for Verification and Analysis, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10.","short":"A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121."},"date_published":"2012-01-01T00:00:00Z","type":"book_chapter","ddc":["005"],"status":"public","title":"Improved Single Pass Algorithms for Resolution Proof Reduction","intvolume":" 7561","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"5745","file":[{"checksum":"68415837a315de3cc4d120f6019d752c","date_updated":"2020-07-14T12:47:10Z","date_created":"2018-12-18T13:07:35Z","relation":"main_file","file_id":"5746","file_size":465502,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2012_ATVA_Gupta.pdf"}],"oa_version":"None","pubrep_id":"180"},{"citation":{"ama":"Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition systems. In: Vol 7148. Springer; 2012:445-460. doi:10.1007/978-3-642-27940-9_29","apa":"Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29","ieee":"D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured transition systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460.","ista":"Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.","short":"D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.","mla":"Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.","chicago":"Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_29."},"page":"445 - 460","date_published":"2012-01-01T00:00:00Z","day":"01","has_accepted_license":"1","_id":"3251","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","ddc":["000","005"],"title":"Ideal abstractions for well structured transition systems","intvolume":" 7148","pubrep_id":"100","file":[{"access_level":"open_access","file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","content_type":"application/pdf","file_size":217104,"creator":"system","relation":"main_file","file_id":"4759","checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","date_created":"2018-12-12T10:09:35Z","date_updated":"2020-07-14T12:46:05Z"}],"oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system.","lang":"eng"}],"oa":1,"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2012-01-24","location":"Philadelphia, PA, USA","start_date":"2012-01-22"},"doi":"10.1007/978-3-642-27940-9_29","language":[{"iso":"eng"}],"month":"01","acknowledgement":"This research was supported in part by the European Research Council (ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF) project S11402-N23.","year":"2012","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"author":[{"full_name":"Zufferey, Damien","last_name":"Zufferey","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"1405","relation":"dissertation_contains","status":"public"}]},"date_updated":"2023-09-07T11:36:36Z","date_created":"2018-12-11T12:02:16Z","volume":7148,"file_date_updated":"2020-07-14T12:46:05Z","publist_id":"3406","ec_funded":1},{"day":"05","month":"12","language":[{"iso":"eng"}],"conference":{"location":"Kenting, Taiwan","start_date":"2011-12-05","end_date":"2011-12-07","name":"APLAS: Asian Symposium on Programming Languages and Systems"},"date_published":"2011-12-05T00:00:00Z","doi":"10.1007/978-3-642-25318-8_16","quality_controlled":"1","page":"188 - 203","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"citation":{"ama":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:10.1007/978-3-642-25318-8_16","ista":"Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS, vol. 7078, 188–203.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2011). Solving recursion-free Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan: Springer. https://doi.org/10.1007/978-3-642-25318-8_16","mla":"Gupta, Ashutosh, et al. Solving Recursion-Free Horn Clauses over LI+UIF. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:10.1007/978-3-642-25318-8_16.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011. https://doi.org/10.1007/978-3-642-25318-8_16."},"abstract":[{"text":"Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.","lang":"eng"}],"ec_funded":1,"publist_id":"3383","alternative_title":["LNCS"],"type":"conference","date_updated":"2021-01-12T07:42:15Z","date_created":"2018-12-11T12:02:20Z","volume":7078,"oa_version":"None","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"full_name":"Popeea, Corneliu","first_name":"Corneliu","last_name":"Popeea"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"publication_status":"published","title":"Solving recursion-free Horn clauses over LI+UIF","status":"public","publisher":"Springer","intvolume":" 7078","editor":[{"full_name":"Yang, Hongseok","first_name":"Hongseok","last_name":"Yang"}],"department":[{"_id":"ToHe"}],"_id":"3264","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","year":"2011"},{"has_accepted_license":"1","month":"06","day":"14","language":[{"iso":"eng"}],"date_published":"2011-06-14T00:00:00Z","conference":{"start_date":"2011-06-14","end_date":"2011-06-15","name":"HotCloud: Workshop on Hot Topics in Cloud Computing"},"page":"1 - 6","quality_controlled":"1","oa":1,"citation":{"ieee":"T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, 2011, pp. 1–6.","apa":"Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.","ista":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.","ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.","chicago":"Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011.","short":"T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.","mla":"Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6."},"publist_id":"3338","abstract":[{"lang":"eng","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."}],"file_date_updated":"2020-07-14T12:46:06Z","type":"conference","file":[{"content_type":"application/pdf","file_size":232770,"creator":"system","file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:06Z","date_created":"2018-12-12T10:18:14Z","checksum":"21a461ac004bb535c83320fe79b30375","relation":"main_file","file_id":"5333"}],"oa_version":"Submitted Version","date_updated":"2021-01-12T07:42:31Z","date_created":"2018-12-11T12:02:33Z","pubrep_id":"90","author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Anmol","last_name":"Singh","id":"72A86902-E99F-11E9-9F62-915534D1B916","full_name":"Singh, Anmol"},{"id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh","first_name":"Vasu","full_name":"Singh, Vasu"},{"full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Wies"},{"full_name":"Zufferey, Damien","last_name":"Zufferey","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"department":[{"_id":"ToHe"}],"publisher":"USENIX","ddc":["000","005"],"title":"Static scheduling in clouds","publication_status":"published","status":"public","_id":"3302","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2011"},{"conference":{"name":"WCSB: Workshop on Computational Systems Biology (TICSP)"},"date_published":"2011-01-01T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"ista":"Henzinger TA, Mateescu M. 2011. Tail approximation for the chemical master equation. WCSB: Workshop on Computational Systems Biology (TICSP).","apa":"Henzinger, T. A., & Mateescu, M. (2011). Tail approximation for the chemical master equation. Presented at the WCSB: Workshop on Computational Systems Biology (TICSP), Tampere International Center for Signal Processing.","ieee":"T. A. Henzinger and M. Mateescu, “Tail approximation for the chemical master equation,” presented at the WCSB: Workshop on Computational Systems Biology (TICSP), 2011.","ama":"Henzinger TA, Mateescu M. Tail approximation for the chemical master equation. In: Tampere International Center for Signal Processing; 2011.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Tail Approximation for the Chemical Master Equation.” Tampere International Center for Signal Processing, 2011.","mla":"Henzinger, Thomas A., and Maria Mateescu. Tail Approximation for the Chemical Master Equation. Tampere International Center for Signal Processing, 2011.","short":"T.A. Henzinger, M. Mateescu, in:, Tampere International Center for Signal Processing, 2011."},"quality_controlled":"1","month":"01","day":"01","has_accepted_license":"1","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Mateescu, Maria","last_name":"Mateescu","first_name":"Maria"}],"pubrep_id":"91","date_created":"2018-12-11T12:02:33Z","date_updated":"2021-01-12T07:42:30Z","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2012-91-v1+1_Tail_approximation_for_the_chemical_master_equation.pdf","creator":"system","content_type":"application/pdf","file_size":240820,"file_id":"5331","relation":"main_file","checksum":"aa4d7a832a5419e6c0090650ebff2b9a","date_created":"2018-12-12T10:18:12Z","date_updated":"2020-07-14T12:46:06Z"}],"year":"2011","_id":"3301","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","ddc":["005","570"],"title":"Tail approximation for the chemical master equation","publisher":"Tampere International Center for Signal Processing","department":[{"_id":"ToHe"}],"abstract":[{"text":"The chemical master equation is a differential equation describing the time evolution of the probability distribution over the possible “states” of a biochemical system. The solution of this equation is of interest within the systems biology field ever since the importance of the molec- ular noise has been acknowledged. Unfortunately, most of the systems do not have analytical solutions, and numerical solutions suffer from the course of dimensionality and therefore need to be approximated. Here, we introduce the concept of tail approximation, which retrieves an approximation of the probabilities in the tail of a distribution from the total probability of the tail and its conditional expectation. This approximation method can then be used to numerically compute the solution of the chemical master equation on a subset of the state space, thus fighting the explosion of the state space, for which this problem is renowned.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:06Z","publist_id":"3339","type":"conference"},{"doi":"10.1145/2037509.2037510","conference":{"end_date":"2011-09-23","location":"Paris, France","start_date":"2011-09-21","name":"CMSB: Computational Methods in Systems Biology"},"language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","month":"09","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Mateescu, Maria","last_name":"Mateescu","first_name":"Maria"}],"date_created":"2018-12-11T12:02:32Z","date_updated":"2021-01-12T07:42:29Z","year":"2011","publisher":"Springer","department":[{"_id":"ToHe"}],"publication_status":"published","publist_id":"3341","file_date_updated":"2020-07-14T12:46:06Z","date_published":"2011-09-21T00:00:00Z","citation":{"chicago":"Henzinger, Thomas A, and Maria Mateescu. “Propagation Models for Computing Biochemical Reaction Networks,” 1–3. Springer, 2011. https://doi.org/10.1145/2037509.2037510.","short":"T.A. Henzinger, M. Mateescu, in:, Springer, 2011, pp. 1–3.","mla":"Henzinger, Thomas A., and Maria Mateescu. Propagation Models for Computing Biochemical Reaction Networks. Springer, 2011, pp. 1–3, doi:10.1145/2037509.2037510.","apa":"Henzinger, T. A., & Mateescu, M. (2011). Propagation models for computing biochemical reaction networks (pp. 1–3). Presented at the CMSB: Computational Methods in Systems Biology, Paris, France: Springer. https://doi.org/10.1145/2037509.2037510","ieee":"T. A. Henzinger and M. Mateescu, “Propagation models for computing biochemical reaction networks,” presented at the CMSB: Computational Methods in Systems Biology, Paris, France, 2011, pp. 1–3.","ista":"Henzinger TA, Mateescu M. 2011. Propagation models for computing biochemical reaction networks. CMSB: Computational Methods in Systems Biology, 1–3.","ama":"Henzinger TA, Mateescu M. Propagation models for computing biochemical reaction networks. In: Springer; 2011:1-3. doi:10.1145/2037509.2037510"},"page":"1 - 3","has_accepted_license":"1","day":"21","scopus_import":1,"pubrep_id":"92","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2012-92-v1+1_Propagation_models_for_computing_biochemical_reaction_networks.pdf","creator":"system","content_type":"application/pdf","file_size":255780,"file_id":"4649","relation":"main_file","checksum":"7f5c65509db1a9fb049abedd9663ed06","date_updated":"2020-07-14T12:46:06Z","date_created":"2018-12-12T10:07:50Z"}],"_id":"3299","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","title":"Propagation models for computing biochemical reaction networks","status":"public","ddc":["000","004"],"abstract":[{"text":"We introduce propagation models, a formalism designed to support general and efficient data structures for the transient analysis of biochemical reaction networks. We give two use cases for propagation abstract data types: the uniformization method and numerical integration. We also sketch an implementation of a propagation abstract data type, which uses abstraction to approximate states.","lang":"eng"}],"type":"conference"},{"abstract":[{"text":"In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates.","lang":"eng"}],"type":"conference","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3316","status":"public","title":"Specification-centered robustness","day":"14","article_processing_charge":"No","scopus_import":1,"date_published":"2011-07-14T00:00:00Z","publication":"6th IEEE International Symposium on Industrial and Embedded Systems","citation":{"chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In 6th IEEE International Symposium on Industrial and Embedded Systems, 176–85. IEEE, 2011. https://doi.org/10.1109/SIES.2011.5953660.","mla":"Bloem, Roderick, et al. “Specification-Centered Robustness.” 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–85, doi:10.1109/SIES.2011.5953660.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185.","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems. SIES: International Symposium on Industrial Embedded Systems, 176–185.","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in 6th IEEE International Symposium on Industrial and Embedded Systems, Vasteras, Sweden, 2011, pp. 176–185.","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann, B. (2011). Specification-centered robustness. In 6th IEEE International Symposium on Industrial and Embedded Systems (pp. 176–185). Vasteras, Sweden: IEEE. https://doi.org/10.1109/SIES.2011.5953660","ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: 6th IEEE International Symposium on Industrial and Embedded Systems. IEEE; 2011:176-185. doi:10.1109/SIES.2011.5953660"},"page":"176 - 185","ec_funded":1,"publist_id":"3323","author":[{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Karin","last_name":"Greimel","full_name":"Greimel, Karin"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"}],"date_updated":"2021-01-12T07:42:36Z","date_created":"2018-12-11T12:02:38Z","year":"2011","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","month":"07","conference":{"end_date":"2011-06-17","start_date":"2011-06-15","location":"Vasteras, Sweden","name":" SIES: International Symposium on Industrial Embedded Systems"},"doi":"10.1109/SIES.2011.5953660","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse"}],"oa":1,"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"year":"2011","department":[{"_id":"ToHe"}],"publisher":"ACM","publication_status":"published","author":[{"full_name":"Tripakis, Stavros","last_name":"Tripakis","first_name":"Stavros"},{"full_name":"Lickly, Ben","last_name":"Lickly","first_name":"Ben"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Lee","first_name":"Edward","full_name":"Lee, Edward"}],"volume":33,"date_updated":"2021-01-12T07:42:52Z","date_created":"2018-12-11T12:02:51Z","article_number":"14","ec_funded":1,"publist_id":"3263","file_date_updated":"2020-07-14T12:46:09Z","oa":1,"project":[{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543"},{"call_identifier":"FP7","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"quality_controlled":"1","doi":"10.1145/1985342.1985345","language":[{"iso":"eng"}],"month":"07","_id":"3353","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","intvolume":" 33","title":"A theory of synchronous relational interfaces","ddc":["000","005"],"status":"public","pubrep_id":"85","oa_version":"Submitted Version","file":[{"relation":"main_file","file_id":"5235","date_created":"2018-12-12T10:16:45Z","date_updated":"2020-07-14T12:46:09Z","checksum":"5d44a8aa81e33210649beae507602138","file_name":"IST-2012-85-v1+1_A_theory_of_synchronous_relational_interfaces.pdf","access_level":"open_access","content_type":"application/pdf","file_size":775662,"creator":"system"}],"type":"journal_article","issue":"4","abstract":[{"text":"Compositional theories are crucial when designing large and complex systems from smaller components. In this work we propose such a theory for synchronous concurrent systems. Our approach follows so-called interface theories, which use game-theoretic interpretations of composition and refinement. These are appropriate for systems with distinct inputs and outputs, and explicit conditions on inputs that must be enforced during composition. Our interfaces model systems that execute in an infinite sequence of synchronous rounds. At each round, a contract must be satisfied. The contract is simply a relation specifying the set of valid input/output pairs. Interfaces can be composed by parallel, serial or feedback composition. A refinement relation between interfaces is defined, and shown to have two main properties: (1) it is preserved by composition, and (2) it is equivalent to substitutability, namely, the ability to replace an interface by another one in any context. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.","lang":"eng"}],"citation":{"ista":"Tripakis S, Lickly B, Henzinger TA, Lee E. 2011. A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). 33(4), 14.","apa":"Tripakis, S., Lickly, B., Henzinger, T. A., & Lee, E. (2011). A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). ACM. https://doi.org/10.1145/1985342.1985345","ieee":"S. Tripakis, B. Lickly, T. A. Henzinger, and E. Lee, “A theory of synchronous relational interfaces,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 33, no. 4. ACM, 2011.","ama":"Tripakis S, Lickly B, Henzinger TA, Lee E. A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems (TOPLAS). 2011;33(4). doi:10.1145/1985342.1985345","chicago":"Tripakis, Stavros, Ben Lickly, Thomas A Henzinger, and Edward Lee. “A Theory of Synchronous Relational Interfaces.” ACM Transactions on Programming Languages and Systems (TOPLAS). ACM, 2011. https://doi.org/10.1145/1985342.1985345.","mla":"Tripakis, Stavros, et al. “A Theory of Synchronous Relational Interfaces.” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 33, no. 4, 14, ACM, 2011, doi:10.1145/1985342.1985345.","short":"S. Tripakis, B. Lickly, T.A. Henzinger, E. Lee, ACM Transactions on Programming Languages and Systems (TOPLAS) 33 (2011)."},"publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","date_published":"2011-07-01T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"01"},{"abstract":[{"text":"Byzantine Fault Tolerant (BFT) protocols aim to improve the reliability of distributed systems. They enable systems to tolerate arbitrary failures in a bounded number of nodes. BFT protocols are usually proven correct for certain safety and liveness properties. However, recent studies have shown that the performance of state-of-the-art BFT protocols decreases drastically in the presence of even a single malicious node. This motivates a formal quantitative analysis of BFT protocols to investigate their performance characteristics under different scenarios. We present HyPerf, a new hybrid methodology based on model checking and simulation techniques for evaluating the performance of BFT protocols. We build a transition system corresponding to a BFT protocol and systematically explore the set of behaviors allowed by the protocol. We associate certain timing information with different operations in the protocol, like cryptographic operations and message transmission. After an elaborate state exploration, we use the time information to evaluate the performance characteristics of the protocol using simulation techniques. We integrate our framework in Mace, a tool for building and verifying distributed systems. We evaluate the performance of PBFT using our framework. We describe two different use-cases of our methodology. For the benign operation of the protocol, we use the time information as random variables to compute the probability distribution of the execution times. In the presence of faults, we estimate the worst-case performance of the protocol for various attacks that can be employed by malicious nodes. Our results show the importance of hybrid techniques in systematically analyzing the performance of large-scale systems.","lang":"eng"}],"type":"conference","oa_version":"Submitted Version","file":[{"file_name":"IST-2012-84-v1+1_Quantitative_evaluation_of_BFT_protocols.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":272017,"file_id":"4648","relation":"main_file","date_created":"2018-12-12T10:07:49Z","date_updated":"2020-07-14T12:46:09Z","checksum":"4dc8750ab7921f51de992000b13d1b01"}],"pubrep_id":"84","title":"Quantitative evaluation of BFT protocols","status":"public","ddc":["000","004"],"_id":"3355","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"13","has_accepted_license":"1","scopus_import":1,"date_published":"2011-10-13T00:00:00Z","page":"255 - 264","citation":{"chicago":"Halalai, Raluca, Thomas A Henzinger, and Vasu Singh. “Quantitative Evaluation of BFT Protocols,” 255–64. IEEE, 2011. https://doi.org/10.1109/QEST.2011.40.","short":"R. Halalai, T.A. Henzinger, V. Singh, in:, IEEE, 2011, pp. 255–264.","mla":"Halalai, Raluca, et al. Quantitative Evaluation of BFT Protocols. IEEE, 2011, pp. 255–64, doi:10.1109/QEST.2011.40.","ieee":"R. Halalai, T. A. Henzinger, and V. Singh, “Quantitative evaluation of BFT protocols,” presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany, 2011, pp. 255–264.","apa":"Halalai, R., Henzinger, T. A., & Singh, V. (2011). Quantitative evaluation of BFT protocols (pp. 255–264). Presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany: IEEE. https://doi.org/10.1109/QEST.2011.40","ista":"Halalai R, Henzinger TA, Singh V. 2011. Quantitative evaluation of BFT protocols. QEST: Quantitative Evaluation of Systems, 255–264.","ama":"Halalai R, Henzinger TA, Singh V. Quantitative evaluation of BFT protocols. In: IEEE; 2011:255-264. doi:10.1109/QEST.2011.40"},"file_date_updated":"2020-07-14T12:46:09Z","publist_id":"3260","date_created":"2018-12-11T12:02:51Z","date_updated":"2021-01-12T07:42:53Z","author":[{"full_name":"Halalai, Raluca","last_name":"Halalai","first_name":"Raluca","id":"584C6850-E996-11E9-805B-F01764644770"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","full_name":"Singh, Vasu"}],"publication_status":"published","publisher":"IEEE","department":[{"_id":"ToHe"}],"year":"2011","month":"10","language":[{"iso":"eng"}],"conference":{"start_date":"2011-09-05","location":"Aachen, Germany","end_date":"2011-09-08","name":"QEST: Quantitative Evaluation of Systems"},"doi":"10.1109/QEST.2011.40","quality_controlled":"1","oa":1},{"intvolume":" 12","publisher":"ACM","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","status":"public","title":"Qualitative concurrent parity games","year":"2011","_id":"3354","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","volume":12,"oa_version":"None","date_updated":"2023-02-23T10:26:18Z","date_created":"2018-12-11T12:02:51Z","related_material":{"record":[{"status":"public","relation":"later_version","id":"2054"}]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"type":"journal_article","article_number":"28","issue":"4","publist_id":"3262","abstract":[{"text":"We consider two-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We consider ω-regular winning conditions specified as parity objectives. Both players are allowed to use randomization when choosing their moves. We study the computation of the limit-winning set of states, consisting of the states where the sup-inf value of the game for player 1 is 1: in other words, a state is limit-winning if player 1 can ensure a probability of winning arbitrarily close to 1. We show that the limit-winning set can be computed in O(n2d+2) time, where n is the size of the game structure and 2d is the number of priorities (or colors). The membership problem of whether a state belongs to the limit-winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games. This is because concurrent games do not satisfy two of the most fundamental properties of turn-based parity games. First, in concurrent games limit-winning strategies require randomization; and second, they require infinite memory.","lang":"eng"}],"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","citation":{"short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational Logic (TOCL) 12 (2011).","mla":"Chatterjee, Krishnendu, et al. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4, 28, ACM, 2011, doi:10.1145/1970398.1970404.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL). ACM, 2011. https://doi.org/10.1145/1970398.1970404.","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 2011;12(4). doi:10.1145/1970398.1970404","ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Qualitative concurrent parity games,” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4. ACM, 2011.","apa":"Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2011). Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/1970398.1970404","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2011. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 12(4), 28."},"publication":"ACM Transactions on Computational Logic (TOCL)","language":[{"iso":"eng"}],"doi":"10.1145/1970398.1970404","date_published":"2011-07-04T00:00:00Z","scopus_import":1,"day":"04","month":"07"},{"day":"01","month":"10","page":"72 - 82","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"quality_controlled":"1","citation":{"ista":"Fisher J, Harel D, Henzinger TA. 2011. Biology as reactivity. Communications of the ACM. 54(10), 72–82.","apa":"Fisher, J., Harel, D., & Henzinger, T. A. (2011). Biology as reactivity. Communications of the ACM. ACM. https://doi.org/10.1145/2001269.2001289","ieee":"J. Fisher, D. Harel, and T. A. Henzinger, “Biology as reactivity,” Communications of the ACM, vol. 54, no. 10. ACM, pp. 72–82, 2011.","ama":"Fisher J, Harel D, Henzinger TA. Biology as reactivity. Communications of the ACM. 2011;54(10):72-82. doi:10.1145/2001269.2001289","chicago":"Fisher, Jasmin, David Harel, and Thomas A Henzinger. “Biology as Reactivity.” Communications of the ACM. ACM, 2011. https://doi.org/10.1145/2001269.2001289.","mla":"Fisher, Jasmin, et al. “Biology as Reactivity.” Communications of the ACM, vol. 54, no. 10, ACM, 2011, pp. 72–82, doi:10.1145/2001269.2001289.","short":"J. Fisher, D. Harel, T.A. Henzinger, Communications of the ACM 54 (2011) 72–82."},"publication":"Communications of the ACM","language":[{"iso":"eng"}],"date_published":"2011-10-01T00:00:00Z","doi":"10.1145/2001269.2001289","type":"journal_article","issue":"10","publist_id":"3267","ec_funded":1,"abstract":[{"text":"Exploring the connection of biology with reactive systems to better understand living systems.","lang":"eng"}],"department":[{"_id":"ToHe"}],"publisher":"ACM","intvolume":" 54","status":"public","title":"Biology as reactivity","publication_status":"published","_id":"3352","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","year":"2011","volume":54,"oa_version":"None","date_updated":"2021-01-12T07:42:52Z","date_created":"2018-12-11T12:02:50Z","author":[{"last_name":"Fisher","first_name":"Jasmin","full_name":"Fisher, Jasmin"},{"first_name":"David","last_name":"Harel","full_name":"Harel, David"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}]},{"oa":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1007/978-3-642-23217-6_27","conference":{"start_date":"2011-09-06","location":"Aachen, Germany","end_date":"2011-09-09","name":"CONCUR: Concurrency Theory"},"language":[{"iso":"eng"}],"month":"01","year":"2011","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","author":[{"full_name":"Fisher, Jasmin","first_name":"Jasmin","last_name":"Fisher"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Piterman, Nir","first_name":"Nir","last_name":"Piterman"},{"full_name":"Singh, Anmol","first_name":"Anmol","last_name":"Singh"},{"last_name":"Vardi","first_name":"Moshe","full_name":"Vardi, Moshe"}],"volume":6901,"date_updated":"2021-01-12T07:42:57Z","date_created":"2018-12-11T12:02:54Z","ec_funded":1,"publist_id":"3253","file_date_updated":"2020-07-14T12:46:10Z","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:10.1007/978-3-642-23217-6_27","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.","apa":"Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., & 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. https://doi.org/10.1007/978-3-642-23217-6_27","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.","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. Dynamic Reactive Modules. Vol. 6901, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:10.1007/978-3-642-23217-6_27.","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. https://doi.org/10.1007/978-3-642-23217-6_27."},"page":"404 - 418","date_published":"2011-01-01T00:00:00Z","scopus_import":1,"has_accepted_license":"1","article_processing_charge":"No","day":"01","_id":"3362","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 6901","status":"public","title":"Dynamic reactive modules","ddc":["000"],"oa_version":"Submitted Version","file":[{"checksum":"6bf2453d8e52e979ddb58d17325bad26","date_updated":"2020-07-14T12:46:10Z","date_created":"2020-05-19T16:17:48Z","relation":"main_file","file_id":"7870","file_size":337125,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2011_CONCUR_Fisher.pdf"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"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.","lang":"eng"}]},{"alternative_title":["LNCS"],"type":"conference","abstract":[{"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.","lang":"eng"}],"intvolume":" 6605","ddc":["000","005"],"title":"QUASY: quantitative synthesis tool","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3365","file":[{"file_id":"5022","relation":"main_file","checksum":"762e52eb296f6dbfbf2a75d98b8ebaee","date_created":"2018-12-12T10:13:37Z","date_updated":"2020-07-14T12:46:10Z","access_level":"open_access","file_name":"IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf","creator":"system","file_size":475661,"content_type":"application/pdf"}],"oa_version":"Submitted Version","pubrep_id":"77","scopus_import":1,"has_accepted_license":"1","day":"29","page":"267 - 271","citation":{"short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011, pp. 267–271.","mla":"Chatterjee, Krishnendu, et al. QUASY: Quantitative Synthesis Tool. Vol. 6605, Springer, 2011, pp. 267–71, doi:10.1007/978-3-642-19835-9_24.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. https://doi.org/10.1007/978-3-642-19835-9_24.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis tool. In: Vol 6605. Springer; 2011:267-271. doi:10.1007/978-3-642-19835-9_24","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.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., & 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. https://doi.org/10.1007/978-3-642-19835-9_24","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."},"date_published":"2011-09-29T00:00:00Z","publist_id":"3248","file_date_updated":"2020-07-14T12:46:10Z","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","year":"2011","volume":6605,"date_updated":"2021-01-12T07:42:58Z","date_created":"2018-12-11T12:02:55Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"},{"full_name":"Singh, Rohit","last_name":"Singh","first_name":"Rohit"}],"month":"09","quality_controlled":"1","oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-19835-9_24","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Saarbrucken, Germany","start_date":"2011-03-26","end_date":"2011-04-03"}},{"day":"01","month":"04","date_published":"2011-04-01T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"ama":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words.","ista":"Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words.","apa":"Chatterjee, K., Henzinger, T. A., & Tracol, M. (n.d.). The decidability frontier for probabilistic automata on infinite words. ArXiv.","ieee":"K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier for probabilistic automata on infinite words.” ArXiv.","mla":"Chatterjee, Krishnendu, et al. The Decidability Frontier for Probabilistic Automata on Infinite Words. ArXiv.","short":"K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1104.0127"}],"external_id":{"arxiv":["1104.0127"]},"project":[{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","call_identifier":"FP7"}],"page":"19","ec_funded":1,"publist_id":"3251","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"}],"type":"preprint","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","last_name":"Tracol","first_name":"Mathieu","full_name":"Tracol, Mathieu"}],"oa_version":"Preprint","date_updated":"2020-01-21T13:20:24Z","date_created":"2018-12-11T12:02:54Z","_id":"3363","year":"2011","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"ArXiv","publication_status":"submitted","title":"The decidability frontier for probabilistic automata on infinite words","status":"public"},{"_id":"3381","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Formalisms for specifying Markovian population models","ddc":["000"],"intvolume":" 22","pubrep_id":"628","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2016-628-v1+1_journals-ijfcs-HenzingerJW11.pdf","creator":"system","content_type":"application/pdf","file_size":222840,"file_id":"4707","relation":"main_file","checksum":"df88431872586c773fbcfea37d7b36a2","date_created":"2018-12-12T10:08:45Z","date_updated":"2020-07-14T12:46:11Z"}],"type":"journal_article","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"}],"issue":"4","publication":"IJFCS: International Journal of Foundations of Computer Science","citation":{"chicago":"Henzinger, Thomas A, Barbara Jobstmann, and Verena Wolf. “Formalisms for Specifying Markovian Population Models.” IJFCS: International Journal of Foundations of Computer Science. World Scientific Publishing, 2011. https://doi.org/10.1142/S0129054111008441.","mla":"Henzinger, Thomas A., et al. “Formalisms for Specifying Markovian Population Models.” IJFCS: International Journal of Foundations of Computer Science, vol. 22, no. 4, World Scientific Publishing, 2011, pp. 823–41, doi:10.1142/S0129054111008441.","short":"T.A. Henzinger, B. Jobstmann, V. Wolf, IJFCS: International Journal of Foundations of Computer Science 22 (2011) 823–841.","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.","ieee":"T. A. Henzinger, B. Jobstmann, and V. Wolf, “Formalisms for specifying Markovian population models,” IJFCS: International Journal of Foundations of Computer Science, vol. 22, no. 4. World Scientific Publishing, pp. 823–841, 2011.","apa":"Henzinger, T. A., Jobstmann, B., & Wolf, V. (2011). Formalisms for specifying Markovian population models. IJFCS: International Journal of Foundations of Computer Science. World Scientific Publishing. https://doi.org/10.1142/S0129054111008441","ama":"Henzinger TA, Jobstmann B, Wolf V. Formalisms for specifying Markovian population models. IJFCS: International Journal of Foundations of Computer Science. 2011;22(4):823-841. doi:10.1142/S0129054111008441"},"page":"823 - 841","date_published":"2011-06-01T00:00:00Z","scopus_import":1,"day":"01","has_accepted_license":"1","year":"2011","publication_status":"published","publisher":"World Scientific Publishing","department":[{"_id":"ToHe"}],"author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"first_name":"Verena","last_name":"Wolf","full_name":"Wolf, Verena"}],"related_material":{"record":[{"id":"3841","relation":"earlier_version","status":"public"}]},"date_created":"2018-12-11T12:03:00Z","date_updated":"2023-02-23T11:45:03Z","volume":22,"file_date_updated":"2020-07-14T12:46:11Z","publist_id":"3226","oa":1,"quality_controlled":"1","doi":"10.1142/S0129054111008441","language":[{"iso":"eng"}],"month":"06"},{"publication":"Logical Methods in Computer Science","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed Parity Games: Complexity and Robustness.” Logical Methods in Computer Science. International Federation of Computational Logic, 2011. https://doi.org/10.2168/LMCS-7(4:8)2011.","mla":"Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.” Logical Methods in Computer Science, vol. 7, no. 4, International Federation of Computational Logic, 2011, doi:10.2168/LMCS-7(4:8)2011.","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).","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity and robustness,” Logical Methods in Computer Science, vol. 7, no. 4. International Federation of Computational Logic, 2011.","apa":"Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2011). Timed parity games: Complexity and robustness. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-7(4:8)2011","ama":"Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 2011;7(4). doi:10.2168/LMCS-7(4:8)2011"},"date_published":"2011-12-14T00:00:00Z","scopus_import":1,"day":"14","has_accepted_license":"1","ddc":["000","005"],"title":"Timed parity games: Complexity and robustness","status":"public","intvolume":" 7","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"3315","oa_version":"Published Version","file":[{"date_updated":"2020-07-14T12:46:07Z","date_created":"2018-12-12T10:16:42Z","checksum":"3480e1594bbef25ff7462fa93a8a814e","file_id":"5231","relation":"main_file","creator":"system","content_type":"application/pdf","file_size":588863,"file_name":"IST-2016-86-v2+1_1011.0688_3_.pdf","access_level":"open_access"}],"pubrep_id":"506","type":"journal_article","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."}],"issue":"4","quality_controlled":"1","project":[{"grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7"}],"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.2168/LMCS-7(4:8)2011","month":"12","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"International Federation of Computational Logic","year":"2011","date_updated":"2023-02-23T11:46:35Z","date_created":"2018-12-11T12:02:37Z","volume":7,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Prabhu, Vinayak","first_name":"Vinayak","last_name":"Prabhu"}],"related_material":{"record":[{"id":"3876","relation":"earlier_version","status":"public"}]},"license":"https://creativecommons.org/licenses/by-nd/4.0/","file_date_updated":"2020-07-14T12:46:07Z","publist_id":"3324","ec_funded":1},{"month":"10","doi":"10.1007/978-3-642-24372-1_37","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2011-10-11","location":"Taipei, Taiwan","end_date":"2011-10-14"},"language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","publist_id":"3309","file_date_updated":"2020-07-14T12:46:07Z","author":[{"full_name":"Almagor, Shaull","first_name":"Shaull","last_name":"Almagor"},{"last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"volume":6996,"date_created":"2018-12-11T12:02:41Z","date_updated":"2021-01-12T07:42:40Z","year":"2011","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","article_processing_charge":"No","has_accepted_license":"1","day":"14","date_published":"2011-10-14T00:00:00Z","citation":{"chicago":"Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about Weighted Automata ,” 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37.","mla":"Almagor, Shaull, et al. What’s Decidable about Weighted Automata . Vol. 6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37.","short":"S. Almagor, U. Boker, O. Kupferman, in:, Springer, 2011, pp. 482–491.","ista":"Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata . ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996, 482–491.","apa":"Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about weighted automata (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37","ieee":"S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted automata ,” presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.","ama":"Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata . In: Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37"},"page":"482 - 491","abstract":[{"lang":"eng","text":"Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning, make the un- decidability result accessible to the automata-theoretic community, and strengthen it to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Submitted Version","file":[{"checksum":"a7ca08a2cb1b6925f4c18a3034ae5659","date_created":"2020-05-19T16:08:32Z","date_updated":"2020-07-14T12:46:07Z","file_id":"7868","relation":"main_file","creator":"dernst","file_size":182309,"content_type":"application/pdf","access_level":"open_access","file_name":"2011_LNCS_Almagor.pdf"}],"_id":"3326","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 6996","ddc":["000"],"status":"public","title":"What’s decidable about weighted automata "},{"date_published":"2011-01-26T00:00:00Z","doi":"10.1145/1926385.1926454","conference":{"end_date":"2011-01-28","location":"Texas, USA","start_date":"2011-01-26","name":"POPL: Principles of Programming Languages"},"language":[{"iso":"eng"}],"citation":{"ama":"Alur R, Cerny P. Streaming transducers for algorithmic verification of single pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:10.1145/1926385.1926454","ista":"Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification of single pass list processing programs. POPL: Principles of Programming Languages vol. 46, 599–610.","apa":"Alur, R., & Cerny, P. (2011). Streaming transducers for algorithmic verification of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the POPL: Principles of Programming Languages, Texas, USA: ACM. https://doi.org/10.1145/1926385.1926454","ieee":"R. Alur and P. Cerny, “Streaming transducers for algorithmic verification of single pass list processing programs,” presented at the POPL: Principles of Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.","mla":"Alur, Rajeev, and Pavol Cerny. Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs. Vol. 46, no. 1, ACM, 2011, pp. 599–610, doi:10.1145/1926385.1926454.","short":"R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610.","chicago":"Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. https://doi.org/10.1145/1926385.1926454."},"page":"599 - 610","quality_controlled":"1","article_processing_charge":"No","day":"26","month":"01","scopus_import":"1","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"}],"oa_version":"None","volume":46,"date_updated":"2022-03-21T08:12:51Z","date_created":"2018-12-11T12:02:41Z","_id":"3325","year":"2011","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 46","department":[{"_id":"ToHe"}],"publisher":"ACM","title":"Streaming transducers for algorithmic verification of single pass list processing programs","status":"public","publication_status":"published","issue":"1","publist_id":"3310","abstract":[{"lang":"eng","text":"We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data do- main that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next in- put symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenat- ing data-string variables and new symbols formed from data vari- ables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over in- put/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional pro- grams, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative pro- grams dynamically modify a singly-linked heap by changing next- pointers of heap-nodes and by adding new nodes. The main re- striction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse."}],"type":"conference"},{"status":"public","title":"Decision procedures for automating termination proofs","intvolume":" 6538","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"3324","oa_version":"Submitted Version","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs."}],"page":"371 - 386","citation":{"ama":"Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26","ieee":"R. Piskac and T. Wies, “Decision procedures for automating termination proofs,” presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA, 2011, vol. 6538, pp. 371–386.","apa":"Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26","ista":"Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.","short":"R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386.","mla":"Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26.","chicago":"Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. https://doi.org/10.1007/978-3-642-18275-4_26."},"date_published":"2011-01-01T00:00:00Z","scopus_import":1,"day":"01","publication_status":"published","editor":[{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"first_name":"David","last_name":"Schmidt","full_name":"Schmidt, David"}],"department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2011","date_created":"2018-12-11T12:02:40Z","date_updated":"2021-01-12T07:42:39Z","volume":6538,"author":[{"full_name":"Piskac, Ruzica","last_name":"Piskac","first_name":"Ruzica"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"}],"publist_id":"3311","quality_controlled":"1","oa":1,"main_file_link":[{"url":"https://infoscience.epfl.ch/record/170697/","open_access":"1"}],"language":[{"iso":"eng"}],"conference":{"name":"VMCAI: Verification Model Checking and Abstract Interpretation","start_date":"2011-01-23","location":"Texas, USA","end_date":"2011-01-25"},"doi":"10.1007/978-3-642-18275-4_26","month":"01"},{"month":"08","language":[{"iso":"eng"}],"conference":{"location":"Bergen, Norway","start_date":"2011-09-12","end_date":"2011-09-15","name":"CSL: Computer Science Logic"},"doi":"10.4230/LIPIcs.CSL.2011.82","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","name":"Design for Embedded Systems","call_identifier":"FP7"}],"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"file_date_updated":"2020-07-14T12:46:10Z","publist_id":"3255","ec_funded":1,"date_updated":"2021-01-12T07:42:56Z","date_created":"2018-12-11T12:02:53Z","volume":12,"author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi","full_name":"Boker, Udi"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2011","day":"31","has_accepted_license":"1","scopus_import":1,"date_published":"2011-08-31T00:00:00Z","page":"82 - 96","citation":{"mla":"Boker, Udi, and Thomas A. Henzinger. Determinizing Discounted-Sum Automata. Vol. 12, Springer, 2011, pp. 82–96, doi:10.4230/LIPIcs.CSL.2011.82.","short":"U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 82–96.","chicago":"Boker, Udi, and Thomas A Henzinger. “Determinizing Discounted-Sum Automata,” 12:82–96. Springer, 2011. https://doi.org/10.4230/LIPIcs.CSL.2011.82.","ama":"Boker U, Henzinger TA. Determinizing discounted-sum automata. In: Vol 12. Springer; 2011:82-96. doi:10.4230/LIPIcs.CSL.2011.82","ista":"Boker U, Henzinger TA. 2011. Determinizing discounted-sum automata. CSL: Computer Science Logic, LIPIcs, vol. 12, 82–96.","ieee":"U. Boker and T. A. Henzinger, “Determinizing discounted-sum automata,” presented at the CSL: Computer Science Logic, Bergen, Norway, 2011, vol. 12, pp. 82–96.","apa":"Boker, U., & Henzinger, T. A. (2011). Determinizing discounted-sum automata (Vol. 12, pp. 82–96). Presented at the CSL: Computer Science Logic, Bergen, Norway: Springer. https://doi.org/10.4230/LIPIcs.CSL.2011.82"},"abstract":[{"text":"A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, which values a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by lambda^i, where the discount factor lambda is a fixed rational number greater than 1. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, which reflects the assumption that earlier weights are more important than later weights. Determinizing automata is often essential, for example, in formal verification, where there are polynomial algorithms for comparing two deterministic NDAs, while the equivalence problem for NDAs is not known to be decidable. Unfortunately, however, discounted-sum automata are, in general, not determinizable: it is currently known that for every rational discount factor 1 < lambda < 2, there is an NDA with lambda (denoted lambda-NDA) that cannot be determinized. We provide positive news, showing that every NDA with an integral factor is determinizable. We also complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: we show that for every non-integral rational factor lambda, there is a nondeterminizable lambda-NDA. Finally, we prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. This shows that for integral discount factors, the class of NDAs forms an attractive specification formalism in quantitative formal verification. All our results hold equally for automata over finite words and for automata over infinite words. ","lang":"eng"}],"alternative_title":["LIPIcs"],"type":"conference","oa_version":"Published Version","file":[{"checksum":"250603c6be8ccad4fbd4d7b24221f0ee","date_updated":"2020-07-14T12:46:10Z","date_created":"2018-12-12T10:10:17Z","file_id":"4803","relation":"main_file","creator":"system","content_type":"application/pdf","file_size":504270,"access_level":"open_access","file_name":"IST-2012-82-v1+1_Determinizing_discounted-sum_automata.pdf"}],"pubrep_id":"82","ddc":["004"],"title":"Determinizing discounted-sum automata","status":"public","intvolume":" 12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"3360"},{"month":"06","doi":"10.1109/CSF.2011.21","conference":{"end_date":"2011-06-29","start_date":"2011-06-27","location":"Cernay-la-Ville, France","name":"CSF: Computer Security Foundations"},"language":[{"iso":"eng"}],"oa":1,"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","publist_id":"3254","ec_funded":1,"file_date_updated":"2020-07-14T12:46:10Z","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"date_updated":"2021-01-12T07:42:56Z","date_created":"2018-12-11T12:02:54Z","year":"2011","publisher":"IEEE","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication_status":"published","has_accepted_license":"1","day":"27","scopus_import":1,"date_published":"2011-06-27T00:00:00Z","citation":{"ista":"Cerny P, Chatterjee K, Henzinger TA. 2011. The complexity of quantitative information flow problems. CSF: Computer Security Foundations, 205–217.","apa":"Cerny, P., Chatterjee, K., & Henzinger, T. A. (2011). The complexity of quantitative information flow problems (pp. 205–217). Presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France: IEEE. https://doi.org/10.1109/CSF.2011.21","ieee":"P. Cerny, K. Chatterjee, and T. A. Henzinger, “The complexity of quantitative information flow problems,” presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France, 2011, pp. 205–217.","ama":"Cerny P, Chatterjee K, Henzinger TA. The complexity of quantitative information flow problems. In: IEEE; 2011:205-217. doi:10.1109/CSF.2011.21","chicago":"Cerny, Pavol, Krishnendu Chatterjee, and Thomas A Henzinger. “The Complexity of Quantitative Information Flow Problems,” 205–17. IEEE, 2011. https://doi.org/10.1109/CSF.2011.21.","mla":"Cerny, Pavol, et al. The Complexity of Quantitative Information Flow Problems. IEEE, 2011, pp. 205–17, doi:10.1109/CSF.2011.21.","short":"P. Cerny, K. Chatterjee, T.A. Henzinger, in:, IEEE, 2011, pp. 205–217."},"page":"205 - 217","abstract":[{"text":"In this paper, we investigate the computational complexity of quantitative information flow (QIF) problems. Information-theoretic quantitative relaxations of noninterference (based on Shannon entropy)have been introduced to enable more fine-grained reasoning about programs in situations where limited information flow is acceptable. The QIF bounding problem asks whether the information flow in a given program is bounded by a constant $d$. Our first result is that the QIF bounding problem is PSPACE-complete. The QIF memoryless synthesis problem asks whether it is possible to resolve nondeterministic choices in a given partial program in such a way that in the resulting deterministic program, the quantitative information flow is bounded by a given constant $d$. Our second result is that the QIF memoryless synthesis problem is also EXPTIME-complete. The QIF memoryless synthesis problem generalizes to QIF general synthesis problem which does not impose the memoryless requirement (that is, by allowing the synthesized program to have more variables then the original partial program). Our third result is that the QIF general synthesis problem is EXPTIME-hard.","lang":"eng"}],"type":"conference","pubrep_id":"81","file":[{"checksum":"1a25be0c62459fc7640db88af08ff63a","date_updated":"2020-07-14T12:46:10Z","date_created":"2018-12-12T10:10:07Z","relation":"main_file","file_id":"4792","file_size":299069,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2012-81-v1+1_The_complexity_of_quantitative_information_flow_problems.pdf"}],"oa_version":"Submitted Version","_id":"3361","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","title":"The complexity of quantitative information flow problems","ddc":["000","005"],"status":"public"}]