[{"publist_id":"5837","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fijalkow, Nathanaël","last_name":"Fijalkow","first_name":"Nathanaël"}],"title":"Infinite-state games with finitary conditions","citation":{"ista":"Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions. 22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196.","chicago":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” In 22nd EACSL Annual Conference on Computer Science Logic, 23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.181.","ieee":"K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,” in 22nd EACSL Annual Conference on Computer Science Logic, Torino, Italy, 2013, vol. 23, pp. 181–196.","short":"K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.","apa":"Chatterjee, K., & Fijalkow, N. (2013). Infinite-state games with finitary conditions. In 22nd EACSL Annual Conference on Computer Science Logic (Vol. 23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.181","ama":"Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In: 22nd EACSL Annual Conference on Computer Science Logic. Vol 23. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2013:181-196. doi:10.4230/LIPIcs.CSL.2013.181","mla":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” 22nd EACSL Annual Conference on Computer Science Logic, vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96, doi:10.4230/LIPIcs.CSL.2013.181."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"page":"181 - 196","date_published":"2013-09-01T00:00:00Z","doi":"10.4230/LIPIcs.CSL.2013.181","date_created":"2018-12-11T11:51:39Z","has_accepted_license":"1","year":"2013","day":"01","publication":"22nd EACSL Annual Conference on Computer Science Logic","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1,"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:47Z","date_updated":"2021-01-12T06:50:14Z","ddc":["000"],"type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"203-09-02","location":"Torino, Italy","end_date":"2013-09-05","name":"CSL: Computer Science Logic"},"status":"public","pubrep_id":"624","_id":"1374","series_title":"Leibniz International Proceedings in Informatics","volume":23,"license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"publication_status":"published","file":[{"date_created":"2018-12-12T10:13:38Z","file_name":"IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf","creator":"system","date_updated":"2020-07-14T12:44:47Z","file_size":547296,"file_id":"5023","checksum":"b7091a3866db573c0db5ec486952255e","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"scopus_import":1,"alternative_title":["LIPIcs"],"month":"09","intvolume":" 23","abstract":[{"lang":"eng","text":"We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete."}],"oa_version":"Published Version"},{"project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"title":"Multi-objective discounted reward verification in graphs and MDPs","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Vojtěch","last_name":"Forejt","full_name":"Forejt, Vojtěch"},{"first_name":"Dominik","full_name":"Wojtczak, Dominik","last_name":"Wojtczak"}],"publist_id":"4723","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward verification in graphs and MDPs. 8312, 228–242.","chicago":"Chatterjee, Krishnendu, Vojtěch Forejt, and Dominik Wojtczak. “Multi-Objective Discounted Reward Verification in Graphs and MDPs.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_17.","apa":"Chatterjee, K., Forejt, V., & Wojtczak, D. (2013). Multi-objective discounted reward verification in graphs and MDPs. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_17","ama":"Chatterjee K, Forejt V, Wojtczak D. Multi-objective discounted reward verification in graphs and MDPs. 2013;8312:228-242. doi:10.1007/978-3-642-45221-5_17","ieee":"K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013.","short":"K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242.","mla":"Chatterjee, Krishnendu, et al. Multi-Objective Discounted Reward Verification in Graphs and MDPs. Vol. 8312, Springer, 2013, pp. 228–42, doi:10.1007/978-3-642-45221-5_17."},"publisher":"Springer","quality_controlled":"1","date_created":"2018-12-11T11:56:30Z","date_published":"2013-12-01T00:00:00Z","doi":"10.1007/978-3-642-45221-5_17","page":"228 - 242","day":"01","year":"2013","status":"public","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","end_date":"2013-12-19","location":"Stellenbosch, South Africa","start_date":"2013-12-14"},"type":"conference","_id":"2238","series_title":"Lecture Notes in Computer Science","department":[{"_id":"KrCh"}],"date_updated":"2020-08-11T10:09:42Z","intvolume":" 8312","month":"12","alternative_title":["LNCS"],"scopus_import":1,"oa_version":"None","abstract":[{"text":"We study the problem of achieving a given value in Markov decision processes (MDPs) with several independent discounted reward objectives. We consider a generalised version of discounted reward objectives, in which the amount of discounting depends on the states visited and on the objective. This definition extends the usual definition of discounted reward, and allows to capture the systems in which the value of different commodities diminish at different and variable rates.\r\n\r\nWe establish results for two prominent subclasses of the problem, namely state-discount models where the discount factors are only dependent on the state of the MDP (and independent of the objective), and reward-discount models where they are only dependent on the objective (but not on the state of the MDP). For the state-discount models we use a straightforward reduction to expected total reward and show that the problem whether a value is achievable can be solved in polynomial time. For the reward-discount model we show that memory and randomisation of the strategies are required, but nevertheless that the problem is decidable and it is sufficient to consider strategies which after a certain number of steps behave in a memoryless way.\r\n\r\nFor the general case, we show that when restricted to graphs (i.e. MDPs with no randomisation), pure strategies and discount factors of the form 1/n where n is an integer, the problem is in PSPACE and finite memory suffices for achieving a given value. We also show that when the discount factors are not of the form 1/n, the memory required by a strategy can be infinite.\r\n","lang":"eng"}],"ec_funded":1,"volume":8312,"language":[{"iso":"eng"}],"publication_status":"published"},{"editor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Sgall, Jiri","last_name":"Sgall","first_name":"Jiri"}],"title":"Mathematical Foundations of Computer Science 2013","department":[{"_id":"KrCh"}],"publist_id":"4636","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2020-08-11T10:09:45Z","citation":{"mla":"Chatterjee, Krishnendu, and Jiri Sgall, editors. Mathematical Foundations of Computer Science 2013. Vol. 8087, Springer, 2013, p. VI-854, doi:10.1007/978-3-642-40313-2.","short":"K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science 2013, Springer, 2013.","ieee":"K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer Science 2013, vol. 8087. Springer, 2013, p. VI-854.","ama":"Chatterjee K, Sgall J, eds. Mathematical Foundations of Computer Science 2013. Vol 8087. Springer; 2013:VI-854. doi:10.1007/978-3-642-40313-2","apa":"Chatterjee, K., & Sgall, J. (Eds.). (2013). Mathematical Foundations of Computer Science 2013 (Vol. 8087, p. VI-854). Presented at the MFCS: Mathematical Foundations of Computer Science, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40313-2","chicago":"Chatterjee, Krishnendu, and Jiri Sgall, eds. Mathematical Foundations of Computer Science 2013. Vol. 8087. Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40313-2.","ista":"Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science 2013, Springer,p."},"status":"public","type":"conference_editor","conference":{"start_date":"2013-08-26","end_date":"2013-08-30","location":"Klosterneuburg, Austria","name":"MFCS: Mathematical Foundations of Computer Science"},"_id":"2292","series_title":"Lecture Notes in Computer Science","date_published":"2013-08-08T00:00:00Z","volume":8087,"doi":"10.1007/978-3-642-40313-2","date_created":"2018-12-11T11:56:48Z","page":"VI - 854","day":"08","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-3-642-40312-5"]},"publication_status":"published","year":"2013","month":"08","intvolume":" 8087","quality_controlled":"1","publisher":"Springer","alternative_title":["LNCS"],"scopus_import":1,"oa_version":"None","abstract":[{"text":"This book constitutes the thoroughly refereed conference proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013, held in Klosterneuburg, Austria, in August 2013. The 67 revised full papers presented together with six invited talks were carefully selected from 191 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence.","lang":"eng"}]},{"author":[{"last_name":"Godhal","full_name":"Godhal, Yashdeep","first_name":"Yashdeep","id":"5B547124-EB61-11E9-8887-89D9C04DBDF5"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"4629","title":"Synthesis of AMBA AHB from formal specification: A case study","citation":{"ista":"Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 15(5–6), 585–601.","chicago":"Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.","apa":"Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9","ama":"Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9","ieee":"Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from formal specification: A case study,” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.","short":"Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601.","mla":"Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"page":"585 - 601","date_published":"2013-10-01T00:00:00Z","doi":"10.1007/s10009-011-0207-9","date_created":"2018-12-11T11:56:51Z","has_accepted_license":"1","year":"2013","day":"01","publication":"International Journal on Software Tools for Technology Transfer","quality_controlled":"1","publisher":"Springer","oa":1,"file_date_updated":"2020-07-14T12:45:37Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2021-01-12T06:56:37Z","ddc":["000"],"type":"journal_article","status":"public","pubrep_id":"87","_id":"2299","issue":"5-6","volume":15,"publication_status":"published","file":[{"file_name":"IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf","date_created":"2018-12-12T10:11:53Z","file_size":277372,"date_updated":"2020-07-14T12:45:37Z","creator":"system","file_id":"4910","checksum":"57b06a732dd8d6349190dba6b5b0d33b","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"scopus_import":1,"month":"10","intvolume":" 15","abstract":[{"text":"The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol.","lang":"eng"}],"oa_version":"Submitted Version"},{"title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","external_id":{"arxiv":["1304.5281"]},"publist_id":"4457","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Gaiser","full_name":"Gaiser, Andreas","first_name":"Andreas"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_37.","ista":"Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.","mla":"Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37.","ama":"Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37","apa":"Chatterjee, K., Gaiser, A., & Kretinsky, J. (2013). Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_37","ieee":"K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013.","short":"K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575."},"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_created":"2018-12-11T11:57:42Z","date_published":"2013-07-01T00:00:00Z","doi":"10.1007/978-3-642-39799-8_37","page":"559 - 575","day":"01","year":"2013","oa":1,"publisher":"Springer","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_updated":"2020-08-11T10:09:47Z","status":"public","conference":{"location":"St. Petersburg, Russia","end_date":"2013-07-19","start_date":"2013-07-13","name":"CAV: Computer Aided Verification"},"type":"conference","_id":"2446","series_title":"Lecture Notes in Computer Science","ec_funded":1,"volume":8044,"language":[{"iso":"eng"}],"publication_status":"published","intvolume":" 8044","month":"07","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1304.5281"}],"alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Preprint","abstract":[{"lang":"eng","text":"The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements."}]}]