[{"corr_author":"1","pubrep_id":"28","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","call_identifier":"FP7"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems","grant_number":"214373","call_identifier":"FP7"}],"type":"conference","month":"10","abstract":[{"lang":"eng","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 an almost complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words."}],"doi":"10.1007/978-3-642-15643-4_1","oa_version":"None","date_created":"2018-12-11T12:05:33Z","title":"Probabilistic Automata on infinite words: decidability and undecidability results","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publist_id":"2324","intvolume":"      6252","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2010-10-12T00:00:00Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5392"}]},"_id":"3857","quality_controlled":"1","volume":6252,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","day":"12","alternative_title":["LNCS"],"citation":{"chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Probabilistic Automata on Infinite Words: Decidability and Undecidability Results,” 6252:1–16. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15643-4_1\">https://doi.org/10.1007/978-3-642-15643-4_1</a>.","ista":"Chatterjee K, Henzinger TA. 2010. Probabilistic Automata on infinite words: decidability and undecidability results. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6252, 1–16.","short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2010, pp. 1–16.","ieee":"K. Chatterjee and T. A. Henzinger, “Probabilistic Automata on infinite words: decidability and undecidability results,” presented at the ATVA: Automated Technology for Verification and Analysis, Singapore, Singapore, 2010, vol. 6252, pp. 1–16.","ama":"Chatterjee K, Henzinger TA. Probabilistic Automata on infinite words: decidability and undecidability results. In: Vol 6252. Springer; 2010:1-16. doi:<a href=\"https://doi.org/10.1007/978-3-642-15643-4_1\">10.1007/978-3-642-15643-4_1</a>","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2010). Probabilistic Automata on infinite words: decidability and undecidability results (Vol. 6252, pp. 1–16). Presented at the ATVA: Automated Technology for Verification and Analysis, Singapore, Singapore: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15643-4_1\">https://doi.org/10.1007/978-3-642-15643-4_1</a>","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. Vol. 6252, Springer, 2010, pp. 1–16, doi:<a href=\"https://doi.org/10.1007/978-3-642-15643-4_1\">10.1007/978-3-642-15643-4_1</a>."},"page":"1 - 16","status":"public","publisher":"Springer","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2010-09-21","end_date":"2010-09-24","location":"Singapore, Singapore"},"scopus_import":1,"ec_funded":1,"date_updated":"2024-10-09T21:08:23Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"year":"2010"},{"status":"public","citation":{"mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>The Complexity of Partial-Observation Parity Games</i>. Vol. 6397, Springer, 2010, pp. 1–14, doi:<a href=\"https://doi.org/10.1007/978-3-642-16242-8_1\">10.1007/978-3-642-16242-8_1</a>.","ama":"Chatterjee K, Doyen L. The complexity of partial-observation parity games. In: Vol 6397. Springer; 2010:1-14. doi:<a href=\"https://doi.org/10.1007/978-3-642-16242-8_1\">10.1007/978-3-642-16242-8_1</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2010). The complexity of partial-observation parity games (Vol. 6397, pp. 1–14). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, Indonesia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-16242-8_1\">https://doi.org/10.1007/978-3-642-16242-8_1</a>","ieee":"K. Chatterjee and L. Doyen, “The complexity of partial-observation parity games,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, Indonesia, 2010, vol. 6397, pp. 1–14.","short":"K. Chatterjee, L. Doyen, in:, Springer, 2010, pp. 1–14.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “The Complexity of Partial-Observation Parity Games,” 6397:1–14. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-16242-8_1\">https://doi.org/10.1007/978-3-642-16242-8_1</a>.","ista":"Chatterjee K, Doyen L. 2010. The complexity of partial-observation parity games. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 6397, 1–14."},"ddc":["000"],"page":"1 - 14","scopus_import":"1","has_accepted_license":"1","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","end_date":"2010-10-15","start_date":"2010-10-10","location":"Yogyakarta, Indonesia"},"publisher":"Springer","file":[{"date_created":"2020-05-19T16:29:04Z","date_updated":"2020-07-14T12:46:18Z","access_level":"open_access","checksum":"770e86e5d78c56fddb4786a8da7ef126","file_size":142836,"content_type":"application/pdf","relation":"main_file","file_id":"7872","creator":"dernst","file_name":"2010_LPAR_Chatterjee.pdf"}],"date_updated":"2025-09-30T09:34:35Z","year":"2010","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}],"quality_controlled":"1","oa":1,"volume":6397,"alternative_title":["LNCS"],"day":"09","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","intvolume":"      6397","publist_id":"2323","language":[{"iso":"eng"}],"date_published":"2010-12-09T00:00:00Z","_id":"3858","isi":1,"corr_author":"1","abstract":[{"lang":"eng","text":"We consider two-player zero-sum games on graphs. On the basis of the information available to the players 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 com- plete view of the game). We survey the complexity results for the problem of de- ciding the winner in various classes of partial-observation games with ω-regular winning conditions specified as parity objectives. We present a reduction from the class of parity objectives that depend on sequence of states of the game to the sub-class of parity objectives that only depend on the sequence of observations. We also establish that partial-observation acyclic games are PSPACE-complete."}],"type":"conference","month":"12","file_date_updated":"2020-07-14T12:46:18Z","external_id":{"isi":["000288062700001"]},"title":"The complexity of partial-observation parity games","article_processing_charge":"No","date_created":"2018-12-11T12:05:33Z","doi":"10.1007/978-3-642-16242-8_1","oa_version":"Submitted Version","department":[{"_id":"KrCh"}]},{"date_published":"2010-09-20T00:00:00Z","editor":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2024-10-09T20:54:05Z","year":"2010","_id":"3859","related_material":{"link":[{"description":"eBook available via IST BookList","relation":"other","url":"https://koha.app.ist.ac.at/cgi-bin/koha/opac-detail.pl?biblionumber=12721"}]},"publist_id":"2322","citation":{"ieee":"K. Chatterjee and T. A. Henzinger, Eds., <i>Formal modeling and analysis of timed systems</i>, vol. 6246. Springer, 2010.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger, editors. <i>Formal Modeling and Analysis of Timed Systems</i>. Vol. 6246, Springer, 2010, doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9\">10.1007/978-3-642-15297-9</a>.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (Eds.). (2010). <i>Formal modeling and analysis of timed systems</i> (Vol. 6246). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-642-15297-9\">https://doi.org/10.1007/978-3-642-15297-9</a>","ama":"Chatterjee K, Henzinger TA, eds. <i>Formal Modeling and Analysis of Timed Systems</i>. Vol 6246. Springer; 2010. doi:<a href=\"https://doi.org/10.1007/978-3-642-15297-9\">10.1007/978-3-642-15297-9</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger, eds. <i>Formal Modeling and Analysis of Timed Systems</i>. Vol. 6246. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15297-9\">https://doi.org/10.1007/978-3-642-15297-9</a>.","short":"K. Chatterjee, T.A. Henzinger, eds., Formal Modeling and Analysis of Timed Systems, Springer, 2010.","ista":"Chatterjee K, Henzinger TA eds. 2010. Formal modeling and analysis of timed systems, Springer,p."},"status":"public","intvolume":"      6246","publication_status":"published","language":[{"iso":"eng"}],"publisher":"Springer","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2010-09-10","start_date":"2010-09-08","location":"Klosterneuburg, Austria"},"doi":"10.1007/978-3-642-15297-9","date_created":"2018-12-11T12:05:33Z","oa_version":"None","title":"Formal modeling and analysis of timed systems","volume":6246,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"20","alternative_title":["LNCS"],"corr_author":"1","type":"conference_editor","month":"09","quality_controlled":"1","abstract":[{"text":"This book constitutes the proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, held in Klosterneuburg, Austria in September 2010. The 14 papers presented were carefully reviewed and selected from 31 submissions. In addition, the volume contains 3 invited talks and 2 invited tutorials.The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share an interest in the modeling and analysis of timed systems. Typical topics include foundations and semantics, methods and tools, and applications.","lang":"eng"}]},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Generalized mean-payoff and energy games","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","doi":"10.4230/LIPIcs.FSTTCS.2010.505","oa_version":"Submitted Version","date_created":"2018-12-11T12:05:34Z","article_processing_charge":"No","type":"conference","file_date_updated":"2020-07-14T12:46:18Z","month":"12","abstract":[{"text":"In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter- reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.","lang":"eng"}],"external_id":{"isi":["000310361000043"]},"pubrep_id":"59","corr_author":"1","_id":"3860","isi":1,"date_published":"2010-12-13T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"         8","publication_status":"published","publist_id":"2321","day":"13","alternative_title":["LIPIcs"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":8,"quality_controlled":"1","oa":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Jean","last_name":"Raskin","full_name":"Raskin, Jean"}],"year":"2010","date_updated":"2025-09-30T09:33:50Z","file":[{"creator":"system","file_name":"IST-2012-59-v1+1_Generalized_mean-payoff_and_energy_games.pdf","relation":"main_file","file_id":"5147","file_size":178278,"content_type":"application/pdf","checksum":"1caabd6319b979927208117a41192637","access_level":"open_access","date_updated":"2020-07-14T12:46:18Z","date_created":"2018-12-12T10:15:27Z"},{"checksum":"3a59759ceeacdb5b578f3803d5e6769b","content_type":"application/pdf","file_size":477976,"access_level":"open_access","date_updated":"2020-07-14T12:46:18Z","date_created":"2018-12-12T10:15:28Z","creator":"system","file_name":"IST-2016-59-v2+1_2_1_.pdf","relation":"main_file","file_id":"5148"}],"conference":{"location":"Chennai, India","start_date":"2010-12-15","end_date":"2010-12-18","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","has_accepted_license":"1","scopus_import":"1","status":"public","citation":{"short":"K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 505–516.","ista":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2010. Generalized mean-payoff and energy games. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 8, 505–516.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Generalized Mean-Payoff and Energy Games,” 8:505–16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505\">https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. Generalized mean-payoff and energy games. In: Vol 8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:505-516. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505\">10.4230/LIPIcs.FSTTCS.2010.505</a>","mla":"Chatterjee, Krishnendu, et al. <i>Generalized Mean-Payoff and Energy Games</i>. Vol. 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 505–16, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505\">10.4230/LIPIcs.FSTTCS.2010.505</a>.","apa":"Chatterjee, K., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2010). Generalized mean-payoff and energy games (Vol. 8, pp. 505–516). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Chennai, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505\">https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505</a>","ieee":"K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Generalized mean-payoff and energy games,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Chennai, India, 2010, vol. 8, pp. 505–516."},"ddc":["005"],"page":"505 - 516"},{"oa":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"01","issue":"6","volume":208,"publisher":"Elsevier","file":[{"file_name":"IST-2012-56-v1+1_Strategy_logic.pdf","creator":"system","file_id":"4911","relation":"main_file","checksum":"13bff93f3c2a014e2908145a4517f177","content_type":"application/pdf","file_size":189120,"date_updated":"2020-07-14T12:46:18Z","access_level":"open_access","date_created":"2018-12-12T10:11:54Z"}],"has_accepted_license":"1","scopus_import":"1","page":"677 - 693","ddc":["000","004"],"citation":{"ista":"Chatterjee K, Henzinger TA, Piterman N. 2010. Strategy logic. Information and Computation. 208(6), 677–693.","short":"K. Chatterjee, T.A. Henzinger, N. Piterman, Information and Computation 208 (2010) 677–693.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “Strategy Logic.” <i>Information and Computation</i>. Elsevier, 2010. <a href=\"https://doi.org/10.1016/j.ic.2009.07.004\">https://doi.org/10.1016/j.ic.2009.07.004</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Piterman, N. (2010). Strategy logic. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2009.07.004\">https://doi.org/10.1016/j.ic.2009.07.004</a>","mla":"Chatterjee, Krishnendu, et al. “Strategy Logic.” <i>Information and Computation</i>, vol. 208, no. 6, Elsevier, 2010, pp. 677–93, doi:<a href=\"https://doi.org/10.1016/j.ic.2009.07.004\">10.1016/j.ic.2009.07.004</a>.","ama":"Chatterjee K, Henzinger TA, Piterman N. Strategy logic. <i>Information and Computation</i>. 2010;208(6):677-693. doi:<a href=\"https://doi.org/10.1016/j.ic.2009.07.004\">10.1016/j.ic.2009.07.004</a>","ieee":"K. Chatterjee, T. A. Henzinger, and N. Piterman, “Strategy logic,” <i>Information and Computation</i>, vol. 208, no. 6. Elsevier, pp. 677–693, 2010."},"status":"public","publication":"Information and Computation","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"}],"year":"2010","date_updated":"2025-09-30T09:32:18Z","external_id":{"isi":["000278070100006"]},"month":"06","type":"journal_article","file_date_updated":"2020-07-14T12:46:18Z","abstract":[{"lang":"eng","text":"We introduce strategy logic, a logic that treats strategies in two-player games as explicit first-order objects. The explicit treatment of strategies allows us to specify properties of nonzero-sum games in a simple and natural way. We show that the one-alternation fragment of strategy logic is strong enough to express the existence of Nash equilibria and secure equilibria, and subsumes other logics that were introduced to reason about games, such as ATL, ATL*, and game logic. We show that strategy logic is decidable, by constructing tree automata that recognize sets of strategies. While for the general logic, our decision procedure is nonelementary, for the simple fragment that is used above we show that the complexity is polynomial in the size of the game graph and optimal in the size of the formula (ranging from polynomial to 2EXPTIME depending on the form of the formula)."}],"pubrep_id":"56","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"doi":"10.1016/j.ic.2009.07.004","date_created":"2018-12-11T12:05:34Z","oa_version":"Submitted Version","article_processing_charge":"No","title":"Strategy logic","language":[{"iso":"eng"}],"publist_id":"2317","intvolume":"       208","publication_status":"published","_id":"3861","related_material":{"record":[{"id":"3884","relation":"earlier_version","status":"public"}]},"isi":1,"date_published":"2010-06-01T00:00:00Z"},{"date_updated":"2025-09-30T09:33:19Z","year":"2010","author":[{"full_name":"Berwanger, Dietmar","last_name":"Berwanger","first_name":"Dietmar"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Martin","last_name":"De Wulf","full_name":"De Wulf, Martin"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publication":"Information and Computation","status":"public","page":"1206 - 1220","ddc":["005"],"citation":{"chicago":"Berwanger, Dietmar, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, and Thomas A Henzinger. “Strategy Construction for Parity Games with Imperfect Information.” <i>Information and Computation</i>. Elsevier, 2010. <a href=\"https://doi.org/10.1016/j.ic.2009.09.006\">https://doi.org/10.1016/j.ic.2009.09.006</a>.","short":"D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, T.A. Henzinger, Information and Computation 208 (2010) 1206–1220.","ista":"Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. 2010. Strategy construction for parity games with imperfect information. Information and Computation. 208(10), 1206–1220.","mla":"Berwanger, Dietmar, et al. “Strategy Construction for Parity Games with Imperfect Information.” <i>Information and Computation</i>, vol. 208, no. 10, Elsevier, 2010, pp. 1206–20, doi:<a href=\"https://doi.org/10.1016/j.ic.2009.09.006\">10.1016/j.ic.2009.09.006</a>.","ieee":"D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and T. A. Henzinger, “Strategy construction for parity games with imperfect information,” <i>Information and Computation</i>, vol. 208, no. 10. Elsevier, pp. 1206–1220, 2010.","apa":"Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., &#38; Henzinger, T. A. (2010). Strategy construction for parity games with imperfect information. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2009.09.006\">https://doi.org/10.1016/j.ic.2009.09.006</a>","ama":"Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. Strategy construction for parity games with imperfect information. <i>Information and Computation</i>. 2010;208(10):1206-1220. doi:<a href=\"https://doi.org/10.1016/j.ic.2009.09.006\">10.1016/j.ic.2009.09.006</a>"},"ec_funded":1,"has_accepted_license":"1","scopus_import":"1","file":[{"creator":"system","file_name":"IST-2012-58-v1+1_Strategy_construction_for_parity_games_with_imperfect_information.pdf","relation":"main_file","file_id":"5300","checksum":"29d146e4f8049dbb7f80bbf7ea3700ed","file_size":287496,"content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:18Z","date_created":"2018-12-12T10:17:44Z"}],"publisher":"Elsevier","volume":208,"issue":"10","day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","oa":1,"date_published":"2010-10-01T00:00:00Z","_id":"3863","isi":1,"related_material":{"record":[{"relation":"earlier_version","id":"3880","status":"public"}]},"publication_status":"published","intvolume":"       208","publist_id":"2319","language":[{"iso":"eng"}],"title":"Strategy construction for parity games with imperfect information","article_processing_charge":"No","date_created":"2018-12-11T12:05:35Z","oa_version":"Submitted Version","doi":"10.1016/j.ic.2009.09.006","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pubrep_id":"58","abstract":[{"lang":"eng","text":"We consider two-player parity games with imperfect information in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. One major obstacle in adapting the classical procedure is that the complementation of attractor sets would break the invariant of downward-closedness on which the antichain representation relies. We overcome this difficulty by decomposing problem instances recursively into games with a combination of reachability, safety, and simpler parity conditions. We also report on an experimental implementation of our algorithm: to our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs."}],"file_date_updated":"2020-07-14T12:46:18Z","type":"journal_article","month":"10","project":[{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"external_id":{"isi":["000281830300007"]}},{"acknowledgement":"This research was supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign.","corr_author":"1","external_id":{"arxiv":["1004.0739"]},"arxiv":1,"month":"07","type":"conference","abstract":[{"lang":"eng","text":"Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal-synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification tinder the given input assumption, synthesize a system that optimizes the measured value. For safety specifications and measures that are defined by mean-payoff automata, the optimal-synthesis problem amounts to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be done in polynomial time. For general omega-regular specifications, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. We present some experimental results showing optimal systems that were automatically generated in this way."}],"date_created":"2018-12-11T12:05:35Z","oa_version":"Preprint","doi":"10.1007/978-3-642-14295-6_34","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1004.0739"}],"title":"Measuring and synthesizing systems in probabilistic environments","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publist_id":"2313","intvolume":"      6174","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2010-07-09T00:00:00Z","related_material":{"record":[{"id":"1856","relation":"later_version","status":"public"}]},"_id":"3864","oa":1,"quality_controlled":"1","volume":6174,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"09","alternative_title":["LNCS"],"page":"380 - 395","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” presented at the CAV: Computer Aided Verification, Edinburgh, United Kingdom, 2010, vol. 6174, pp. 380–395.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. In: Vol 6174. Springer; 2010:380-395. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_34\">10.1007/978-3-642-14295-6_34</a>","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2010). Measuring and synthesizing systems in probabilistic environments (Vol. 6174, pp. 380–395). Presented at the CAV: Computer Aided Verification, Edinburgh, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_34\">https://doi.org/10.1007/978-3-642-14295-6_34</a>","mla":"Chatterjee, Krishnendu, et al. <i>Measuring and Synthesizing Systems in Probabilistic Environments</i>. Vol. 6174, Springer, 2010, pp. 380–95, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_34\">10.1007/978-3-642-14295-6_34</a>.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2010. Measuring and synthesizing systems in probabilistic environments. CAV: Computer Aided Verification, LNCS, vol. 6174, 380–395.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments,” 6174:380–95. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_34\">https://doi.org/10.1007/978-3-642-14295-6_34</a>.","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2010, pp. 380–395."},"status":"public","conference":{"name":"CAV: Computer Aided Verification","end_date":"2010-07-19","start_date":"201-07-15","location":"Edinburgh, United Kingdom"},"publisher":"Springer","scopus_import":"1","date_updated":"2025-09-23T09:33:01Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"full_name":"Singh, Rohit","first_name":"Rohit","last_name":"Singh"}],"year":"2010"},{"department":[{"_id":"KrCh"}],"title":"Analyzing the impact of change in multi-threaded programs","doi":"10.1007/978-3-642-12029-9_21","oa_version":"None","date_created":"2018-12-11T12:05:35Z","article_processing_charge":"No","type":"conference","month":"04","abstract":[{"lang":"eng","text":"We introduce a technique for debugging multi-threaded C programs and analyzing the impact of source code changes, and its implementation in the prototype tool DIRECT. Our approach uses a combination of source code instrumentation and runtime management. The source code along with a test harness is instrumented to monitor Operating System (OS) and user defined function calls. DIRECT tracks all concurrency control primitives and, optionally, data from the program. DIRECT maintains an abstract global state that combines information from every thread, including the sequence of function calls and concurrency primitives executed. The runtime manager can insert delays, provoking thread inter-leavings that may exhibit bugs that are difficult to reach otherwise. The runtime manager collects an approximation of the reachable state space and uses this approximation to assess the impact of change in a new version of the program."}],"publication_identifier":{"eisbn":["9783642120299"],"eissn":["1611-3349"]},"_id":"3865","date_published":"2010-04-21T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"      6013","publication_status":"published","publist_id":"2315","day":"21","alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":6013,"quality_controlled":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"first_name":"Vishwanath","last_name":"Raman","full_name":"Raman, Vishwanath"},{"full_name":"Sánchez, César","first_name":"César","last_name":"Sánchez"}],"year":"2010","date_updated":"2025-05-20T06:36:30Z","conference":{"start_date":"2010-03-20","end_date":"2010-03-28","name":"FASE: Fundamental Approaches To Software Engineering","location":"Paphos, Cyprus"},"publisher":"Springer","scopus_import":"1","status":"public","publication":"13th International Conference on Fundamental Approaches to Software Engineering","OA_type":"closed access","citation":{"ista":"Chatterjee K, De Alfaro L, Raman V, Sánchez C. 2010. Analyzing the impact of change in multi-threaded programs. 13th International Conference on Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 6013, 293–307.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, Vishwanath Raman, and César Sánchez. “Analyzing the Impact of Change in Multi-Threaded Programs.” In <i>13th International Conference on Fundamental Approaches to Software Engineering</i>, 6013:293–307. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_21\">https://doi.org/10.1007/978-3-642-12029-9_21</a>.","short":"K. Chatterjee, L. De Alfaro, V. Raman, C. Sánchez, in:, 13th International Conference on Fundamental Approaches to Software Engineering, Springer, 2010, pp. 293–307.","mla":"Chatterjee, Krishnendu, et al. “Analyzing the Impact of Change in Multi-Threaded Programs.” <i>13th International Conference on Fundamental Approaches to Software Engineering</i>, vol. 6013, Springer, 2010, pp. 293–307, doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_21\">10.1007/978-3-642-12029-9_21</a>.","ieee":"K. Chatterjee, L. De Alfaro, V. Raman, and C. Sánchez, “Analyzing the impact of change in multi-threaded programs,” in <i>13th International Conference on Fundamental Approaches to Software Engineering</i>, Paphos, Cyprus, 2010, vol. 6013, pp. 293–307.","ama":"Chatterjee K, De Alfaro L, Raman V, Sánchez C. Analyzing the impact of change in multi-threaded programs. In: <i>13th International Conference on Fundamental Approaches to Software Engineering</i>. Vol 6013. Springer; 2010:293-307. doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_21\">10.1007/978-3-642-12029-9_21</a>","apa":"Chatterjee, K., De Alfaro, L., Raman, V., &#38; Sánchez, C. (2010). Analyzing the impact of change in multi-threaded programs. In <i>13th International Conference on Fundamental Approaches to Software Engineering</i> (Vol. 6013, pp. 293–307). Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_21\">https://doi.org/10.1007/978-3-642-12029-9_21</a>"},"page":"293 - 307"},{"ddc":["004"],"page":"410 - 424","citation":{"apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., &#38; Jobstmann, B. (2010). Robustness in the presence of liveness. In T. Touili, B. Cook, &#38; P. Jackson (Eds.) (Vol. 6174, pp. 410–424). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_36\">https://doi.org/10.1007/978-3-642-14295-6_36</a>","ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Robustness in the presence of liveness. In: Touili T, Cook B, Jackson P, eds. Vol 6174. Springer; 2010:410-424. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_36\">10.1007/978-3-642-14295-6_36</a>","mla":"Bloem, Roderick, et al. <i>Robustness in the Presence of Liveness</i>. Edited by Tayssir Touili et al., vol. 6174, Springer, 2010, pp. 410–24, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_36\">10.1007/978-3-642-14295-6_36</a>.","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Robustness in the presence of liveness,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 410–424.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, T. Touili, B. Cook, P. Jackson (Eds.), Springer, 2010, pp. 410–424.","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2010. Robustness in the presence of liveness. CAV: Computer Aided Verification, LNCS, vol. 6174, 410–424.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Robustness in the Presence of Liveness.” edited by Tayssir Touili, Byron Cook, and Paul Jackson, 6174:410–24. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_36\">https://doi.org/10.1007/978-3-642-14295-6_36</a>."},"status":"public","file":[{"relation":"main_file","file_id":"5243","creator":"system","file_name":"IST-2012-54-v1+1_Robustness_in_the_presence_of_liveness.pdf","content_type":"application/pdf","file_size":213083,"checksum":"9d204611c8d7855bed8134f8708a0010","date_created":"2018-12-12T10:16:52Z","date_updated":"2020-07-14T12:46:19Z","access_level":"open_access"}],"publisher":"Springer","conference":{"end_date":"2010-07-19","start_date":"2010-07-15","name":"CAV: Computer Aided Verification","location":"Edinburgh, UK"},"ec_funded":1,"has_accepted_license":"1","scopus_import":1,"editor":[{"first_name":"Tayssir","last_name":"Touili","full_name":"Touili, Tayssir"},{"full_name":"Cook, Byron","last_name":"Cook","first_name":"Byron"},{"full_name":"Jackson, Paul","first_name":"Paul","last_name":"Jackson"}],"date_updated":"2021-01-12T07:52:47Z","author":[{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Karin","last_name":"Greimel","full_name":"Greimel, Karin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"}],"year":"2010","oa":1,"quality_controlled":"1","volume":6174,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","day":"01","alternative_title":["LNCS"],"publist_id":"2310","intvolume":"      6174","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2010-07-01T00:00:00Z","_id":"3866","pubrep_id":"54","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"month":"07","file_date_updated":"2020-07-14T12:46:19Z","type":"conference","abstract":[{"lang":"eng","text":"Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees."}],"date_created":"2018-12-11T12:05:36Z","doi":"10.1007/978-3-642-14295-6_36","oa_version":"Submitted Version","title":"Robustness in the presence of liveness","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"corr_author":"1","pubrep_id":"504","month":"08","file_date_updated":"2020-07-14T12:46:19Z","type":"journal_article","abstract":[{"lang":"eng","text":"Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages L that assign to each word w a real number L(w). In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the transition weights. The value of a word w is the supremum of the values of the runs over w. We study expressiveness and closure questions about these quantitative languages. We first show that the set of words with value greater than a threshold can be omega-regular for deterministic limit-average and discounted-sum automata, while this set is always omega-regular when the threshold is isolated (i.e., some neighborhood around the threshold contains no word). In the latter case, we prove that the omega-regular language is robust against small perturbations of the transition weights. We next consider automata with transition weights 0 or 1 and show that they are as expressive as general weighted automata in the limit-average case, but not in the discounted-sum case. Third, for quantitative languages L-1 and L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1 - L-1, which generalize the boolean operations on languages, as well as the sum L-1 + L-2. We establish the closure properties of all classes of quantitative languages with respect to these four operations."}],"external_id":{"isi":["000282653500010"]},"project":[{"call_identifier":"FP7","grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"}],"title":"Expressiveness and closure properties for quantitative languages","license":"https://creativecommons.org/licenses/by-nd/4.0/","date_created":"2018-12-11T12:05:36Z","doi":"10.2168/LMCS-6(3:10)2010","oa_version":"Published Version","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":"         6","publication_status":"published","publist_id":"2311","language":[{"iso":"eng"}],"date_published":"2010-08-30T00:00:00Z","_id":"3867","related_material":{"record":[{"id":"4540","relation":"earlier_version","status":"public"}]},"isi":1,"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)"},"quality_controlled":"1","oa":1,"volume":6,"issue":"3","day":"30","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","status":"public","publication":"Logical Methods in Computer Science","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness and Closure Properties for Quantitative Languages.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2010. <a href=\"https://doi.org/10.2168/LMCS-6(3:10)2010\">https://doi.org/10.2168/LMCS-6(3:10)2010</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2010. Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science. 6(3), 1–23.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Logical Methods in Computer Science 6 (2010) 1–23.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2010). Expressiveness and closure properties for quantitative languages. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-6(3:10)2010\">https://doi.org/10.2168/LMCS-6(3:10)2010</a>","mla":"Chatterjee, Krishnendu, et al. “Expressiveness and Closure Properties for Quantitative Languages.” <i>Logical Methods in Computer Science</i>, vol. 6, no. 3, International Federation of Computational Logic, 2010, pp. 1–23, doi:<a href=\"https://doi.org/10.2168/LMCS-6(3:10)2010\">10.2168/LMCS-6(3:10)2010</a>.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure properties for quantitative languages,” <i>Logical Methods in Computer Science</i>, vol. 6, no. 3. International Federation of Computational Logic, pp. 1–23, 2010.","ama":"Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties for quantitative languages. <i>Logical Methods in Computer Science</i>. 2010;6(3):1-23. doi:<a href=\"https://doi.org/10.2168/LMCS-6(3:10)2010\">10.2168/LMCS-6(3:10)2010</a>"},"ddc":["000","004"],"page":"1 - 23","publisher":"International Federation of Computational Logic","file":[{"content_type":"application/pdf","checksum":"0243da726476817f2ea33b48b78be696","file_size":216598,"date_updated":"2020-07-14T12:46:19Z","access_level":"open_access","date_created":"2018-12-12T10:17:54Z","file_name":"IST-2012-55-v1+1_Expressiveness_Closure_Properties_Quantitative_Languages.pdf","creator":"system","file_id":"5312","relation":"main_file"},{"relation":"main_file","file_id":"5313","creator":"system","file_name":"IST-2016-55-v2+1_1007.4018.pdf","date_created":"2018-12-12T10:17:55Z","access_level":"open_access","date_updated":"2020-07-14T12:46:19Z","content_type":"application/pdf","checksum":"5e512b8503a9cb263de26331c4ee9cf2","file_size":302416}],"scopus_import":"1","ec_funded":1,"has_accepted_license":"1","date_updated":"2025-09-30T09:31:00Z","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"year":"2010"},{"department":[{"_id":"KrCh"}],"title":"Algorithms for game metrics","article_processing_charge":"No","oa_version":"Published Version","date_created":"2018-12-11T12:05:36Z","doi":"10.2168/LMCS-6(3:13)2010","abstract":[{"lang":"eng","text":"Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative mu-calculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in long-run average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turn-based games and MDPs, we provide a polynomial-time algorithm for the computation of the one-step metric distance between states. The algorithm is based on linear programming; it improves on the previous known exponential-time algorithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n(4)) for both turn-based games and MDPs; improving the previously best known O(n(9).log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance be tween states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time complexity, improving the previously known reduction, which yielded O(vertical bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms can be iterated to approximate the metrics using binary search"}],"type":"journal_article","month":"09","file_date_updated":"2020-07-14T12:46:19Z","external_id":{"isi":["000282653500013"]},"corr_author":"1","pubrep_id":"370","isi":1,"_id":"3868","related_material":{"record":[{"id":"3504","relation":"earlier_version","status":"public"}]},"date_published":"2010-09-01T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","intvolume":"         6","publist_id":"2312","day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":6,"issue":"3","quality_controlled":"1","oa":1,"tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)"},"year":"2010","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"first_name":"Vishwanath","last_name":"Raman","full_name":"Raman, Vishwanath"}],"date_updated":"2025-09-30T09:31:30Z","scopus_import":"1","has_accepted_license":"1","file":[{"date_updated":"2020-07-14T12:46:19Z","access_level":"open_access","date_created":"2018-12-12T10:08:11Z","file_size":346527,"checksum":"a18988135fef3016c93808ecb15b55f5","content_type":"application/pdf","file_name":"IST-2015-370-v1+1_0809.4326.pdf","creator":"system","file_id":"4671","relation":"main_file"}],"publisher":"International Federation of Computational Logic","status":"public","publication":"Logical Methods in Computer Science","page":"1 - 27","citation":{"ista":"Chatterjee K, De Alfaro L, Majumdar R, Raman V. 2010. Algorithms for game metrics. Logical Methods in Computer Science. 6(3), 1–27.","short":"K. Chatterjee, L. De Alfaro, R. Majumdar, V. Raman, Logical Methods in Computer Science 6 (2010) 1–27.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, Ritankar Majumdar, and Vishwanath Raman. “Algorithms for Game Metrics.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2010. <a href=\"https://doi.org/10.2168/LMCS-6(3:13)2010\">https://doi.org/10.2168/LMCS-6(3:13)2010</a>.","apa":"Chatterjee, K., De Alfaro, L., Majumdar, R., &#38; Raman, V. (2010). Algorithms for game metrics. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-6(3:13)2010\">https://doi.org/10.2168/LMCS-6(3:13)2010</a>","ama":"Chatterjee K, De Alfaro L, Majumdar R, Raman V. Algorithms for game metrics. <i>Logical Methods in Computer Science</i>. 2010;6(3):1-27. doi:<a href=\"https://doi.org/10.2168/LMCS-6(3:13)2010\">10.2168/LMCS-6(3:13)2010</a>","ieee":"K. Chatterjee, L. De Alfaro, R. Majumdar, and V. Raman, “Algorithms for game metrics,” <i>Logical Methods in Computer Science</i>, vol. 6, no. 3. International Federation of Computational Logic, pp. 1–27, 2010.","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Game Metrics.” <i>Logical Methods in Computer Science</i>, vol. 6, no. 3, International Federation of Computational Logic, 2010, pp. 1–27, doi:<a href=\"https://doi.org/10.2168/LMCS-6(3:13)2010\">10.2168/LMCS-6(3:13)2010</a>."},"ddc":["000"]},{"language":[{"iso":"eng"}],"publist_id":"1068","publication_status":"published","intvolume":"      6174","_id":"4388","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5393"}]},"date_published":"2010-07-01T00:00:00Z","project":[{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"external_id":{"arxiv":["1004.2367"]},"abstract":[{"text":"GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.","lang":"eng"}],"month":"07","arxiv":1,"file_date_updated":"2020-07-14T12:46:28Z","type":"conference","pubrep_id":"43","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","doi":"10.1007/978-3-642-14295-6_57","oa_version":"Submitted Version","date_created":"2018-12-11T12:08:36Z","title":"GIST: A solver for probabilistic games","has_accepted_license":"1","ec_funded":1,"scopus_import":1,"publisher":"Springer","file":[{"creator":"system","file_name":"IST-2012-43-v1+1_GIST-_A_solver_for_probabilistic_games.pdf","relation":"main_file","file_id":"5221","access_level":"open_access","date_updated":"2020-07-14T12:46:28Z","date_created":"2018-12-12T10:16:33Z","content_type":"application/pdf","file_size":293605,"checksum":"0b2ef8c4037ffccc6902d93081af24f7"}],"conference":{"start_date":"2010-07-15","end_date":"2010-07-17","name":"CAV: Computer Aided Verification","location":"Edinburgh, UK"},"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun Radhakrishna. “GIST: A Solver for Probabilistic Games,” 6174:665–69. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">https://doi.org/10.1007/978-3-642-14295-6_57</a>.","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, in:, Springer, 2010, pp. 665–669.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2010. GIST: A solver for probabilistic games. CAV: Computer Aided Verification, LNCS, vol. 6174, 665–669.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Radhakrishna, A. (2010). GIST: A solver for probabilistic games (Vol. 6174, pp. 665–669). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">https://doi.org/10.1007/978-3-642-14295-6_57</a>","mla":"Chatterjee, Krishnendu, et al. <i>GIST: A Solver for Probabilistic Games</i>. Vol. 6174, Springer, 2010, pp. 665–69, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">10.1007/978-3-642-14295-6_57</a>.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, “GIST: A solver for probabilistic games,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 665–669.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. GIST: A solver for probabilistic games. In: Vol 6174. Springer; 2010:665-669. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">10.1007/978-3-642-14295-6_57</a>"},"ddc":["004"],"page":"665 - 669","status":"public","year":"2010","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"},{"full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2024-10-09T20:54:00Z","oa":1,"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"01","volume":6174},{"file":[{"content_type":"application/pdf","checksum":"fb7563150231325b00b1718d956f687b","file_size":311065,"date_updated":"2020-07-14T12:46:43Z","access_level":"open_access","date_created":"2018-12-12T11:54:08Z","file_name":"IST-2009-0004_IST-2009-0004.pdf","creator":"system","file_id":"5530","relation":"main_file"}],"publisher":"IST Austria","has_accepted_license":"1","status":"public","ddc":["005"],"page":"17","citation":{"mla":"Chatterjee, Krishnendu. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">10.15479/AT:IST-2009-0004</a>.","apa":"Chatterjee, K. (2009). <i>Probabilistic automata on infinite words: Decidability and undecidability results</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">https://doi.org/10.15479/AT:IST-2009-0004</a>","ama":"Chatterjee K. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">10.15479/AT:IST-2009-0004</a>","ieee":"K. Chatterjee, <i>Probabilistic automata on infinite words: Decidability and undecidability results</i>. IST Austria, 2009.","short":"K. Chatterjee, Probabilistic Automata on Infinite Words: Decidability and Undecidability Results, IST Austria, 2009.","chicago":"Chatterjee, Krishnendu. <i>Probabilistic Automata on Infinite Words: Decidability and Undecidability Results</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0004\">https://doi.org/10.15479/AT:IST-2009-0004</a>.","ista":"Chatterjee K. 2009. Probabilistic automata on infinite words: Decidability and undecidability results, IST Austria, 17p."},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"}],"year":"2009","date_updated":"2025-04-14T13:37:25Z","oa":1,"day":"02","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"relation":"later_version","id":"3857","status":"public"}]},"_id":"5392","date_published":"2009-11-02T00:00:00Z","type":"technical_report","month":"11","file_date_updated":"2020-07-14T12:46:43Z","abstract":[{"lang":"eng","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 of [GO09] and present a precise characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems."}],"publication_identifier":{"issn":["2664-1690"]},"corr_author":"1","pubrep_id":"28","department":[{"_id":"KrCh"}],"title":"Probabilistic automata on infinite words: Decidability and undecidability results","oa_version":"Published Version","doi":"10.15479/AT:IST-2009-0004","date_created":"2018-12-12T11:39:04Z"},{"oa":1,"day":"09","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","checksum":"49551ac552915b17593a14c993845274","file_size":386866,"date_created":"2018-12-12T11:52:58Z","access_level":"open_access","date_updated":"2020-07-14T12:46:43Z","file_id":"5459","relation":"main_file","file_name":"IST-2009-0003_IST-2009-0003.pdf","creator":"system"}],"publisher":"IST Austria","has_accepted_license":"1","status":"public","ddc":["000","005"],"citation":{"short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, Gist: A Solver for Probabilistic Games, IST Austria, 2009.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2009. Gist: A solver for probabilistic games, IST Austria, 12p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun Radhakrishna. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">https://doi.org/10.15479/AT:IST-2009-0003</a>.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, <i>Gist: A solver for probabilistic games</i>. IST Austria, 2009.","mla":"Chatterjee, Krishnendu, et al. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">10.15479/AT:IST-2009-0003</a>.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Radhakrishna, A. (2009). <i>Gist: A solver for probabilistic games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">https://doi.org/10.15479/AT:IST-2009-0003</a>","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0003\">10.15479/AT:IST-2009-0003</a>"},"page":"12","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"year":"2009","date_updated":"2025-04-14T13:37:27Z","file_date_updated":"2020-07-14T12:46:43Z","month":"10","type":"technical_report","abstract":[{"lang":"eng","text":"Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides efficient implementations of several reduction based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications."}],"publication_identifier":{"issn":["2664-1690"]},"pubrep_id":"29","corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Gist: A solver for probabilistic games","doi":"10.15479/AT:IST-2009-0003","date_created":"2018-12-12T11:39:05Z","oa_version":"Published Version","language":[{"iso":"eng"}],"publication_status":"published","_id":"5393","related_material":{"record":[{"status":"public","relation":"later_version","id":"4388"}]},"date_published":"2009-10-09T00:00:00Z"},{"language":[{"iso":"eng"}],"publisher":"IST Austria","file":[{"content_type":"application/pdf","file_size":238091,"checksum":"1c50a9723fbae1b2c46d18138968efb3","date_updated":"2020-07-14T12:46:43Z","access_level":"open_access","date_created":"2018-12-12T11:53:50Z","creator":"system","file_name":"IST-2009-0002_IST-2009-0002.pdf","relation":"main_file","file_id":"5511"}],"has_accepted_license":"1","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). <i>Improved lower bounds for request-response and finitary Streett games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">https://doi.org/10.15479/AT:IST-2009-0002</a>","mla":"Chatterjee, Krishnendu, et al. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">10.15479/AT:IST-2009-0002</a>.","ama":"Chatterjee K, Henzinger TA, Horn F. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">10.15479/AT:IST-2009-0002</a>","ieee":"K. Chatterjee, T. A. Henzinger, and F. Horn, <i>Improved lower bounds for request-response and finitary Streett games</i>. IST Austria, 2009.","ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Improved lower bounds for request-response and finitary Streett games, IST Austria, 11p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. <i>Improved Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0002\">https://doi.org/10.15479/AT:IST-2009-0002</a>.","short":"K. Chatterjee, T.A. Henzinger, F. Horn, Improved Lower Bounds for Request-Response and Finitary Streett Games, IST Austria, 2009."},"ddc":["004"],"page":"11","status":"public","publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","first_name":"Florian","last_name":"Horn","full_name":"Horn, Florian"}],"year":"2009","_id":"5394","date_published":"2009-09-09T00:00:00Z","date_updated":"2024-10-09T21:08:23Z","oa":1,"type":"technical_report","file_date_updated":"2020-07-14T12:46:43Z","month":"09","abstract":[{"text":"We consider two-player games played on graphs with request-response and finitary Streett objectives. We show these games are PSPACE-hard, improving the previous known NP-hardness. We also improve the lower bounds on memory required by the winning strategies for the players.","lang":"eng"}],"pubrep_id":"30","corr_author":"1","publication_identifier":{"issn":["2664-1690"]},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"09","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","date_created":"2018-12-12T11:39:05Z","doi":"10.15479/AT:IST-2009-0002","title":"Improved lower bounds for request-response and finitary Streett games"},{"pubrep_id":"31","corr_author":"1","publication_identifier":{"issn":["2664-1690"]},"abstract":[{"lang":"eng","text":"We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with omega-regular objectives. An observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observa- tions. We consider the qualitative analysis problem: given a POMDP with an omega-regular objective, whether there is an observation-based strategy to achieve the objective with probability 1 (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis of POMDPs with parity objectives (a canonical form to express omega-regular objectives) and its subclasses. Our contribution consists in establishing several upper and lower bounds that were not known in literature. Second, we present optimal bounds (matching upper and lower bounds) on the memory required by pure and randomized observation-based strategies for the qualitative analysis of POMDPs with parity objectives and its subclasses."}],"month":"09","type":"technical_report","file_date_updated":"2020-07-14T12:46:43Z","doi":"10.15479/AT:IST-2009-0001","oa_version":"Published Version","date_created":"2018-12-12T11:39:05Z","title":"Qualitative analysis of partially-observable Markov decision processes","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","language":[{"iso":"eng"}],"date_published":"2009-09-09T00:00:00Z","related_material":{"record":[{"status":"public","id":"3855","relation":"later_version"}]},"_id":"5395","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"day":"09","page":"20","ddc":["005"],"citation":{"short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Qualitative Analysis of Partially-Observable Markov Decision Processes, IST Austria, 2009.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Qualitative analysis of partially-observable Markov decision processes, IST Austria, 20p.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria, 2009. <a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">https://doi.org/10.15479/AT:IST-2009-0001</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria, 2009, doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">10.15479/AT:IST-2009-0001</a>.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). <i>Qualitative analysis of partially-observable Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">https://doi.org/10.15479/AT:IST-2009-0001</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, <i>Qualitative analysis of partially-observable Markov decision processes</i>. IST Austria, 2009.","ama":"Chatterjee K, Doyen L, Henzinger TA. <i>Qualitative Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria; 2009. doi:<a href=\"https://doi.org/10.15479/AT:IST-2009-0001\">10.15479/AT:IST-2009-0001</a>"},"status":"public","has_accepted_license":"1","file":[{"checksum":"04d9cc065cc19598a4e8631c47f1a562","file_size":342088,"content_type":"application/pdf","date_created":"2018-12-12T11:53:25Z","date_updated":"2020-07-14T12:46:43Z","access_level":"open_access","file_id":"5486","relation":"main_file","file_name":"IST-2009-0001_IST-2009-0001.pdf","creator":"system"}],"publisher":"IST Austria","date_updated":"2025-04-14T13:37:25Z","year":"2009","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}]},{"acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the NSF grants CCR-0132780, CNS-0720884, and CCR- 225610, by the Swiss National Science Foundation, by the COMBEST project of the European Union, and EU-TMR network Games.\r\nWe thank anonymous reviewers for useful comments.","pubrep_id":"53","corr_author":"1","external_id":{"isi":["000272039900001"]},"project":[{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"}],"file_date_updated":"2020-07-14T12:46:20Z","month":"10","type":"journal_article","abstract":[{"text":"Games on graphs with omega-regular objectives provide a model for the control and synthesis of reactive systems. Every omega-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Buchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. We show that finitary parity games can be solved in polynomial time, which is not known for infinitary parity games. For finitary Streett games, we give an EXPTIME algorithm and show that the problem is NP-hard. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound.","lang":"eng"}],"doi":"10.1145/1614431.1614432","date_created":"2018-12-11T12:05:37Z","oa_version":"Submitted Version","article_processing_charge":"No","title":"Finitary winning in omega-regular games","department":[{"_id":"KrCh"}],"publist_id":"2309","intvolume":"        11","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2009-10-01T00:00:00Z","_id":"3870","isi":1,"oa":1,"quality_controlled":"1","issue":"1","volume":11,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"01","article_number":"1","ddc":["004"],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Finitary Winning in Omega-Regular Games.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 11, no. 1, 1, ACM, 2009, doi:<a href=\"https://doi.org/10.1145/1614431.1614432\">10.1145/1614431.1614432</a>.","ama":"Chatterjee K, Henzinger TA, Horn F. Finitary winning in omega-regular games. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2009;11(1). doi:<a href=\"https://doi.org/10.1145/1614431.1614432\">10.1145/1614431.1614432</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). Finitary winning in omega-regular games. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/1614431.1614432\">https://doi.org/10.1145/1614431.1614432</a>","ieee":"K. Chatterjee, T. A. Henzinger, and F. Horn, “Finitary winning in omega-regular games,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 11, no. 1. ACM, 2009.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Finitary Winning in Omega-Regular Games.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2009. <a href=\"https://doi.org/10.1145/1614431.1614432\">https://doi.org/10.1145/1614431.1614432</a>.","short":"K. Chatterjee, T.A. Henzinger, F. Horn, ACM Transactions on Computational Logic (TOCL) 11 (2009).","ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Finitary winning in omega-regular games. ACM Transactions on Computational Logic (TOCL). 11(1), 1."},"status":"public","publication":"ACM Transactions on Computational Logic (TOCL)","file":[{"content_type":"application/pdf","file_size":180082,"checksum":"139c4586d24f11e5da31fb3a0cf96ef4","date_created":"2018-12-12T10:15:08Z","date_updated":"2020-07-14T12:46:20Z","access_level":"open_access","file_id":"5125","relation":"main_file","file_name":"IST-2012-53-v1+1_Finitary_winning_in_omega-regular_games.pdf","creator":"system"}],"publisher":"ACM","scopus_import":"1","has_accepted_license":"1","ec_funded":1,"date_updated":"2025-09-30T09:53:52Z","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Horn, Florian","first_name":"Florian","last_name":"Horn","id":"37327ACE-F248-11E8-B48F-1D18A9856A87"}],"year":"2009"},{"language":[{"iso":"eng"}],"publist_id":"2304","intvolume":"      5710","publication_status":"published","_id":"3871","date_published":"2009-09-01T00:00:00Z","project":[{"call_identifier":"FP7","grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"type":"conference","file_date_updated":"2020-07-14T12:46:20Z","month":"09","abstract":[{"lang":"eng","text":"Nondeterministic weighted automata are finite automata with numerical weights oil transitions. They define quantitative languages 1, that assign to each word v; a real number L(w). The value of ail infinite word w is computed as the maximal value of all runs over w, and the value of a run as the supremum, limsup liminf, limit average, or discounted sum of the transition weights. We introduce probabilistic weighted antomata, in which the transitions are chosen in a randomized (rather than nondeterministic) fashion. Under almost-sure semantics (resp. positive semantics), the value of a word v) is the largest real v such that the runs over w have value at least v with probability I (resp. positive probability). We study the classical questions of automata theory for probabilistic weighted automata: emptiness and universality, expressiveness, and closure under various operations oil languages. For quantitative languages, emptiness university axe defined as whether the value of some (resp. every) word exceeds a given threshold. We prove some, of these questions to he decidable, and others undecidable. Regarding expressive power, we show that probabilities allow its to define a wide variety of new classes of quantitative languages except for discounted-sum automata, where probabilistic choice is no more expressive than nondeterminism. Finally we live ail almost complete picture of the closure of various classes of probabilistic weighted automata for the following, provide, is operations oil quantitative languages: maximum, sum. and numerical complement."}],"acknowledgement":"This research was supported in part by the Swiss National Science Foundation under the Indo-Swiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), by the European projects Combest, Quasimodo, and Gasics, by the PAI program Moves funded by the Belgian Federal Government, and by the CFV (Federated Center in Verification ) funded by the F.R.S.-FNRS.","pubrep_id":"52","corr_author":"1","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T12:05:37Z","oa_version":"Submitted Version","doi":"10.1007/978-3-642-04081-8_17","title":"Probabilistic weighted automata","conference":{"name":"CONCUR: Concurrency Theory","end_date":"2009-09-04","start_date":"2009-09-01","location":"Bologna, Italy"},"publisher":"Springer","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:46:20Z","date_created":"2018-12-12T10:09:46Z","content_type":"application/pdf","file_size":200161,"checksum":"af973ddbcf131b8810c6bff2c055ff56","creator":"system","file_name":"IST-2012-52-v1+1_Probabilistic_Weighted_Automata.pdf","relation":"main_file","file_id":"4771"}],"has_accepted_license":"1","ec_funded":1,"scopus_import":1,"citation":{"apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Probabilistic weighted automata (Vol. 5710, pp. 244–258). Presented at the CONCUR: Concurrency Theory, Bologna, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-642-04081-8_17\">https://doi.org/10.1007/978-3-642-04081-8_17</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Probabilistic weighted automata,” presented at the CONCUR: Concurrency Theory, Bologna, Italy, 2009, vol. 5710, pp. 244–258.","ama":"Chatterjee K, Doyen L, Henzinger TA. Probabilistic weighted automata. In: Vol 5710. Springer; 2009:244-258. doi:<a href=\"https://doi.org/10.1007/978-3-642-04081-8_17\">10.1007/978-3-642-04081-8_17</a>","mla":"Chatterjee, Krishnendu, et al. <i>Probabilistic Weighted Automata</i>. Vol. 5710, Springer, 2009, pp. 244–58, doi:<a href=\"https://doi.org/10.1007/978-3-642-04081-8_17\">10.1007/978-3-642-04081-8_17</a>.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Probabilistic Weighted Automata,” 5710:244–58. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-04081-8_17\">https://doi.org/10.1007/978-3-642-04081-8_17</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 244–258.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Probabilistic weighted automata. CONCUR: Concurrency Theory, LNCS, vol. 5710, 244–258."},"ddc":["000","005"],"page":"244 - 258","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"year":"2009","date_updated":"2024-10-09T20:53:56Z","oa":1,"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","alternative_title":["LNCS"],"volume":5710},{"department":[{"_id":"KrCh"}],"oa_version":"Submitted Version","date_created":"2018-12-11T12:09:23Z","doi":"10.1007/978-3-642-03409-1_2","title":"Alternating weighted automata","project":[{"name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"abstract":[{"text":"Weighted automata are finite automata with numerical weights on transitions. Nondeterministic weighted automata define quantitative languages L that assign to each word w a real number L(w) computed as the maximal value of all runs over w, and the value of a run r is a function of the sequence of weights that appear along r. There are several natural functions to consider such as Sup, LimSup, LimInf, limit average, and discounted sum of transition weights.\r\nWe introduce alternating weighted automata in which the transitions of the runs are chosen by two players in a turn-based fashion. Each word is assigned the maximal value of a run that the first player can enforce regardless of the choices made by the second player. We survey the results about closure properties, expressiveness, and decision problems for nondeterministic weighted automata, and we extend these results to alternating weighted automata.\r\nFor quantitative languages L 1 and L 2, we consider the pointwise operations max(L 1,L 2), min(L 1,L 2), 1 − L 1, and the sum L 1 + L 2. We establish the closure properties of all classes of alternating weighted automata with respect to these four operations.\r\nWe next compare the expressive power of the various classes of alternating and nondeterministic weighted automata over infinite words. In particular, for limit average and discounted sum, we show that alternation brings more expressive power than nondeterminism.\r\nFinally, we present decidability results and open questions for the quantitative extension of the classical decision problems in automata theory: emptiness, universality, language inclusion, and language equivalence.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:31Z","type":"conference","month":"09","corr_author":"1","pubrep_id":"39","acknowledgement":"This research was supported in part by the Swiss National Science Foundation under the Indo-Swiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), by the European Combest, Quasimodo, and Gasics projects, by the PAI program Moves funded by the Belgian Federal Government, and by the CFV (Federated Center in Verification) funded by the F.R.S.-FNRS.","_id":"4542","date_published":"2009-09-10T00:00:00Z","language":[{"iso":"eng"}],"publist_id":"180","publication_status":"published","intvolume":"      5699","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"10","volume":5699,"oa":1,"quality_controlled":"1","year":"2009","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"date_updated":"2024-10-09T20:53:55Z","scopus_import":1,"ec_funded":1,"has_accepted_license":"1","file":[{"date_created":"2018-12-12T10:15:09Z","access_level":"open_access","date_updated":"2020-07-14T12:46:31Z","content_type":"application/pdf","checksum":"e8f53abb63579de3f2bff58b2a1188e2","file_size":164428,"file_id":"5126","relation":"main_file","file_name":"IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf","creator":"system"}],"publisher":"Springer","conference":{"start_date":"2009-09-02","end_date":"2009-09-04","name":"FCT: Fundamentals of Computation Theory","location":"Wroclaw, Poland"},"ddc":["004"],"page":"3 - 13","citation":{"short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Alternating Weighted Automata,” 5699:3–13. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata. FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13.","ama":"Chatterjee K, Doyen L, Henzinger TA. Alternating weighted automata. In: Vol 5699. Springer; 2009:3-13. doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>","mla":"Chatterjee, Krishnendu, et al. <i>Alternating Weighted Automata</i>. Vol. 5699, Springer, 2009, pp. 3–13, doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “Alternating weighted automata,” presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland, 2009, vol. 5699, pp. 3–13.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Alternating weighted automata (Vol. 5699, pp. 3–13). Presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>"},"status":"public"},{"day":"01","alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":5734,"quality_controlled":"1","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","last_name":"Horn","first_name":"Florian","full_name":"Horn, Florian"}],"year":"2009","date_updated":"2024-10-09T20:53:54Z","publisher":"Springer","conference":{"location":"High Tatras, Slovakia","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2009-08-24","end_date":"2009-08-28"},"scopus_import":1,"ec_funded":1,"status":"public","citation":{"short":"K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, pp. 34–54.","ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734, 34–54.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Stochastic Games with Finitary Objectives,” 5734:34–54. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>.","ama":"Chatterjee K, Henzinger TA, Horn F. Stochastic games with finitary objectives. In: Vol 5734. Springer; 2009:34-54. doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Games with Finitary Objectives</i>. Vol. 5734, Springer, 2009, pp. 34–54, doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and F. Horn, “Stochastic games with finitary objectives,” presented at the MFCS: Mathematical Foundations of Computer Science, High Tatras, Slovakia, 2009, vol. 5734, pp. 34–54.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). Stochastic games with finitary objectives (Vol. 5734, pp. 34–54). Presented at the MFCS: Mathematical Foundations of Computer Science, High Tatras, Slovakia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>"},"page":"34 - 54","department":[{"_id":"KrCh"}],"title":"Stochastic games with finitary objectives","date_created":"2018-12-11T12:09:24Z","oa_version":"None","doi":"10.1007/978-3-642-03816-7_4","type":"conference","month":"08","abstract":[{"text":"The synthesis of a reactive system with respect to all omega-regular specification requires the solution of a graph game. Such games have been extended in two natural ways. First, a game graph can be equipped with probabilistic choices between alternative transitions, thus allowing the, modeling of uncertain behaviour. These are called stochastic games. Second, a liveness specification can he strengthened to require satisfaction within all unknown but bounded amount of time. These are called finitary objectives. We study. for the first time, the, combination of Stochastic games and finitary objectives. We characterize the requirements on optimal strategies and provide algorithms for Computing the maximal achievable probability of winning stochastic games with finitary parity or Street, objectives. Most notably the set of state's from which a player can win with probability . for a finitary parity objective can he computed in polynomial time even though no polynomial-time algorithm is known in the nonfinitary case.","lang":"eng"}],"project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This research was supported in part by the Swiss National Science Foundation under the Indo-Swiss Joint Research Programme, by the European Network of Excellence on Embedded Systems Design (ArtistDesign), and by the European project Combest.","corr_author":"1","_id":"4543","date_published":"2009-08-01T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"      5734","publication_status":"published","publist_id":"178"}]