[{"file_date_updated":"2020-07-14T12:46:45Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Distributed synthesis for LTL Fragments","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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","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","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.","mla":"Chatterjee, Krishnendu, et al. 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.","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."},"date_updated":"2023-02-21T17:01:26Z","status":"public","pubrep_id":"130","type":"technical_report","_id":"5406","related_material":{"record":[{"id":"1376","status":"public","relation":"later_version"}]},"doi":"10.15479/AT:IST-2013-130-v1-1","date_published":"2013-07-08T00:00:00Z","date_created":"2018-12-12T11:39:09Z","page":"11","day":"08","file":[{"file_id":"5540","checksum":"855513ebaf6f72228800c5fdb522f93c","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2013-130-v1+1_Distributed_Synthesis.pdf","date_created":"2018-12-12T11:54:18Z","creator":"system","file_size":467895,"date_updated":"2020-07-14T12:46:45Z"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2013","publication_status":"published","month":"07","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"oa_version":"Published Version","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:45:38Z","department":[{"_id":"ToHe"}],"date_updated":"2023-02-23T12:25:26Z","ddc":["005","000"],"type":"conference","conference":{"name":"CONCUR: Concurrency Theory","end_date":"2013-08-30","location":"Buenos Aires, Argentina","start_date":"2013-08-27"},"status":"public","pubrep_id":"129","series_title":"Lecture Notes in Computer Science","_id":"2327","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5417"}]},"volume":8052,"publication_status":"published","file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"4c04695c4bfdf2119cd4f5d1babc3e8a","file_id":"5301","creator":"system","file_size":378587,"date_updated":"2020-07-14T12:45:38Z","file_name":"IST-2013-129-v1+1_concur.pdf","date_created":"2018-12-12T10:17:45Z"}],"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"08","intvolume":" 8052","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."}],"oa_version":"Submitted Version","author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop"}],"publist_id":"4599","title":"From model checking to model measuring","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.","ista":"Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052, 273–287.","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.","ieee":"T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol. 8052. Springer, pp. 273–287, 2013.","ama":"Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287. doi:10.1007/978-3-642-40184-8_20","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"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"273 - 287","date_published":"2013-08-01T00:00:00Z","doi":"10.1007/978-3-642-40184-8_20","date_created":"2018-12-11T11:57:00Z","has_accepted_license":"1","year":"2013","day":"01","quality_controlled":"1","publisher":"Springer","oa":1},{"oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","month":"06","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"}],"oa_version":"Published Version","page":"23","date_created":"2019-05-13T14:13:27Z","doi":"10.15479/AT:IST-2013-124-v1-1","date_published":"2013-06-13T00:00:00Z","publication_status":"published","year":"2013","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"file":[{"file_size":549684,"date_updated":"2020-07-14T12:47:30Z","creator":"dernst","file_name":"2013_TechRep_Henzinger.pdf","date_created":"2019-05-13T14:11:39Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"6441","checksum":"a219ba4eada6cd62befed52262ee15d4"}],"day":"13","type":"technical_report","pubrep_id":"124","status":"public","_id":"6440","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Payer, Hannes","last_name":"Payer","first_name":"Hannes"},{"last_name":"Sezgin","full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali"}],"title":"Replacing competition with cooperation to achieve scalable lock-free FIFO queues ","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:30Z","date_updated":"2020-07-14T23:06:19Z","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.","ista":"Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p.","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.","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","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","short":"T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.","ieee":"T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013."},"ddc":["000","005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"author":[{"full_name":"Dragoi, Cezara","last_name":"Dragoi","first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","citation":{"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.","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.","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, 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","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.","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."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"page":"174-190","date_published":"2013-01-01T00:00:00Z","doi":"10.1007/978-3-642-39799-8_11","date_created":"2018-12-18T13:10:21Z","has_accepted_license":"1","year":"2013","publication":"Computer Aided Verification","publisher":"Springer Berlin Heidelberg","quality_controlled":"1","oa":1,"file_date_updated":"2020-07-14T12:47:10Z","department":[{"_id":"ToHe"}],"date_updated":"2023-09-05T14:16:07Z","ddc":["005"],"type":"book_chapter","conference":{"start_date":"2013-07-13","end_date":"2013-07-19","location":"Saint Petersburg, Russia","name":"CAV 2013"},"status":"public","pubrep_id":"195","_id":"5747","series_title":"CAV","volume":8044,"ec_funded":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642397981","9783642397998"]},"publication_status":"published","file":[{"date_created":"2018-12-18T13:13:33Z","file_name":"2013_CAV_Dragoi.pdf","creator":"dernst","date_updated":"2020-07-14T12:47:10Z","file_size":236480,"checksum":"a901cc6b71db08b61c0d4c0cbacc6287","file_id":"5748","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"scopus_import":"1","place":"Berlin, Heidelberg","intvolume":" 8044","oa_version":"None"},{"author":[{"full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien"}],"publist_id":"5802","article_processing_charge":"No","title":"Analysis of dynamic message passing programs","citation":{"apa":"Zufferey, D. (2013). Analysis of dynamic message passing programs. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:1405","ama":"Zufferey D. Analysis of dynamic message passing programs. 2013. doi:10.15479/at:ista:1405","ieee":"D. Zufferey, “Analysis of dynamic message passing programs,” Institute of Science and Technology Austria, 2013.","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.","ista":"Zufferey D. 2013. Analysis of dynamic message passing programs. Institute of Science and Technology Austria.","chicago":"Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute of Science and Technology Austria, 2013. https://doi.org/10.15479/at:ista:1405."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"page":"134","date_published":"2013-09-05T00:00:00Z","doi":"10.15479/at:ista:1405","date_created":"2018-12-11T11:51:50Z","has_accepted_license":"1","year":"2013","day":"05","publisher":"Institute of Science and Technology Austria","oa":1,"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. ","file_date_updated":"2021-11-17T13:47:58Z","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"date_updated":"2023-09-07T11:36:37Z","ddc":["000"],"type":"dissertation","status":"public","_id":"1405","related_material":{"record":[{"id":"2847","status":"public","relation":"part_of_dissertation"},{"status":"public","id":"3251","relation":"part_of_dissertation"},{"status":"public","id":"4361","relation":"part_of_dissertation"}]},"ec_funded":1,"publication_identifier":{"issn":["2663-337X"]},"degree_awarded":"PhD","publication_status":"published","file":[{"file_id":"9176","checksum":"ed2d7b52933d134e8dc69d569baa284e","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2021-02-22T11:28:36Z","file_name":"2013_Zufferey_thesis_final.pdf","creator":"dernst","date_updated":"2021-02-22T11:28:36Z","file_size":1514906},{"creator":"cchlebak","file_size":1378313,"date_updated":"2021-11-17T13:47:58Z","file_name":"2013_Zufferey_thesis_final_pdfa.pdf","date_created":"2021-11-16T14:42:52Z","relation":"main_file","access_level":"closed","content_type":"application/pdf","file_id":"10298","checksum":"cecc4c4b14225bee973d32e3dba91a55"}],"language":[{"iso":"eng"}],"alternative_title":["ISTA Thesis"],"main_file_link":[{"url":"http://dzufferey.github.io/files/2013_thesis.pdf"}],"month":"09","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."}],"oa_version":"Published Version"},{"status":"public","type":"conference","conference":{"end_date":"2013-03-24","location":"Rome, Italy","start_date":"2013-03-16","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"_id":"2847","series_title":"Lecture Notes in Computer Science","department":[{"_id":"ToHe"}],"date_updated":"2023-09-07T11:36:36Z","month":"03","intvolume":" 7795","scopus_import":1,"alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf"}],"oa_version":"Submitted Version","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"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"volume":7795,"ec_funded":1,"language":[{"iso":"eng"}],"publication_status":"published","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"title":"Structural Counter Abstraction","editor":[{"first_name":"Nir","full_name":"Piterman, Nir","last_name":"Piterman"},{"last_name":"Smolka","full_name":"Smolka, Scott","first_name":"Scott"}],"publist_id":"3947","author":[{"first_name":"Kshitij","last_name":"Bansal","full_name":"Bansal, Kshitij"},{"last_name":"Koskinen","full_name":"Koskinen, Eric","first_name":"Eric"},{"first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies"},{"last_name":"Zufferey","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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","short":"K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.","ieee":"K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,” vol. 7795. Springer, pp. 62–77, 2013.","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.","ista":"Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman & S. Smolka). 7795, 62–77."},"quality_controlled":"1","publisher":"Springer","oa":1,"date_published":"2013-03-01T00:00:00Z","doi":"10.1007/978-3-642-36742-7_5","date_created":"2018-12-11T11:59:54Z","page":"62 - 77","day":"01","year":"2013"},{"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"citation":{"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.","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","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","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.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2013, pp. 951–967.","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.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","full_name":"Cerny, Pavol","last_name":"Cerny"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid","first_name":"Leonid"},{"full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","first_name":"Thorsten"}],"publist_id":"4458","title":"Efficient synthesis for concurrency by semantics-preserving transformations","quality_controlled":"1","publisher":"Springer","oa":1,"has_accepted_license":"1","year":"2013","day":"01","page":"951 - 967","date_published":"2013-07-01T00:00:00Z","doi":"10.1007/978-3-642-39799-8_68","date_created":"2018-12-11T11:57:42Z","_id":"2445","type":"conference","conference":{"start_date":"2013-07-13","location":"St. Petersburg, Russia","end_date":"2013-07-19","name":"CAV: Computer Aided Verification"},"status":"public","pubrep_id":"199","date_updated":"2023-09-07T11:57:01Z","ddc":["000","004"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:40Z","abstract":[{"lang":"eng","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."}],"oa_version":"Submitted Version","scopus_import":1,"alternative_title":["LNCS"],"month":"07","intvolume":" 8044","publication_status":"published","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"70c70ca5487faba82262c63e1b678a27","file_id":"5158","file_size":365548,"date_updated":"2020-07-14T12:45:40Z","creator":"system","file_name":"IST-2014-199-v1+1_cav2013-final.pdf","date_created":"2018-12-12T10:15:37Z"}],"language":[{"iso":"eng"}],"volume":8044,"related_material":{"record":[{"relation":"dissertation_contains","id":"1130","status":"public"}]},"ec_funded":1},{"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1109.6926","open_access":"1"}],"month":"11","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."}],"oa_version":"Preprint","ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"type":"conference","conference":{"end_date":"2012-11-16","location":"Cary, NC, USA","start_date":"2012-11-11","name":"FSE: Foundations of Software Engineering"},"status":"public","_id":"1384","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:50:18Z","publisher":"ACM","quality_controlled":"1","oa":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.","doi":"10.1145/2393596.2393664","date_published":"2012-11-01T00:00:00Z","date_created":"2018-12-11T11:51:42Z","year":"2012","day":"01","publication":"Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"article_number":"57","author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mehmet","last_name":"Keremoglu","full_name":"Keremoglu, Mehmet"},{"last_name":"Wendler","full_name":"Wendler, Philipp","first_name":"Philipp"}],"publist_id":"5826","title":"Conditional model checking: A technique to pass information between verifiers","citation":{"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.","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.","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.","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.","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","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."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"status":"public","type":"journal_article","_id":"2302","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"date_updated":"2021-01-12T06:56:38Z","month":"07","intvolume":" 10","scopus_import":1,"oa_version":"None","pmid":1,"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."}],"volume":10,"issue":"2","ec_funded":1,"language":[{"iso":"eng"}],"publication_status":"published","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"title":"The propagation approach for computing biochemical reaction networks","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Mateescu, Maria","last_name":"Mateescu","first_name":"Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"4625","external_id":{"pmid":["22778152"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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","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","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.","short":"T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322.","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.","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."},"publisher":"IEEE","quality_controlled":"1","date_published":"2012-07-03T00:00:00Z","doi":"10.1109/TCBB.2012.91","date_created":"2018-12-11T11:56:52Z","page":"310 - 322","day":"03","publication":"IEEE ACM Transactions on Computational Biology and Bioinformatics","year":"2012"},{"abstract":[{"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.","lang":"eng"}],"oa_version":"Submitted Version","pmid":1,"scopus_import":1,"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/","open_access":"1"}],"month":"05","intvolume":" 301","publication_status":"published","language":[{"iso":"eng"}],"volume":301,"ec_funded":1,"_id":"2848","type":"journal_article","status":"public","date_updated":"2021-01-12T07:00:12Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Elsevier","quality_controlled":"1","oa":1,"year":"2012","day":"21","publication":"Journal of Theoretical Biology","page":"161 - 173","doi":"10.1016/j.jtbi.2012.02.021","date_published":"2012-05-21T00:00:00Z","date_created":"2018-12-11T11:59:55Z","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"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","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","short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","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.","ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 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."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"3946","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"external_id":{"pmid":["22394652"]},"title":"Evolutionary game dynamics in populations with different learners"}]