--- _id: '2039' abstract: - lang: eng text: 'A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time.' article_number: 7p author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Ben full_name: Adlam, Ben last_name: Adlam - first_name: Martin full_name: Nowak, Martin last_name: Nowak citation: ama: Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. PLoS Computational Biology. 2014;10(9). doi:10.1371/journal.pcbi.1003818 apa: Chatterjee, K., Pavlogiannis, A., Adlam, B., & Nowak, M. (2014). The time scale of evolutionary innovation. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818 chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology. Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818. ieee: K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” PLoS Computational Biology, vol. 10, no. 9. Public Library of Science, 2014. ista: Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p. mla: Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818. short: K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014). date_created: 2018-12-11T11:55:22Z date_published: 2014-09-11T00:00:00Z date_updated: 2023-02-23T14:06:36Z day: '11' ddc: - '510' department: - _id: KrCh doi: 10.1371/journal.pcbi.1003818 ec_funded: 1 file: - access_level: open_access checksum: 712d4c5787ddf97809cfc962507f0738 content_type: application/pdf creator: system date_created: 2018-12-12T10:11:35Z date_updated: 2020-07-14T12:45:26Z file_id: '4890' file_name: IST-2016-440-v1+1_journal.pcbi.1003818.pdf file_size: 1399093 relation: main_file file_date_updated: 2020-07-14T12:45:26Z has_accepted_license: '1' intvolume: ' 10' issue: '9' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: PLoS Computational Biology publication_status: published publisher: Public Library of Science publist_id: '5012' pubrep_id: '440' quality_controlled: '1' related_material: record: - id: '9739' relation: research_data status: public scopus_import: 1 status: public title: The time scale of evolutionary innovation tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 10 year: '2014' ... --- _id: '9739' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Ben full_name: Adlam, Ben last_name: Adlam - first_name: Martin full_name: Novak, Martin last_name: Novak citation: ama: Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:10.1371/journal.pcbi.1003818.s001 apa: Chatterjee, K., Pavlogiannis, A., Adlam, B., & Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818.s001 chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.s001. ieee: K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014. ista: Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, 10.1371/journal.pcbi.1003818.s001. mla: Chatterjee, Krishnendu, et al. Detailed Proofs for “The Time Scale of Evolutionary Innovation.” Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.s001. short: K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014). date_created: 2021-07-28T08:13:57Z date_published: 2014-09-11T00:00:00Z date_updated: 2023-02-23T10:25:37Z day: '11' department: - _id: KrCh doi: 10.1371/journal.pcbi.1003818.s001 month: '09' oa_version: Published Version publisher: Public Library of Science related_material: record: - id: '2039' relation: used_in_publication status: public status: public title: Detailed proofs for “The time scale of evolutionary innovation” type: research_data_reference user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf year: '2014' ... --- _id: '535' abstract: - lang: eng text: Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help. article_processing_charge: No article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Sebastian full_name: Krinninger, Sebastian last_name: Krinninger - first_name: Danupon full_name: Nanongkai, Danupon last_name: Nanongkai citation: ama: Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 2014;70(3):457-492. doi:10.1007/s00453-013-9843-7 apa: Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2014). Polynomial-time algorithms for energy games with special weight structures. Algorithmica. Springer. https://doi.org/10.1007/s00453-013-9843-7 chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7. ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” Algorithmica, vol. 70, no. 3. Springer, pp. 457–492, 2014. ista: Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2014. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 70(3), 457–492. mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer, 2014, pp. 457–92, doi:10.1007/s00453-013-9843-7. short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492. date_created: 2018-12-11T11:47:01Z date_published: 2014-11-01T00:00:00Z date_updated: 2023-09-05T14:09:29Z day: '01' department: - _id: KrCh doi: 10.1007/s00453-013-9843-7 ec_funded: 1 external_id: arxiv: - '1604.08234' intvolume: ' 70' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.08234 month: '11' oa: 1 oa_version: Preprint page: 457 - 492 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: Algorithmica publication_status: published publisher: Springer publist_id: '7282' quality_controlled: '1' related_material: record: - id: '10905' relation: earlier_version status: public scopus_import: '1' status: public title: Polynomial-time algorithms for energy games with special weight structures type: journal_article user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd volume: 70 year: '2014' ... --- _id: '2063' abstract: - lang: eng text: We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca citation: ama: 'Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31' apa: 'Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31' chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31. ieee: 'K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.' ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.' mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31. short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490. conference: end_date: 2014-07-22 location: Vienna, Austria name: 'CAV: Computer Aided Verification' start_date: 2014-07-18 date_created: 2018-12-11T11:55:30Z date_published: 2014-07-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-08867-9_31 ec_funded: 1 intvolume: ' 8559' language: - iso: eng month: '07' oa_version: None page: 473 - 490 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _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 - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '4978' quality_controlled: '1' related_material: record: - id: '5412' relation: earlier_version status: public - id: '5413' relation: earlier_version status: public - id: '5414' relation: earlier_version status: public - id: '1155' relation: dissertation_contains status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ... --- _id: '5428' abstract: - lang: eng text: "Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata." alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop - first_name: Yaron full_name: Velner, Yaron last_name: Velner citation: ama: Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1 apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1. ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair simulation games. IST Austria, 2014. ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p. mla: Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1. short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014. date_created: 2018-12-12T11:39:16Z date_published: 2014-12-05T00:00:00Z date_updated: 2023-09-20T12:07:48Z day: '05' ddc: - '004' department: - _id: ToHe - _id: KrCh doi: 10.15479/AT:IST-2014-315-v1-1 file: - access_level: open_access checksum: b1d573bc04365625ff9974880c0aa807 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:59Z date_updated: 2020-07-14T12:46:52Z file_id: '5521' file_name: IST-2014-315-v1+1_report.pdf file_size: 531046 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '26' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '315' related_material: record: - id: '1066' relation: later_version status: public status: public title: Quantitative fair simulation games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '1374' 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.' alternative_title: - LIPIcs author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Nathanaël full_name: Fijalkow, Nathanaël last_name: Fijalkow citation: 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' 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' 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. 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.' 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. 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. conference: end_date: 2013-09-05 location: Torino, Italy name: 'CSL: Computer Science Logic' start_date: 203-09-02 date_created: 2018-12-11T11:51:39Z date_published: 2013-09-01T00:00:00Z date_updated: 2021-01-12T06:50:14Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.CSL.2013.181 ec_funded: 1 file: - access_level: open_access checksum: b7091a3866db573c0db5ec486952255e content_type: application/pdf creator: system date_created: 2018-12-12T10:13:38Z date_updated: 2020-07-14T12:44:47Z file_id: '5023' file_name: IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf file_size: 547296 relation: main_file file_date_updated: 2020-07-14T12:44:47Z has_accepted_license: '1' intvolume: ' 23' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 181 - 196 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: 22nd EACSL Annual Conference on Computer Science Logic publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '5837' pubrep_id: '624' quality_controlled: '1' scopus_import: 1 series_title: Leibniz International Proceedings in Informatics status: public title: Infinite-state games with finitary conditions tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 23 year: '2013' ... --- _id: '2238' abstract: - lang: eng 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" alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Dominik full_name: Wojtczak, Dominik last_name: Wojtczak citation: 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 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' 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. ieee: K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013. ista: Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward verification in graphs and MDPs. 8312, 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. short: K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242. conference: end_date: 2013-12-19 location: Stellenbosch, South Africa name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning' start_date: 2013-12-14 date_created: 2018-12-11T11:56:30Z date_published: 2013-12-01T00:00:00Z date_updated: 2020-08-11T10:09:42Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-45221-5_17 ec_funded: 1 intvolume: ' 8312' language: - iso: eng month: '12' oa_version: None page: 228 - 242 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: Springer publist_id: '4723' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Multi-objective discounted reward verification in graphs and MDPs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8312 year: '2013' ... --- _id: '2292' abstract: - lang: eng 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. alternative_title: - LNCS citation: 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. ieee: K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer Science 2013, vol. 8087. Springer, 2013, p. VI-854. ista: Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science 2013, Springer,p. 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. conference: end_date: 2013-08-30 location: Klosterneuburg, Austria name: 'MFCS: Mathematical Foundations of Computer Science' start_date: 2013-08-26 date_created: 2018-12-11T11:56:48Z date_published: 2013-08-08T00:00:00Z date_updated: 2020-08-11T10:09:45Z day: '08' department: - _id: KrCh doi: 10.1007/978-3-642-40313-2 editor: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Jiri full_name: Sgall, Jiri last_name: Sgall intvolume: ' 8087' language: - iso: eng month: '08' oa_version: None page: VI - 854 publication_identifier: isbn: - 978-3-642-40312-5 publication_status: published publisher: Springer publist_id: '4636' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Mathematical Foundations of Computer Science 2013 type: conference_editor user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8087 year: '2013' ... --- _id: '2299' abstract: - lang: eng 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.' author: - first_name: Yashdeep full_name: Godhal, Yashdeep id: 5B547124-EB61-11E9-8887-89D9C04DBDF5 last_name: Godhal - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: 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' 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' 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.' 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.' 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.' 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.' short: Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601. date_created: 2018-12-11T11:56:51Z date_published: 2013-10-01T00:00:00Z date_updated: 2021-01-12T06:56:37Z day: '01' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1007/s10009-011-0207-9 file: - access_level: open_access checksum: 57b06a732dd8d6349190dba6b5b0d33b content_type: application/pdf creator: system date_created: 2018-12-12T10:11:53Z date_updated: 2020-07-14T12:45:37Z file_id: '4910' file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf file_size: 277372 relation: main_file file_date_updated: 2020-07-14T12:45:37Z has_accepted_license: '1' intvolume: ' 15' issue: 5-6 language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 585 - 601 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: International Journal on Software Tools for Technology Transfer publication_status: published publisher: Springer publist_id: '4629' pubrep_id: '87' quality_controlled: '1' scopus_import: 1 status: public title: 'Synthesis of AMBA AHB from formal specification: A case study' type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2013' ... --- _id: '2446' 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. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Gaiser, Andreas last_name: Gaiser - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: 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' 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. 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. 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. short: K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575. conference: end_date: 2013-07-19 location: St. Petersburg, Russia name: 'CAV: Computer Aided Verification' start_date: 2013-07-13 date_created: 2018-12-11T11:57:42Z date_published: 2013-07-01T00:00:00Z date_updated: 2020-08-11T10:09:47Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-39799-8_37 ec_funded: 1 external_id: arxiv: - '1304.5281' intvolume: ' 8044' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1304.5281 month: '07' oa: 1 oa_version: Preprint page: 559 - 575 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication_status: published publisher: Springer publist_id: '4457' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8044 year: '2013' ... --- _id: '2444' abstract: - lang: eng text: 'We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Jakub full_name: Ła̧Cki, Jakub last_name: Ła̧Cki citation: ama: Chatterjee K, Ła̧Cki J. Faster algorithms for Markov decision processes with low treewidth. 2013;8044:543-558. doi:10.1007/978-3-642-39799-8_36 apa: 'Chatterjee, K., & Ła̧Cki, J. (2013). Faster algorithms for Markov decision processes with low treewidth. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_36' chicago: Chatterjee, Krishnendu, and Jakub Ła̧Cki. “Faster Algorithms for Markov Decision Processes with Low Treewidth.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_36. ieee: K. Chatterjee and J. Ła̧Cki, “Faster algorithms for Markov decision processes with low treewidth,” vol. 8044. Springer, pp. 543–558, 2013. ista: Chatterjee K, Ła̧Cki J. 2013. Faster algorithms for Markov decision processes with low treewidth. 8044, 543–558. mla: Chatterjee, Krishnendu, and Jakub Ła̧Cki. Faster Algorithms for Markov Decision Processes with Low Treewidth. Vol. 8044, Springer, 2013, pp. 543–58, doi:10.1007/978-3-642-39799-8_36. short: K. Chatterjee, J. Ła̧Cki, 8044 (2013) 543–558. conference: end_date: 2013-07-19 location: St. Petersburg, Russia name: 'CAV: Computer Aided Verification' start_date: 2013-07-13 date_created: 2018-12-11T11:57:42Z date_published: 2013-07-01T00:00:00Z date_updated: 2020-08-11T10:09:47Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-39799-8_36 ec_funded: 1 external_id: arxiv: - '1304.0084' intvolume: ' 8044' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1304.0084 month: '07' oa: 1 oa_version: Preprint page: 543 - 558 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication_status: published publisher: Springer publist_id: '4459' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Faster algorithms for Markov decision processes with low treewidth type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8044 year: '2013' ... --- _id: '2814' abstract: - lang: eng text: We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing "reset" action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies. We also discuss the memory requirement for deterministic strategies and extensions of our results to other models, such as pushdown systems and timed systems. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: Alfaro, Luca last_name: Alfaro - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar citation: ama: Chatterjee K, Alfaro L, Majumdar R. The complexity of coverage. International Journal of Foundations of Computer Science. 2013;24(2):165-185. doi:10.1142/S0129054113400066 apa: Chatterjee, K., Alfaro, L., & Majumdar, R. (2013). The complexity of coverage. International Journal of Foundations of Computer Science. World Scientific Publishing. https://doi.org/10.1142/S0129054113400066 chicago: Chatterjee, Krishnendu, Luca Alfaro, and Ritankar Majumdar. “The Complexity of Coverage.” International Journal of Foundations of Computer Science. World Scientific Publishing, 2013. https://doi.org/10.1142/S0129054113400066. ieee: K. Chatterjee, L. Alfaro, and R. Majumdar, “The complexity of coverage,” International Journal of Foundations of Computer Science, vol. 24, no. 2. World Scientific Publishing, pp. 165–185, 2013. ista: Chatterjee K, Alfaro L, Majumdar R. 2013. The complexity of coverage. International Journal of Foundations of Computer Science. 24(2), 165–185. mla: Chatterjee, Krishnendu, et al. “The Complexity of Coverage.” International Journal of Foundations of Computer Science, vol. 24, no. 2, World Scientific Publishing, 2013, pp. 165–85, doi:10.1142/S0129054113400066. short: K. Chatterjee, L. Alfaro, R. Majumdar, International Journal of Foundations of Computer Science 24 (2013) 165–185. date_created: 2018-12-11T11:59:44Z date_published: 2013-02-01T00:00:00Z date_updated: 2021-01-12T06:59:54Z day: '01' department: - _id: KrCh doi: 10.1142/S0129054113400066 ec_funded: 1 external_id: arxiv: - '0804.4525' intvolume: ' 24' issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/0804.4525 month: '02' oa: 1 oa_version: Preprint page: 165 - 185 project: - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: International Journal of Foundations of Computer Science publication_status: published publisher: World Scientific Publishing publist_id: '4070' quality_controlled: '1' scopus_import: 1 status: public title: The complexity of coverage type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 24 year: '2013' ... --- _id: '2817' abstract: - lang: eng text: The basic idea of evolutionary game theory is that payoff determines reproductive rate. Successful individuals have a higher payoff and produce more offspring. But in evolutionary and ecological situations there is not only reproductive rate but also carrying capacity. Individuals may differ in their exposure to density limiting effects. Here we explore an alternative approach to evolutionary game theory by assuming that the payoff from the game determines the carrying capacity of individual phenotypes. Successful strategies are less affected by density limitation (crowding) and reach higher equilibrium abundance. We demonstrate similarities and differences between our framework and the standard replicator equation. Our equation is defined on the positive orthant, instead of the simplex, but has the same equilibrium points as the replicator equation. Linear stability analysis produces the classical conditions for asymptotic stability of pure strategies, but the stability properties of internal equilibria can differ in the two frameworks. For example, in a two-strategy game with an internal equilibrium that is always stable under the replicator equation, the corresponding equilibrium can be unstable in the new framework resulting in a limit cycle. author: - first_name: Sebastian full_name: Novak, Sebastian id: 461468AE-F248-11E8-B48F-1D18A9856A87 last_name: Novak - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Nowak, Martin last_name: Nowak citation: ama: Novak S, Chatterjee K, Nowak M. Density games. Journal of Theoretical Biology. 2013;334:26-34. doi:10.1016/j.jtbi.2013.05.029 apa: Novak, S., Chatterjee, K., & Nowak, M. (2013). Density games. Journal of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2013.05.029 chicago: Novak, Sebastian, Krishnendu Chatterjee, and Martin Nowak. “Density Games.” Journal of Theoretical Biology. Elsevier, 2013. https://doi.org/10.1016/j.jtbi.2013.05.029. ieee: S. Novak, K. Chatterjee, and M. Nowak, “Density games,” Journal of Theoretical Biology, vol. 334. Elsevier, pp. 26–34, 2013. ista: Novak S, Chatterjee K, Nowak M. 2013. Density games. Journal of Theoretical Biology. 334, 26–34. mla: Novak, Sebastian, et al. “Density Games.” Journal of Theoretical Biology, vol. 334, Elsevier, 2013, pp. 26–34, doi:10.1016/j.jtbi.2013.05.029. short: S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013) 26–34. date_created: 2018-12-11T11:59:45Z date_published: 2013-10-07T00:00:00Z date_updated: 2021-01-12T06:59:55Z day: '07' ddc: - '000' department: - _id: NiBa - _id: KrCh doi: 10.1016/j.jtbi.2013.05.029 ec_funded: 1 file: - access_level: open_access checksum: 3c29059ab03a4b8f97a07646b817ddbb content_type: application/pdf creator: system date_created: 2018-12-12T10:14:54Z date_updated: 2020-07-14T12:45:49Z file_id: '5110' file_name: IST-2016-400-v1+1_1-s2.0-S0022519313002609-main.pdf file_size: 834604 relation: main_file file_date_updated: 2020-07-14T12:45:49Z has_accepted_license: '1' intvolume: ' 334' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 26 - 34 project: - _id: 25B07788-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '250152' name: Limits to selection in biology and in evolutionary computation - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: Journal of Theoretical Biology publication_status: published publisher: Elsevier publist_id: '3984' pubrep_id: '400' quality_controlled: '1' scopus_import: 1 status: public title: Density games tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 334 year: '2013' ... --- _id: '2819' abstract: - lang: eng text: 'We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions. ' acknowledgement: 'This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOP-TILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); and the Microsoft faculty fellows award' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vinayak full_name: Prabhu, Vinayak last_name: Prabhu citation: ama: 'Chatterjee K, Prabhu V. Quantitative timed simulation functions and refinement metrics for real-time systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. Vol 1. Springer; 2013:273-282. doi:10.1145/2461328.2461370' apa: 'Chatterjee, K., & Prabhu, V. (2013). Quantitative timed simulation functions and refinement metrics for real-time systems. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (Vol. 1, pp. 273–282). Philadelphia, PA USA: Springer. https://doi.org/10.1145/2461328.2461370' chicago: 'Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, 1:273–82. Springer, 2013. https://doi.org/10.1145/2461328.2461370.' ieee: 'K. Chatterjee and V. Prabhu, “Quantitative timed simulation functions and refinement metrics for real-time systems,” in Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Philadelphia, PA USA, 2013, vol. 1, pp. 273–282.' ista: 'Chatterjee K, Prabhu V. 2013. Quantitative timed simulation functions and refinement metrics for real-time systems. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control vol. 1, 273–282.' mla: 'Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, vol. 1, Springer, 2013, pp. 273–82, doi:10.1145/2461328.2461370.' short: 'K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.' conference: end_date: 2013-04-11 location: Philadelphia, PA USA name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2013-04-08 date_created: 2018-12-11T11:59:46Z date_published: 2013-04-01T00:00:00Z date_updated: 2021-01-12T06:59:56Z day: '01' department: - _id: KrCh doi: 10.1145/2461328.2461370 ec_funded: 1 intvolume: ' 1' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1212.6556 month: '04' oa: 1 oa_version: Preprint page: 273 - 282 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: 'Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control' publication_status: published publisher: Springer publist_id: '3982' quality_controlled: '1' scopus_import: 1 status: public title: Quantitative timed simulation functions and refinement metrics for real-time systems type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 1 year: '2013' ... --- _id: '2824' abstract: - lang: eng text: We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vinayak full_name: Prabhu, Vinayak last_name: Prabhu citation: ama: Chatterjee K, Prabhu V. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation. 2013;228-229:83-119. doi:10.1016/j.ic.2013.04.003 apa: Chatterjee, K., & Prabhu, V. (2013). Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2013.04.003 chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” Information and Computation. Elsevier, 2013. https://doi.org/10.1016/j.ic.2013.04.003. ieee: K. Chatterjee and V. Prabhu, “Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems,” Information and Computation, vol. 228–229. Elsevier, pp. 83–119, 2013. ista: Chatterjee K, Prabhu V. 2013. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation. 228–229, 83–119. mla: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” Information and Computation, vol. 228–229, Elsevier, 2013, pp. 83–119, doi:10.1016/j.ic.2013.04.003. short: K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119. date_created: 2018-12-11T11:59:47Z date_published: 2013-04-24T00:00:00Z date_updated: 2021-01-12T06:59:58Z day: '24' department: - _id: KrCh doi: 10.1016/j.ic.2013.04.003 ec_funded: 1 language: - iso: eng month: '04' oa_version: None page: 83-119 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: Information and Computation publication_status: published publisher: Elsevier publist_id: '3977' quality_controlled: '1' scopus_import: 1 status: public title: Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 228-229 year: '2013' ... --- _id: '2836' abstract: - lang: eng text: 'We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party as path formulas in linear temporal logic and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to AGS can be computed efficiently as the secure equilibrium solution of three-player graph games. ' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vishwanath full_name: Raman, Vishwanath last_name: Raman citation: ama: Chatterjee K, Raman V. Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. 2013;26(4):825-859. doi:10.1007/s00165-013-0283-6 apa: Chatterjee, K., & Raman, V. (2013). Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. Springer. https://doi.org/10.1007/s00165-013-0283-6 chicago: Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” Formal Aspects of Computing. Springer, 2013. https://doi.org/10.1007/s00165-013-0283-6. ieee: K. Chatterjee and V. Raman, “Assume-guarantee synthesis for digital contract signing,” Formal Aspects of Computing, vol. 26, no. 4. Springer, pp. 825–859, 2013. ista: Chatterjee K, Raman V. 2013. Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. 26(4), 825–859. mla: Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” Formal Aspects of Computing, vol. 26, no. 4, Springer, 2013, pp. 825–59, doi:10.1007/s00165-013-0283-6. short: K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859. date_created: 2018-12-11T11:59:51Z date_published: 2013-07-04T00:00:00Z date_updated: 2021-01-12T07:00:06Z day: '04' department: - _id: KrCh doi: 10.1007/s00165-013-0283-6 ec_funded: 1 external_id: arxiv: - '1004.2697' intvolume: ' 26' issue: '4' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1004.2697 month: '07' oa: 1 oa_version: Preprint page: 825 - 859 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: Formal Aspects of Computing publication_status: published publisher: Springer publist_id: '3963' quality_controlled: '1' scopus_import: 1 status: public title: Assume-guarantee synthesis for digital contract signing type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 26 year: '2013' ... --- _id: '2854' abstract: - lang: eng text: We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc. acknowledgement: This work was partially supported in part by the NSF grants CCR-0132780, CNS-0720884, CCR-0225610, by the Swiss National Science Foundation, ERC Start Grant Graph Games (Project No. 279307), FWF NFN Grant S11407-N23 (RiSE), and a Microsoft faculty fellows article_processing_charge: No article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent reachability and turn based stochastic safety games. Journal of Computer and System Sciences. 2013;79(5):640-657. doi:10.1016/j.jcss.2012.12.001 apa: Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2013). Strategy improvement for concurrent reachability and turn based stochastic safety games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2012.12.001 chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.” Journal of Computer and System Sciences. Elsevier, 2013. https://doi.org/10.1016/j.jcss.2012.12.001. ieee: K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for concurrent reachability and turn based stochastic safety games,” Journal of Computer and System Sciences, vol. 79, no. 5. Elsevier, pp. 640–657, 2013. ista: Chatterjee K, De Alfaro L, Henzinger TA. 2013. Strategy improvement for concurrent reachability and turn based stochastic safety games. Journal of Computer and System Sciences. 79(5), 640–657. mla: Chatterjee, Krishnendu, et al. “Strategy Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.” Journal of Computer and System Sciences, vol. 79, no. 5, Elsevier, 2013, pp. 640–57, doi:10.1016/j.jcss.2012.12.001. short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, Journal of Computer and System Sciences 79 (2013) 640–657. date_created: 2018-12-11T11:59:57Z date_published: 2013-08-01T00:00:00Z date_updated: 2021-01-12T07:00:16Z day: '01' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1016/j.jcss.2012.12.001 ec_funded: 1 file: - access_level: open_access checksum: 6d3ee12cceb946a0abe69594b6a22409 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:48Z date_updated: 2020-07-14T12:45:51Z file_id: '5370' file_name: IST-2015-388-v1+1_1-s2.0-S0022000012001778-main.pdf file_size: 425488 relation: main_file file_date_updated: 2020-07-14T12:45:51Z has_accepted_license: '1' intvolume: ' 79' issue: '5' language: - iso: eng license: https://creativecommons.org/licenses/by-nc-nd/4.0/ month: '08' oa: 1 oa_version: Published Version page: 640 - 657 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Journal of Computer and System Sciences publication_status: published publisher: Elsevier publist_id: '3938' pubrep_id: '388' quality_controlled: '1' scopus_import: 1 status: public title: Strategy improvement for concurrent reachability and turn based stochastic safety games tmp: image: /images/cc_by_nc_nd.png legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) short: CC BY-NC-ND (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 79 year: '2013' ... --- _id: '2886' abstract: - lang: eng text: We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization. alternative_title: - LNCS author: - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Řehák, Vojtěch last_name: Řehák citation: ama: Chmelik M, Řehák V. Controllable-choice message sequence graphs. 2013;7721:118-130. doi:10.1007/978-3-642-36046-6_12 apa: 'Chmelik, M., & Řehák, V. (2013). Controllable-choice message sequence graphs. Presented at the MEMICS: Mathematical and Engineering Methods in Computer Science, Znojmo, Czech Republic: Springer. https://doi.org/10.1007/978-3-642-36046-6_12' chicago: Chmelik, Martin, and Vojtěch Řehák. “Controllable-Choice Message Sequence Graphs.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-36046-6_12. ieee: M. Chmelik and V. Řehák, “Controllable-choice message sequence graphs,” vol. 7721. Springer, pp. 118–130, 2013. ista: Chmelik M, Řehák V. 2013. Controllable-choice message sequence graphs. 7721, 118–130. mla: Chmelik, Martin, and Vojtěch Řehák. Controllable-Choice Message Sequence Graphs. Vol. 7721, Springer, 2013, pp. 118–30, doi:10.1007/978-3-642-36046-6_12. short: M. Chmelik, V. Řehák, 7721 (2013) 118–130. conference: end_date: 2012-10-28 location: Znojmo, Czech Republic name: 'MEMICS: Mathematical and Engineering Methods in Computer Science' start_date: 2012-10-25 date_created: 2018-12-11T12:00:09Z date_published: 2013-01-09T00:00:00Z date_updated: 2020-08-11T10:09:52Z day: '09' department: - _id: KrCh doi: 10.1007/978-3-642-36046-6_12 ec_funded: 1 intvolume: ' 7721' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1209.4499 month: '01' oa: 1 oa_version: Submitted Version page: 118 - 130 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication_status: published publisher: Springer publist_id: '3873' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Controllable-choice message sequence graphs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 7721 year: '2013' ... --- _id: '3116' abstract: - lang: eng text: Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads. © 2012 Springer Science+Business Media, LLC. acknowledgement: This research was supported in part by the National Science Foundation CAREER award CCR-0132780, by the ONR grant N00014-02-1-0671, by the National Science Foundation grants CCR-0427202 and CCR-0234690, and by the ARP award TO.030.MM.D. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Marco full_name: Faella, Marco last_name: Faella - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar - first_name: Vishwanath full_name: Raman, Vishwanath last_name: Raman citation: ama: Chatterjee K, De Alfaro L, Faella M, Majumdar R, Raman V. Code aware resource management. Formal Methods in System Design. 2013;42(2):142-174. doi:10.1007/s10703-012-0170-4 apa: Chatterjee, K., De Alfaro, L., Faella, M., Majumdar, R., & Raman, V. (2013). Code aware resource management. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0170-4 chicago: Chatterjee, Krishnendu, Luca De Alfaro, Marco Faella, Ritankar Majumdar, and Vishwanath Raman. “Code Aware Resource Management.” Formal Methods in System Design. Springer, 2013. https://doi.org/10.1007/s10703-012-0170-4. ieee: K. Chatterjee, L. De Alfaro, M. Faella, R. Majumdar, and V. Raman, “Code aware resource management,” Formal Methods in System Design, vol. 42, no. 2. Springer, pp. 142–174, 2013. ista: Chatterjee K, De Alfaro L, Faella M, Majumdar R, Raman V. 2013. Code aware resource management. Formal Methods in System Design. 42(2), 142–174. mla: Chatterjee, Krishnendu, et al. “Code Aware Resource Management.” Formal Methods in System Design, vol. 42, no. 2, Springer, 2013, pp. 142–74, doi:10.1007/s10703-012-0170-4. short: K. Chatterjee, L. De Alfaro, M. Faella, R. Majumdar, V. Raman, Formal Methods in System Design 42 (2013) 142–174. date_created: 2018-12-11T12:01:29Z date_published: 2013-04-01T00:00:00Z date_updated: 2021-01-12T07:41:10Z day: '01' department: - _id: KrCh doi: 10.1007/s10703-012-0170-4 intvolume: ' 42' issue: '2' language: - iso: eng month: '04' oa_version: None page: 142 - 174 publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '3583' quality_controlled: '1' scopus_import: 1 status: public title: Code aware resource management type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 42 year: '2013' ... --- _id: '2831' abstract: - lang: eng text: 'We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc''s) of the MDP. The win-lose algorithm requires symbolic computation of scc''s. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps.' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Manas full_name: Joglekar, Manas last_name: Joglekar - first_name: Nisarg full_name: Shah, Nisarg last_name: Shah citation: ama: Chatterjee K, Henzinger MH, Joglekar M, Shah N. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 2013;42(3):301-327. doi:10.1007/s10703-012-0180-2 apa: Chatterjee, K., Henzinger, M. H., Joglekar, M., & Shah, N. (2013). Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0180-2 chicago: Chatterjee, Krishnendu, Monika H Henzinger, Manas Joglekar, and Nisarg Shah. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” Formal Methods in System Design. Springer, 2013. https://doi.org/10.1007/s10703-012-0180-2. ieee: K. Chatterjee, M. H. Henzinger, M. Joglekar, and N. Shah, “Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives,” Formal Methods in System Design, vol. 42, no. 3. Springer, pp. 301–327, 2013. ista: Chatterjee K, Henzinger MH, Joglekar M, Shah N. 2013. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 42(3), 301–327. mla: Chatterjee, Krishnendu, et al. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” Formal Methods in System Design, vol. 42, no. 3, Springer, 2013, pp. 301–27, doi:10.1007/s10703-012-0180-2. short: K. Chatterjee, M.H. Henzinger, M. Joglekar, N. Shah, Formal Methods in System Design 42 (2013) 301–327. date_created: 2018-12-11T11:59:49Z date_published: 2013-06-01T00:00:00Z date_updated: 2023-02-23T11:23:04Z day: '01' department: - _id: KrCh doi: 10.1007/s10703-012-0180-2 ec_funded: 1 external_id: arxiv: - '1104.3348' intvolume: ' 42' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1104.3348 month: '06' oa: 1 oa_version: Preprint page: 301 - 327 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _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 publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '3968' quality_controlled: '1' related_material: record: - id: '3342' relation: earlier_version status: public scopus_import: '1' status: public title: Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives type: journal_article user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd volume: 42 year: '2013' ...