[{"quality_controlled":"1","ec_funded":1,"publisher":"Springer Nature","article_type":"original","scopus_import":"1","license":"https://creativecommons.org/licenses/by/4.0/","_id":"12738","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Joost P","last_name":"Katoen","full_name":"Katoen, Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mohr, Stefanie","first_name":"Stefanie","last_name":"Mohr"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"}],"department":[{"_id":"KrCh"}],"date_created":"2023-03-19T23:00:59Z","article_processing_charge":"No","publication_status":"epub_ahead","title":"Stochastic games with lexicographic objectives","acknowledgement":"Tobias Winkler and Joost-Pieter Katoen are supported by the DFG RTG 2236 UnRAVeL and the innovation programme under the Marie Skłodowska-Curie grant agreement No. 101008233 (Mission). Krishnendu Chatterjee is supported by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) Project ICT15-003. Maximilian Weininger is supported by the DFG projects 383882557 Statistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic Verification (GOPro). Stefanie Mohr is supported by the DFG RTG 2428 CONVEY. Open Access funding enabled and organized by Projekt DEAL.","ddc":["000"],"year":"2023","citation":{"ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic games with lexicographic objectives. Formal Methods in System Design.","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” Formal Methods in System Design, Springer Nature, 2023, doi:10.1007/s10703-023-00411-4.","short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design (2023).","ieee":"K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” Formal Methods in System Design. Springer Nature, 2023.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Stefanie Mohr, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Objectives.” Formal Methods in System Design. Springer Nature, 2023. https://doi.org/10.1007/s10703-023-00411-4.","ama":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with lexicographic objectives. Formal Methods in System Design. 2023. doi:10.1007/s10703-023-00411-4","apa":"Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., & Winkler, T. (2023). Stochastic games with lexicographic objectives. Formal Methods in System Design. Springer Nature. https://doi.org/10.1007/s10703-023-00411-4"},"date_updated":"2025-07-14T09:10:14Z","external_id":{"isi":["000946174300001"]},"isi":1,"day":"08","doi":"10.1007/s10703-023-00411-4","abstract":[{"lang":"eng","text":"We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP∩coNP, matching the current known bound for single objectives; and in general the decision problem is PSPACE-hard and can be solved in NEXPTIME∩coNEXPTIME. We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies."}],"language":[{"iso":"eng"}],"publication":"Formal Methods in System Design","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","month":"03","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10703-023-00411-4"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8272","relation":"earlier_version"}]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"journal_article","date_published":"2023-03-08T00:00:00Z","publication_identifier":{"eissn":["1572-8102"]},"oa":1},{"keyword":["safety","risk","reliability and quality","software"],"language":[{"iso":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","article_number":"164","month":"10","has_accepted_license":"1","publication":"Proceedings of the ACM on Programming Languages","file":[{"success":1,"relation":"main_file","access_level":"open_access","creator":"cchlebak","file_id":"10215","file_size":2903485,"checksum":"9d6dce7b611853c529bb7b1915ac579e","date_created":"2021-11-04T07:24:48Z","content_type":"application/pdf","file_name":"2021_ProcACMPL_Bui.pdf","date_updated":"2021-11-04T07:24:48Z"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"status":"public","publication_identifier":{"eissn":["2475-1421"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"journal_article","date_published":"2021-10-15T00:00:00Z","publisher":"Association for Computing Machinery","article_type":"original","ec_funded":1,"quality_controlled":"1","file_date_updated":"2021-11-04T07:24:48Z","date_created":"2021-10-27T15:05:34Z","article_processing_charge":"No","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"publication_status":"published","intvolume":" 5","title":"The reads-from equivalence for the TSO and PSO memory models","scopus_import":"1","_id":"10191","issue":"OOPSLA","author":[{"last_name":"Bui","first_name":"Truc Lam","full_name":"Bui, Truc Lam"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gautam, Tushar","last_name":"Gautam","first_name":"Tushar"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","first_name":"Viktor","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003.","volume":5,"ddc":["000"],"day":"15","arxiv":1,"doi":"10.1145/3485541","abstract":[{"text":"In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.\r\n\r\n","lang":"eng"}],"year":"2021","citation":{"ista":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","mla":"Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:10.1145/3485541.","ieee":"T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.","chicago":"Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485541.","apa":"Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541","ama":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 2021;5(OOPSLA). doi:10.1145/3485541"},"date_updated":"2025-07-14T09:10:16Z","external_id":{"arxiv":["2011.11763"]}},{"ddc":["000"],"citation":{"ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10199.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:10.15479/at:ista:10199","apa":"Toman, V. (2021). Improved verification techniques for concurrent systems. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10199","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","mla":"Toman, Viktor. Improved Verification Techniques for Concurrent Systems. Institute of Science and Technology Austria, 2021, doi:10.15479/at:ista:10199."},"year":"2021","date_updated":"2025-07-14T09:10:16Z","abstract":[{"lang":"eng","text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness."}],"day":"31","degree_awarded":"PhD","doi":"10.15479/at:ista:10199","file_date_updated":"2021-11-09T09:00:50Z","ec_funded":1,"page":"166","publisher":"Institute of Science and Technology Austria","author":[{"orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","first_name":"Viktor","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"_id":"10199","title":"Improved verification techniques for concurrent systems","alternative_title":["ISTA Thesis"],"date_created":"2021-10-29T20:09:01Z","article_processing_charge":"No","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"publication_status":"published","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"status":"public","id":"10190","relation":"part_of_dissertation"},{"id":"9987","relation":"part_of_dissertation","status":"public"},{"id":"141","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"10191"}]},"file":[{"creator":"vtoman","file_id":"10225","access_level":"open_access","relation":"main_file","file_name":"toman_th_final.pdf","content_type":"application/pdf","date_updated":"2021-11-08T14:12:22Z","file_size":2915234,"checksum":"4f412a1ee60952221b499a4b1268df35","date_created":"2021-11-08T14:12:22Z"},{"access_level":"closed","relation":"source_file","file_id":"10226","creator":"vtoman","date_created":"2021-11-08T14:12:46Z","file_size":8616056,"checksum":"9584943f99127be2dd2963f6784c37d4","date_updated":"2021-11-09T09:00:50Z","file_name":"toman_thesis.zip","content_type":"application/zip"}],"type":"dissertation","date_published":"2021-10-31T00:00:00Z","oa":1,"supervisor":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"publication_identifier":{"issn":["2663-337X"]},"keyword":["concurrency","verification","model checking"],"language":[{"iso":"eng"}],"has_accepted_license":"1","month":"10","project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"acknowledged_ssus":[{"_id":"SSU"}],"oa_version":"Published Version"},{"author":[{"last_name":"Agarwal","first_name":"Pratyush","full_name":"Agarwal, Pratyush"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Pathak, Shreya","last_name":"Pathak","first_name":"Shreya"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"scopus_import":"1","_id":"9987","title":"Stateless model checking under a reads-value-from equivalence","alternative_title":["LNCS"],"date_created":"2021-09-05T22:01:24Z","article_processing_charge":"Yes","department":[{"_id":"KrCh"}],"publication_status":"published","file_date_updated":"2022-05-13T07:00:20Z","quality_controlled":"1","ec_funded":1,"page":"341-366","publisher":"Springer Nature","external_id":{"isi":["000698732400016"],"arxiv":["2105.06424"]},"isi":1,"year":"2021","citation":{"short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16.","ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16.","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 341–366."},"date_updated":"2025-07-14T09:10:15Z","abstract":[{"lang":"eng","text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task."}],"day":"15","doi":"10.1007/978-3-030-81685-8_16","arxiv":1,"ddc":["000"],"volume":"12759 ","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","has_accepted_license":"1","publication":"33rd International Conference on Computer-Aided Verification ","month":"07","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"location":"Virtual","end_date":"2021-07-23","start_date":"2021-07-20","name":"CAV: Computer Aided Verification "},"type":"conference","date_published":"2021-07-15T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["978-3-030-81684-1"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["978-3-030-81685-8"]},"related_material":{"record":[{"status":"public","id":"10199","relation":"dissertation_contains"}]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","file_size":1516756,"date_created":"2022-05-13T07:00:20Z","file_name":"2021_LNCS_Agarwal.pdf","content_type":"application/pdf","date_updated":"2022-05-13T07:00:20Z","relation":"main_file","access_level":"open_access","success":1,"creator":"dernst","file_id":"11368"}]},{"publication_identifier":{"issn":["03029743"],"eissn":["16113349"],"isbn":["9783030449131"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2020-04-18T00:00:00Z","file":[{"file_id":"7895","creator":"dernst","access_level":"open_access","relation":"main_file","date_updated":"2020-07-14T12:48:03Z","content_type":"application/pdf","file_name":"2020_LNCS_Chatterjee.pdf","date_created":"2020-05-26T13:34:48Z","file_size":651250,"checksum":"8618b80f4cf7b39a60e61a6445ad9807"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"8934","status":"public"}]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"oa_version":"Published Version","month":"04","has_accepted_license":"1","publication":"European Symposium on Programming","conference":{"location":"Dublin, Ireland","end_date":"2020-04-30","start_date":"2020-04-25","name":"ESOP: Programming Languages and Systems"},"language":[{"iso":"eng"}],"day":"18","doi":"10.1007/978-3-030-44914-8_5","abstract":[{"text":"Interprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries.\r\nIn this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques.","lang":"eng"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” European Symposium on Programming, vol. 12075, Springer Nature, 2020, pp. 112–40, doi:10.1007/978-3-030-44914-8_5.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, European Symposium on Programming, Springer Nature, 2020, pp. 112–140.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2020. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. European Symposium on Programming. ESOP: Programming Languages and Systems, LNCS, vol. 12075, 112–140.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A. (2020). Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In European Symposium on Programming (Vol. 12075, pp. 112–140). Dublin, Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-44914-8_5","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: European Symposium on Programming. Vol 12075. Springer Nature; 2020:112-140. doi:10.1007/978-3-030-44914-8_5","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal and Perfectly Parallel Algorithms for On-Demand Data-Flow Analysis.” In European Symposium on Programming, 12075:112–40. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-44914-8_5.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal and perfectly parallel algorithms for on-demand data-flow analysis,” in European Symposium on Programming, Dublin, Ireland, 2020, vol. 12075, pp. 112–140."},"year":"2020","date_updated":"2025-06-02T08:53:42Z","external_id":{"isi":["000681656800005"]},"isi":1,"volume":12075,"ddc":["000"],"department":[{"_id":"KrCh"}],"date_created":"2020-05-10T22:00:50Z","article_processing_charge":"No","publication_status":"published","intvolume":" 12075","alternative_title":["LNCS"],"title":"Optimal and perfectly parallel algorithms for on-demand data-flow analysis","scopus_import":"1","_id":"7810","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"}],"publisher":"Springer Nature","quality_controlled":"1","page":"112-140","file_date_updated":"2020-07-14T12:48:03Z"},{"date_published":"2020-07-08T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9781450371049"]},"oa":1,"file":[{"relation":"main_file","success":1,"access_level":"open_access","file_id":"8804","creator":"dernst","date_created":"2020-11-25T09:38:14Z","file_size":1001395,"checksum":"d0d0288fe991dd16cf5f02598b794240","date_updated":"2020-11-25T09:38:14Z","content_type":"application/pdf","file_name":"2020_LICS_Ashok.pdf"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication":"Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science ","has_accepted_license":"1","oa_version":"Published Version","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"month":"07","language":[{"iso":"eng"}],"conference":{"location":"Saarbrücken, Germany","end_date":"2020-07-11","name":"LICS: Symposium on Logic in Computer Science","start_date":"2020-07-08"},"date_updated":"2025-06-02T08:53:42Z","citation":{"chicago":"Ashok, Pranav, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger, and Tobias Winkler. “Approximating Values of Generalized-Reachability Stochastic Games.” In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , 102–15. Association for Computing Machinery, 2020. https://doi.org/10.1145/3373718.3394761.","ieee":"P. Ashok, K. Chatterjee, J. Kretinsky, M. Weininger, and T. Winkler, “Approximating values of generalized-reachability stochastic games,” in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Saarbrücken, Germany, 2020, pp. 102–115.","apa":"Ashok, P., Chatterjee, K., Kretinsky, J., Weininger, M., & Winkler, T. (2020). Approximating values of generalized-reachability stochastic games. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 102–115). Saarbrücken, Germany: Association for Computing Machinery. https://doi.org/10.1145/3373718.3394761","ama":"Ashok P, Chatterjee K, Kretinsky J, Weininger M, Winkler T. Approximating values of generalized-reachability stochastic games. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . Association for Computing Machinery; 2020:102-115. doi:10.1145/3373718.3394761","ista":"Ashok P, Chatterjee K, Kretinsky J, Weininger M, Winkler T. 2020. Approximating values of generalized-reachability stochastic games. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . LICS: Symposium on Logic in Computer Science, 102–115.","short":"P. Ashok, K. Chatterjee, J. Kretinsky, M. Weininger, T. Winkler, in:, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Association for Computing Machinery, 2020, pp. 102–115.","mla":"Ashok, Pranav, et al. “Approximating Values of Generalized-Reachability Stochastic Games.” Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Association for Computing Machinery, 2020, pp. 102–15, doi:10.1145/3373718.3394761."},"year":"2020","isi":1,"external_id":{"isi":["000665014900010"],"arxiv":["1908.05106"]},"doi":"10.1145/3373718.3394761","arxiv":1,"day":"08","abstract":[{"text":"Simple stochastic games are turn-based 2½-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.","lang":"eng"}],"acknowledgement":"Pranav Ashok, Jan Křetínský and Maximilian Weininger were funded in part by TUM IGSSE Grant 10.06 (PARSEC) and the German Research Foundation (DFG) project KR 4890/2-1\r\n“Statistical Unbounded Verification”. Krishnendu Chatterjee was supported by the ERC CoG 863818 (ForM-SMArt) and Vienna Science and Technology Fund (WWTF) Project ICT15-\r\n003. Tobias Winkler was supported by the RTG 2236 UnRAVe.","ddc":["000"],"_id":"7955","scopus_import":"1","author":[{"full_name":"Ashok, Pranav","first_name":"Pranav","last_name":"Ashok"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Kretinsky","full_name":"Kretinsky, Jan"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"}],"publication_status":"published","date_created":"2020-06-14T22:00:48Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"title":"Approximating values of generalized-reachability stochastic games","page":"102-115","quality_controlled":"1","ec_funded":1,"file_date_updated":"2020-11-25T09:38:14Z","publisher":"Association for Computing Machinery"},{"date_created":"2020-07-05T22:00:45Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","title":"Polynomial invariant generation for non-deterministic recursive programs","scopus_import":"1","_id":"8089","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar"},{"full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady","first_name":"Ehsan Kafshdar"}],"publisher":"Association for Computing Machinery","quality_controlled":"1","page":"672-687","day":"11","arxiv":1,"doi":"10.1145/3385412.3385969","abstract":[{"text":"We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set.\r\n\r\nOn the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previous complete method (Kapur, ACA 2004) is doubly-exponential. Even when restricted to linear invariants, the best previous complexity for complete invariant generation is exponential (Colon et al, CAV 2003). On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. We demonstrate the applicability of our approach by providing experimental results on several academic benchmarks. To the best of our knowledge, the only previous invariant generation method that provides completeness guarantees for invariants consisting of polynomial inequalities is (Kapur, ACA 2004), which relies on quantifier elimination and cannot even handle toy programs such as our running example.","lang":"eng"}],"citation":{"ieee":"K. Chatterjee, H. Fu, A. K. Goharshady, and E. K. Goharshady, “Polynomial invariant generation for non-deterministic recursive programs,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, London, United Kingdom, 2020, pp. 672–687.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. “Polynomial Invariant Generation for Non-Deterministic Recursive Programs.” In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 672–87. Association for Computing Machinery, 2020. https://doi.org/10.1145/3385412.3385969.","ama":"Chatterjee K, Fu H, Goharshady AK, Goharshady EK. Polynomial invariant generation for non-deterministic recursive programs. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2020:672-687. doi:10.1145/3385412.3385969","apa":"Chatterjee, K., Fu, H., Goharshady, A. K., & Goharshady, E. K. (2020). Polynomial invariant generation for non-deterministic recursive programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 672–687). London, United Kingdom: Association for Computing Machinery. https://doi.org/10.1145/3385412.3385969","ista":"Chatterjee K, Fu H, Goharshady AK, Goharshady EK. 2020. Polynomial invariant generation for non-deterministic recursive programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 672–687.","mla":"Chatterjee, Krishnendu, et al. “Polynomial Invariant Generation for Non-Deterministic Recursive Programs.” Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2020, pp. 672–87, doi:10.1145/3385412.3385969.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, E.K. Goharshady, in:, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2020, pp. 672–687."},"year":"2020","date_updated":"2025-06-02T08:53:42Z","external_id":{"arxiv":["1902.04373"],"isi":["000614622300045"]},"isi":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"oa_version":"Preprint","month":"06","publication":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation","conference":{"name":"PLDI: Programming Language Design and Implementation","start_date":"2020-06-15","location":"London, United Kingdom","end_date":"2020-06-20"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450376136"]},"oa":1,"type":"conference","date_published":"2020-06-11T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1902.04373","open_access":"1"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]}},{"external_id":{"isi":["000695272500021"],"arxiv":["2005.04018"]},"isi":1,"citation":{"apa":"Chatterjee, K., Katoen, J. P., Weininger, M., & Winkler, T. (2020). Stochastic games with lexicographic reachability-safety objectives. In International Conference on Computer Aided Verification (Vol. 12225, pp. 398–420). Springer Nature. https://doi.org/10.1007/978-3-030-53291-8_21","ama":"Chatterjee K, Katoen JP, Weininger M, Winkler T. Stochastic games with lexicographic reachability-safety objectives. In: International Conference on Computer Aided Verification. Vol 12225. Springer Nature; 2020:398-420. doi:10.1007/978-3-030-53291-8_21","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” In International Conference on Computer Aided Verification, 12225:398–420. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-53291-8_21.","ieee":"K. Chatterjee, J. P. Katoen, M. Weininger, and T. Winkler, “Stochastic games with lexicographic reachability-safety objectives,” in International Conference on Computer Aided Verification, 2020, vol. 12225, pp. 398–420.","short":"K. Chatterjee, J.P. Katoen, M. Weininger, T. Winkler, in:, International Conference on Computer Aided Verification, Springer Nature, 2020, pp. 398–420.","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” International Conference on Computer Aided Verification, vol. 12225, Springer Nature, 2020, pp. 398–420, doi:10.1007/978-3-030-53291-8_21.","ista":"Chatterjee K, Katoen JP, Weininger M, Winkler T. 2020. Stochastic games with lexicographic reachability-safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 12225, 398–420."},"year":"2020","date_updated":"2025-07-14T09:10:14Z","abstract":[{"text":"We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP∩coNP , matching the current known bound for single objectives; and in general the decision problem is PSPACE -hard and can be solved in NEXPTIME∩coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.","lang":"eng"}],"day":"14","arxiv":1,"doi":"10.1007/978-3-030-53291-8_21","ddc":["000"],"volume":12225,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Katoen, Joost P","last_name":"Katoen","first_name":"Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"}],"scopus_import":"1","_id":"8272","intvolume":" 12225","alternative_title":["LNCS"],"title":"Stochastic games with lexicographic reachability-safety objectives","date_created":"2020-08-16T22:00:58Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","publication_status":"published","file_date_updated":"2020-08-17T11:32:44Z","quality_controlled":"1","ec_funded":1,"page":"398-420","publisher":"Springer Nature","type":"conference","date_published":"2020-07-14T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783030532901"],"issn":["03029743"],"eissn":["16113349"]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"record":[{"id":"12738","relation":"later_version","status":"public"}]},"file":[{"file_id":"8276","creator":"dernst","access_level":"open_access","relation":"main_file","success":1,"date_updated":"2020-08-17T11:32:44Z","content_type":"application/pdf","file_name":"2020_LNCS_CAV_Chatterjee.pdf","date_created":"2020-08-17T11:32:44Z","checksum":"093d4788d7d5b2ce0ffe64fbe7820043","file_size":625056}],"has_accepted_license":"1","publication":"International Conference on Computer Aided Verification","month":"07","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification"}},{"oa":1,"publication_identifier":{"issn":["18688969"],"isbn":["9783959771597"]},"date_published":"2020-08-18T00:00:00Z","type":"conference","tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"bbd7c4f55d45f2ff2a0a4ef0e10a77b1","file_size":491374,"date_created":"2020-09-21T13:57:34Z","content_type":"application/pdf","file_name":"2020_LIPIcs_Chatterjee.pdf","date_updated":"2020-09-21T13:57:34Z","access_level":"open_access","success":1,"relation":"main_file","creator":"dernst","file_id":"8550"}],"month":"08","article_number":"22:1-22:13","oa_version":"Published Version","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"publication":"45th International Symposium on Mathematical Foundations of Computer Science","has_accepted_license":"1","conference":{"start_date":"2020-08-24","name":"MFCS: Symposium on Mathematical Foundations of Computer Science","end_date":"2020-08-28","location":"Prague, Czech Republic"},"language":[{"iso":"eng"}],"abstract":[{"text":"Game of Life is a simple and elegant model to study dynamical system over networks. The model consists of a graph where every vertex has one of two types, namely, dead or alive. A configuration is a mapping of the vertices to the types. An update rule describes how the type of a vertex is updated given the types of its neighbors. In every round, all vertices are updated synchronously, which leads to a configuration update. While in general, Game of Life allows a broad range of update rules, we focus on two simple families of update rules, namely, underpopulation and overpopulation, that model several interesting dynamics studied in the literature. In both settings, a dead vertex requires at least a desired number of live neighbors to become alive. For underpopulation (resp., overpopulation), a live vertex requires at least (resp. at most) a desired number of live neighbors to remain alive. We study the basic computation problems, e.g., configuration reachability, for these two families of rules. For underpopulation rules, we show that these problems can be solved in polynomial time, whereas for overpopulation rules they are PSPACE-complete.","lang":"eng"}],"doi":"10.4230/LIPIcs.MFCS.2020.22","arxiv":1,"day":"18","external_id":{"arxiv":["2007.02894"]},"date_updated":"2025-06-02T08:53:42Z","year":"2020","citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Simplified game of life: Algorithms and complexity,” in 45th International Symposium on Mathematical Foundations of Computer Science, Prague, Czech Republic, 2020, vol. 170.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Simplified Game of Life: Algorithms and Complexity.” In 45th International Symposium on Mathematical Foundations of Computer Science, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.MFCS.2020.22.","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Simplified game of life: Algorithms and complexity. In: 45th International Symposium on Mathematical Foundations of Computer Science. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.MFCS.2020.22","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., & Svoboda, J. (2020). Simplified game of life: Algorithms and complexity. In 45th International Symposium on Mathematical Foundations of Computer Science (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2020.22","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2020. Simplified game of life: Algorithms and complexity. 45th International Symposium on Mathematical Foundations of Computer Science. MFCS: Symposium on Mathematical Foundations of Computer Science, LIPIcs, vol. 170, 22:1-22:13.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 45th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","mla":"Chatterjee, Krishnendu, et al. “Simplified Game of Life: Algorithms and Complexity.” 45th International Symposium on Mathematical Foundations of Computer Science, vol. 170, 22:1-22:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.MFCS.2020.22."},"ddc":["000"],"volume":170,"acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the Vienna Science and\r\nTechnology Fund (WWTF) Project ICT15-003.\r\nIsmaël Jecker: This project has received funding from the European Union’s Horizon 2020 research\r\nand innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411.","title":"Simplified game of life: Algorithms and complexity","alternative_title":["LIPIcs"],"intvolume":" 170","publication_status":"published","date_created":"2020-09-20T22:01:36Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","last_name":"Jecker","first_name":"Ismael R","full_name":"Jecker, Ismael R"},{"last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"_id":"8533","scopus_import":"1","license":"https://creativecommons.org/licenses/by/3.0/","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-09-21T13:57:34Z","ec_funded":1,"quality_controlled":"1"},{"conference":{"end_date":"2020-10-23","location":"Hanoi, Vietnam","start_date":"2020-10-19","name":"ATVA: Automated Technology for Verification and Analysis"},"language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"oa_version":"Submitted Version","month":"10","has_accepted_license":"1","publication":"Automated Technology for Verification and Analysis","file":[{"date_created":"2020-11-06T07:41:03Z","checksum":"ae83f27e5b189d5abc2e7514f1b7e1b5","file_size":726648,"date_updated":"2020-11-06T07:41:03Z","file_name":"2020_LNCS_ATVA_Asadi_accepted.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","success":1,"file_id":"8729","creator":"dernst"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"8934"}]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783030591526"],"isbn":["9783030591519"]},"oa":1,"type":"conference","date_published":"2020-10-12T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","page":"253-270","file_date_updated":"2020-11-06T07:41:03Z","date_created":"2020-11-06T07:30:05Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","intvolume":" 12302","alternative_title":["LNCS"],"title":"Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth","scopus_import":"1","_id":"8728","author":[{"full_name":"Asadi, Ali","first_name":"Ali","last_name":"Asadi"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mohammadi, Kiarash","first_name":"Kiarash","last_name":"Mohammadi"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"volume":12302,"ddc":["000"],"day":"12","doi":"10.1007/978-3-030-59152-6_14","abstract":[{"lang":"eng","text":"Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in O((n+m)⋅t2) time, given a tree decomposition of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) for each objective on MDPs, where κ is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude."}],"citation":{"chicago":"Asadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” In Automated Technology for Verification and Analysis, 12302:253–70. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-59152-6_14.","ieee":"A. Asadi, K. Chatterjee, A. K. Goharshady, K. Mohammadi, and A. Pavlogiannis, “Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth,” in Automated Technology for Verification and Analysis, Hanoi, Vietnam, 2020, vol. 12302, pp. 253–270.","apa":"Asadi, A., Chatterjee, K., Goharshady, A. K., Mohammadi, K., & Pavlogiannis, A. (2020). Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In Automated Technology for Verification and Analysis (Vol. 12302, pp. 253–270). Hanoi, Vietnam: Springer Nature. https://doi.org/10.1007/978-3-030-59152-6_14","ama":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. In: Automated Technology for Verification and Analysis. Vol 12302. Springer Nature; 2020:253-270. doi:10.1007/978-3-030-59152-6_14","ista":"Asadi A, Chatterjee K, Goharshady AK, Mohammadi K, Pavlogiannis A. 2020. Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 12302, 253–270.","mla":"Asadi, Ali, et al. “Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth.” Automated Technology for Verification and Analysis, vol. 12302, Springer Nature, 2020, pp. 253–70, doi:10.1007/978-3-030-59152-6_14.","short":"A. Asadi, K. Chatterjee, A.K. Goharshady, K. Mohammadi, A. Pavlogiannis, in:, Automated Technology for Verification and Analysis, Springer Nature, 2020, pp. 253–270."},"year":"2020","date_updated":"2025-06-02T08:53:43Z","external_id":{"isi":["000723555700014"]},"isi":1},{"abstract":[{"text":"In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a\r\ngiven probabilistic program terminates with probability 1. Scalable approaches for program analysis often\r\nrely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule)\r\nof Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure\r\ntermination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [16]. While the\r\nproposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed\r\nmodular rule is still not sound for almost-sure termination of probabilistic programs.\r\nBesides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a\r\nsound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel\r\nnotion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales\r\nthat are linear and show that they can be synthesized in polynomial time. Finally, we present experimental\r\nresults on a variety of benchmarks and several natural examples that model various types of nested while\r\nloops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure\r\ntermination property","lang":"eng"}],"doi":"10.1145/3360555","arxiv":1,"day":"01","external_id":{"arxiv":["1901.06087"]},"date_updated":"2025-06-02T08:53:47Z","citation":{"mla":"Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , vol. 3, 129, ACM, 2019, doi:10.1145/3360555.","short":"M. Huang, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , ACM, 2019.","ista":"Huang M, Fu H, Chatterjee K, Goharshady AK. 2019. Modular verification for almost-sure termination of probabilistic programs. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications . OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 129.","ama":"Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure termination of probabilistic programs. In: Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications . Vol 3. ACM; 2019. doi:10.1145/3360555","apa":"Huang, M., Fu, H., Chatterjee, K., & Goharshady, A. K. (2019). Modular verification for almost-sure termination of probabilistic programs. In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vol. 3). Athens, Greece: ACM. https://doi.org/10.1145/3360555","chicago":"Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , Vol. 3. ACM, 2019. https://doi.org/10.1145/3360555.","ieee":"M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification for almost-sure termination of probabilistic programs,” in Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , Athens, Greece, 2019, vol. 3."},"year":"2019","ddc":["000"],"volume":3,"title":"Modular verification for almost-sure termination of probabilistic programs","intvolume":" 3","publication_status":"published","article_processing_charge":"No","department":[{"_id":"KrCh"}],"date_created":"2019-08-09T09:54:20Z","author":[{"first_name":"Mingzhang","last_name":"Huang","full_name":"Huang, Mingzhang"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"}],"_id":"6780","license":"https://creativecommons.org/licenses/by-nc/4.0/","publisher":"ACM","file_date_updated":"2020-07-14T12:47:40Z","ec_funded":1,"quality_controlled":"1","oa":1,"date_published":"2019-10-01T00:00:00Z","type":"conference","tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"file":[{"access_level":"open_access","relation":"main_file","file_id":"6807","creator":"akafshda","date_created":"2019-08-12T15:40:57Z","file_size":1024643,"checksum":"3482d8ace6fb4991eb7810e3b70f1b9f","date_updated":"2020-07-14T12:47:40Z","content_type":"application/pdf","file_name":"oopsla-2019.pdf"},{"file_id":"7821","creator":"dernst","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:40Z","content_type":"application/pdf","file_name":"2019_ACM_Huang.pdf","date_created":"2020-05-12T15:15:14Z","file_size":538579,"checksum":"4e5a6fb2b59a75222a4e8335a5a60eac"}],"month":"10","article_number":"129","oa_version":"Published Version","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications ","has_accepted_license":"1","conference":{"start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","location":"Athens, Greece","end_date":"2019-10-25"},"language":[{"iso":"eng"}]},{"date_updated":"2021-01-12T08:09:28Z","citation":{"chicago":"Chatterjee, Krishnendu, and Nir Piterman. “Combinations of Qualitative Winning for Stochastic Parity Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.6.","ieee":"K. Chatterjee and N. Piterman, “Combinations of Qualitative Winning for Stochastic Parity Games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","ama":"Chatterjee K, Piterman N. Combinations of Qualitative Winning for Stochastic Parity Games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.6","apa":"Chatterjee, K., & Piterman, N. (2019). Combinations of Qualitative Winning for Stochastic Parity Games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.6","ista":"Chatterjee K, Piterman N. 2019. Combinations of Qualitative Winning for Stochastic Parity Games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 6.","short":"K. Chatterjee, N. Piterman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","mla":"Chatterjee, Krishnendu, and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. Vol. 140, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.6."},"year":"2019","abstract":[{"lang":"eng","text":"We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. "}],"doi":"10.4230/LIPICS.CONCUR.2019.6","day":"01","ddc":["000"],"volume":140,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Piterman","first_name":"Nir","full_name":"Piterman, Nir"}],"_id":"6889","scopus_import":1,"title":"Combinations of Qualitative Winning for Stochastic Parity Games","alternative_title":["LIPIcs"],"intvolume":" 140","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-09-18T08:11:43Z","file_date_updated":"2020-07-14T12:47:43Z","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2019-08-01T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"file_id":"6923","creator":"kschuh","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:43Z","file_name":"2019_LIPIcs_Chatterjee.pdf","content_type":"application/pdf","date_created":"2019-10-01T08:49:45Z","checksum":"7b2ecfd4d9d02360308c0ca986fc10a7","file_size":509163}],"has_accepted_license":"1","month":"08","article_number":"6","oa_version":"Published Version","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"conference":{"start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory","location":"Amsterdam, Netherlands","end_date":"2019-08-30"}},{"oa":1,"publication_identifier":{"issn":["0302-9743"],"eisbn":["9783030302818"],"isbn":["9783030302801"]},"date_published":"2019-09-04T00:00:00Z","type":"conference","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1906.08178"}],"month":"09","oa_version":"Preprint","project":[{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"publication":"16th International Conference on Quantitative Evaluation of Systems","conference":{"location":"Glasgow, United Kingdom","end_date":"2019-09-12","start_date":"2019-09-10","name":"QEST: Quantitative Evaluation of Systems"},"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of 𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees."}],"doi":"10.1007/978-3-030-30281-8_7","arxiv":1,"day":"04","isi":1,"external_id":{"arxiv":["1906.08178"],"isi":["000679281300007"]},"date_updated":"2025-06-02T08:53:47Z","year":"2019","citation":{"ista":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019. Strategy representation by decision trees with linear classifiers. 16th International Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11785, 109–128.","mla":"Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear Classifiers.” 16th International Conference on Quantitative Evaluation of Systems, vol. 11785, Springer Nature, 2019, pp. 109–28, doi:10.1007/978-3-030-30281-8_7.","short":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman, in:, 16th International Conference on Quantitative Evaluation of Systems, Springer Nature, 2019, pp. 109–128.","chicago":"Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear Classifiers.” In 16th International Conference on Quantitative Evaluation of Systems, 11785:109–28. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-30281-8_7.","ieee":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman, “Strategy representation by decision trees with linear classifiers,” in 16th International Conference on Quantitative Evaluation of Systems, Glasgow, United Kingdom, 2019, vol. 11785, pp. 109–128.","apa":"Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., & Toman, V. (2019). Strategy representation by decision trees with linear classifiers. In 16th International Conference on Quantitative Evaluation of Systems (Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. https://doi.org/10.1007/978-3-030-30281-8_7","ama":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy representation by decision trees with linear classifiers. In: 16th International Conference on Quantitative Evaluation of Systems. Vol 11785. Springer Nature; 2019:109-128. doi:10.1007/978-3-030-30281-8_7"},"volume":11785,"title":"Strategy representation by decision trees with linear classifiers","alternative_title":["LNCS"],"intvolume":" 11785","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ChLa"}],"date_created":"2019-10-14T06:57:49Z","article_processing_charge":"No","author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Křetínský","full_name":"Křetínský, Jan"},{"id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","last_name":"Lampert","first_name":"Christoph","full_name":"Lampert, Christoph","orcid":"0000-0001-8622-7887"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"_id":"6942","scopus_import":"1","publisher":"Springer Nature","page":"109-128","quality_controlled":"1"},{"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00317"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","related_material":{"record":[{"status":"public","id":"639","relation":"earlier_version"},{"id":"8934","relation":"dissertation_contains","status":"public"}]},"date_published":"2019-10-01T00:00:00Z","type":"journal_article","oa":1,"language":[{"iso":"eng"}],"publication":"ACM Transactions on Programming Languages and Systems","oa_version":"Preprint","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"month":"10","article_number":"20","volume":41,"date_updated":"2025-06-02T08:53:47Z","year":"2019","citation":{"ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst-case analysis of recursive programs,” ACM Transactions on Programming Languages and Systems, vol. 41, no. 4. ACM, 2019.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” ACM Transactions on Programming Languages and Systems. ACM, 2019. https://doi.org/10.1145/3339984.","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 2019;41(4). doi:10.1145/3339984","apa":"Chatterjee, K., Fu, H., & Goharshady, A. K. (2019). Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. ACM. https://doi.org/10.1145/3339984","ista":"Chatterjee K, Fu H, Goharshady AK. 2019. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 41(4), 20.","mla":"Chatterjee, Krishnendu, et al. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” ACM Transactions on Programming Languages and Systems, vol. 41, no. 4, 20, ACM, 2019, doi:10.1145/3339984.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019)."},"isi":1,"external_id":{"isi":["000564108400001"],"arxiv":["1705.00317"]},"doi":"10.1145/3339984","arxiv":1,"day":"01","abstract":[{"lang":"eng","text":"We study the problem of developing efficient approaches for proving\r\nworst-case bounds of non-deterministic recursive programs. Ranking functions\r\nare sound and complete for proving termination and worst-case bounds of\r\nnonrecursive programs. First, we apply ranking functions to recursion,\r\nresulting in measure functions. We show that measure functions provide a sound\r\nand complete approach to prove worst-case bounds of non-deterministic recursive\r\nprograms. Our second contribution is the synthesis of measure functions in\r\nnonpolynomial forms. We show that non-polynomial measure functions with\r\nlogarithm and exponentiation can be synthesized through abstraction of\r\nlogarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem\r\nusing linear programming. While previous methods obtain worst-case polynomial\r\nbounds, our approach can synthesize bounds of the form $\\mathcal{O}(n\\log n)$\r\nas well as $\\mathcal{O}(n^r)$ where $r$ is not an integer. We present\r\nexperimental results to demonstrate that our approach can obtain efficiently\r\nworst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the\r\ndivide-and-conquer algorithm for the Closest-Pair problem, where we obtain\r\n$\\mathcal{O}(n \\log n)$ worst-case bound, and (ii) Karatsuba's algorithm for\r\npolynomial multiplication and Strassen's algorithm for matrix multiplication,\r\nwhere we obtain $\\mathcal{O}(n^r)$ bound such that $r$ is not an integer and\r\nclose to the best-known bounds for the respective algorithms."}],"quality_controlled":"1","ec_funded":1,"publisher":"ACM","article_type":"original","_id":"7014","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"issue":"4","publication_status":"published","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2019-11-13T08:33:43Z","title":"Non-polynomial worst-case analysis of recursive programs","intvolume":" 41"},{"publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-02-10T22:59:17Z","article_processing_charge":"No","title":"Termination of nondeterministic probabilistic programs","alternative_title":["LNCS"],"intvolume":" 11388","_id":"5948","scopus_import":"1","author":[{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer Nature","page":"468-490","quality_controlled":"1","doi":"10.1007/978-3-030-11245-5_22","arxiv":1,"day":"11","abstract":[{"lang":"eng","text":"We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs."}],"date_updated":"2025-06-02T08:53:41Z","year":"2019","citation":{"short":"H. Fu, K. Chatterjee, in:, International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2019, pp. 468–490.","mla":"Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 11388, Springer Nature, 2019, pp. 468–90, doi:10.1007/978-3-030-11245-5_22.","ista":"Fu H, Chatterjee K. 2019. Termination of nondeterministic probabilistic programs. International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 11388, 468–490.","ama":"Fu H, Chatterjee K. Termination of nondeterministic probabilistic programs. In: International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 11388. Springer Nature; 2019:468-490. doi:10.1007/978-3-030-11245-5_22","apa":"Fu, H., & Chatterjee, K. (2019). Termination of nondeterministic probabilistic programs. In International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 11388, pp. 468–490). Cascais, Portugal: Springer Nature. https://doi.org/10.1007/978-3-030-11245-5_22","chicago":"Fu, Hongfei, and Krishnendu Chatterjee. “Termination of Nondeterministic Probabilistic Programs.” In International Conference on Verification, Model Checking, and Abstract Interpretation, 11388:468–90. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-11245-5_22.","ieee":"H. Fu and K. Chatterjee, “Termination of nondeterministic probabilistic programs,” in International Conference on Verification, Model Checking, and Abstract Interpretation, Cascais, Portugal, 2019, vol. 11388, pp. 468–490."},"isi":1,"external_id":{"isi":["000931943000022"],"arxiv":["1701.02944"]},"volume":11388,"oa_version":"Preprint","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"month":"01","publication":"International Conference on Verification, Model Checking, and Abstract Interpretation","conference":{"location":"Cascais, Portugal","end_date":"2019-01-15","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation","start_date":"2019-01-13"},"language":[{"iso":"eng"}],"date_published":"2019-01-11T00:00:00Z","type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/1701.02944"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public"},{"language":[{"iso":"eng"}],"conference":{"location":"Seoul, Korea","end_date":"2019-05-17","name":"IEEE International Conference on Blockchain and Cryptocurrency","start_date":"2019-05-14"},"publication":"IEEE International Conference on Blockchain and Cryptocurrency","month":"05","article_number":"8751326","oa_version":"Preprint","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1902.07986"}],"date_published":"2019-05-01T00:00:00Z","type":"conference","oa":1,"quality_controlled":"1","ec_funded":1,"publisher":"IEEE","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arash","last_name":"Pourdamghani","full_name":"Pourdamghani, Arash"}],"_id":"6056","scopus_import":1,"title":"Probabilistic smart contracts: Secure randomness on the blockchain","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2019-02-26T09:03:15Z","external_id":{"arxiv":["1902.07986"]},"date_updated":"2024-03-25T23:30:18Z","citation":{"apa":"Chatterjee, K., Goharshady, A. K., & Pourdamghani, A. (2019). Probabilistic smart contracts: Secure randomness on the blockchain. In IEEE International Conference on Blockchain and Cryptocurrency. Seoul, Korea: IEEE. https://doi.org/10.1109/BLOC.2019.8751326","ama":"Chatterjee K, Goharshady AK, Pourdamghani A. Probabilistic smart contracts: Secure randomness on the blockchain. In: IEEE International Conference on Blockchain and Cryptocurrency. IEEE; 2019. doi:10.1109/BLOC.2019.8751326","ieee":"K. Chatterjee, A. K. Goharshady, and A. Pourdamghani, “Probabilistic smart contracts: Secure randomness on the blockchain,” in IEEE International Conference on Blockchain and Cryptocurrency, Seoul, Korea, 2019.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Arash Pourdamghani. “Probabilistic Smart Contracts: Secure Randomness on the Blockchain.” In IEEE International Conference on Blockchain and Cryptocurrency. IEEE, 2019. https://doi.org/10.1109/BLOC.2019.8751326.","short":"K. Chatterjee, A.K. Goharshady, A. Pourdamghani, in:, IEEE International Conference on Blockchain and Cryptocurrency, IEEE, 2019.","mla":"Chatterjee, Krishnendu, et al. “Probabilistic Smart Contracts: Secure Randomness on the Blockchain.” IEEE International Conference on Blockchain and Cryptocurrency, 8751326, IEEE, 2019, doi:10.1109/BLOC.2019.8751326.","ista":"Chatterjee K, Goharshady AK, Pourdamghani A. 2019. Probabilistic smart contracts: Secure randomness on the blockchain. IEEE International Conference on Blockchain and Cryptocurrency. IEEE International Conference on Blockchain and Cryptocurrency, 8751326."},"year":"2019","abstract":[{"text":"In today's programmable blockchains, smart contracts are limited to being deterministic and non-probabilistic. This lack of randomness is a consequential limitation, given that a wide variety of real-world financial contracts, such as casino games and lotteries, depend entirely on randomness. As a result, several ad-hoc random number generation approaches have been developed to be used in smart contracts. These include ideas such as using an oracle or relying on the block hash. However, these approaches are manipulatable, i.e. their output can be tampered with by parties who might not be neutral, such as the owner of the oracle or the miners.We propose a novel game-theoretic approach for generating provably unmanipulatable pseudorandom numbers on the blockchain. Our approach allows smart contracts to access a trustworthy source of randomness that does not rely on potentially compromised miners or oracles, hence enabling the creation of a new generation of smart contracts that are not limited to being non-probabilistic and can be drawn from the much more general class of probabilistic programs.","lang":"eng"}],"arxiv":1,"doi":"10.1109/BLOC.2019.8751326","day":"01"},{"oa":1,"date_published":"2019-06-08T00:00:00Z","type":"conference","related_material":{"record":[{"status":"public","id":"5457","relation":"earlier_version"},{"id":"8934","relation":"dissertation_contains","status":"public"}]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"access_level":"open_access","relation":"main_file","creator":"akafshda","file_id":"6176","checksum":"703a5e9b8c8587f2a44085ffd9a4db64","file_size":4051066,"date_created":"2019-03-25T10:11:22Z","file_name":"paper.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:20Z"}],"month":"06","oa_version":"Submitted Version","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"publication":"PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","has_accepted_license":"1","conference":{"name":"PLDI: Conference on Programming Language Design and Implementation","start_date":"2019-06-22","end_date":"2019-06-26","location":"Phoenix, AZ, United States"},"language":[{"iso":"eng"}],"keyword":["Program Cost Analysis","Program Termination","Probabilistic Programs","Martingales"],"abstract":[{"text":"We consider the problem of expected cost analysis over nondeterministic probabilistic programs,\r\nwhich aims at automated methods for analyzing the resource-usage of such programs.\r\nPrevious approaches for this problem could only handle nonnegative bounded costs.\r\nHowever, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols,\r\nboth positive and negative costs are necessary and the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and efficient approach to obtain polynomial bounds on the\r\nexpected accumulated cost of nondeterministic probabilistic programs.\r\nOur approach can handle (a) general positive and negative costs with bounded updates in\r\nvariables; and (b) nonnegative costs with general updates to variables.\r\nWe show that several natural examples which could not be\r\nhandled by previous approaches are captured in our framework.\r\n\r\nMoreover, our approach leads to an efficient polynomial-time algorithm, while no\r\nprevious approach for cost analysis of probabilistic programs could guarantee polynomial runtime.\r\nFinally, we show the effectiveness of our approach using experimental results on a variety of programs for which we efficiently synthesize tight resource-usage bounds.","lang":"eng"}],"arxiv":1,"doi":"10.1145/3314221.3314581","day":"08","isi":1,"external_id":{"arxiv":["1902.04659"],"isi":["000523190300014"]},"date_updated":"2025-06-02T08:53:45Z","citation":{"ista":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. 2019. Cost analysis of nondeterministic probabilistic programs. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 204–220.","mla":"Wang, Peixin, et al. “Cost Analysis of Nondeterministic Probabilistic Programs.” PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2019, pp. 204–20, doi:10.1145/3314221.3314581.","short":"P. Wang, H. Fu, A.K. Goharshady, K. Chatterjee, X. Qin, W. Shi, in:, PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2019, pp. 204–220.","ieee":"P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi, “Cost analysis of nondeterministic probabilistic programs,” in PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Phoenix, AZ, United States, 2019, pp. 204–220.","chicago":"Wang, Peixin, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. “Cost Analysis of Nondeterministic Probabilistic Programs.” In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 204–20. Association for Computing Machinery, 2019. https://doi.org/10.1145/3314221.3314581.","apa":"Wang, P., Fu, H., Goharshady, A. K., Chatterjee, K., Qin, X., & Shi, W. (2019). Cost analysis of nondeterministic probabilistic programs. In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 204–220). Phoenix, AZ, United States: Association for Computing Machinery. https://doi.org/10.1145/3314221.3314581","ama":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. Cost analysis of nondeterministic probabilistic programs. In: PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2019:204-220. doi:10.1145/3314221.3314581"},"year":"2019","ddc":["000"],"title":"Cost analysis of nondeterministic probabilistic programs","publication_status":"published","article_processing_charge":"No","department":[{"_id":"KrCh"}],"date_created":"2019-03-25T10:13:25Z","author":[{"first_name":"Peixin","last_name":"Wang","full_name":"Wang, Peixin"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Qin, Xudong","last_name":"Qin","first_name":"Xudong"},{"full_name":"Shi, Wenjun","first_name":"Wenjun","last_name":"Shi"}],"_id":"6175","scopus_import":"1","publisher":"Association for Computing Machinery","file_date_updated":"2020-07-14T12:47:20Z","page":"204-220","ec_funded":1,"quality_controlled":"1"},{"oa_version":"Submitted Version","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"month":"04","publication":"Proceedings of the 34th ACM Symposium on Applied Computing","has_accepted_license":"1","conference":{"name":"ACM Symposium on Applied Computing","start_date":"2019-04-08","location":"Limassol, Cyprus","end_date":"2019-04-12"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450359337"]},"oa":1,"date_published":"2019-04-01T00:00:00Z","type":"conference","file":[{"content_type":"application/pdf","file_name":"2019_ACM_Chatterjee.pdf","date_updated":"2020-07-14T12:47:29Z","checksum":"fbfbcd5a0c7a743862bfc3045539a614","file_size":1023934,"date_created":"2019-05-06T12:09:27Z","creator":"dernst","file_id":"6379","relation":"main_file","access_level":"open_access"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"status":"public","publication_status":"published","date_created":"2019-05-06T12:11:36Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"pubrep_id":"1069","title":"Hybrid Mining: Exploiting blockchain’s computational power for distributed problem solving","_id":"6378","scopus_import":"1","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arash","last_name":"Pourdamghani","full_name":"Pourdamghani, Arash"}],"publisher":"ACM","page":"374-381","quality_controlled":"1","ec_funded":1,"file_date_updated":"2020-07-14T12:47:29Z","doi":"10.1145/3297280.3297319","day":"01","abstract":[{"lang":"eng","text":"In today's cryptocurrencies, Hashcash proof of work is the most commonly-adopted approach to mining. In Hashcash, when a miner decides to add a block to the chain, she has to solve the difficult computational puzzle of inverting a hash function. While Hashcash has been successfully adopted in both Bitcoin and Ethereum, it has attracted significant and harsh criticism due to its massive waste of electricity, its carbon footprint and environmental effects, and the inherent lack of usefulness in inverting a hash function. Various other mining protocols have been suggested, including proof of stake, in which a miner's chance of adding the next block is proportional to her current balance. However, such protocols lead to a higher entry cost for new miners who might not still have any stake in the cryptocurrency, and can in the worst case lead to an oligopoly, where the rich have complete control over mining. In this paper, we propose Hybrid Mining: a new mining protocol that combines solving real-world useful problems with Hashcash. Our protocol allows new miners to join the network by taking part in Hashcash mining without having to own an initial stake. It also allows nodes of the network to submit hard computational problems whose solutions are of interest in the real world, e.g.~protein folding problems. Then, miners can choose to compete in solving these problems, in lieu of Hashcash, for adding a new block. Hence, Hybrid Mining incentivizes miners to solve useful problems, such as hard computational problems arising in biology, in a distributed manner. It also gives researchers in other areas an easy-to-use tool to outsource their hard computations to the blockchain network, which has enormous computational power, by paying a reward to the miner who solves the problem for them. Moreover, our protocol provides strong security guarantees and is at least as resilient to double spending as Bitcoin."}],"date_updated":"2025-06-02T08:53:46Z","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, and A. Pourdamghani, “Hybrid Mining: Exploiting blockchain’s computational power for distributed problem solving,” in Proceedings of the 34th ACM Symposium on Applied Computing, Limassol, Cyprus, 2019, vol. Part F147772, pp. 374–381.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Arash Pourdamghani. “Hybrid Mining: Exploiting Blockchain’s Computational Power for Distributed Problem Solving.” In Proceedings of the 34th ACM Symposium on Applied Computing, Part F147772:374–81. ACM, 2019. https://doi.org/10.1145/3297280.3297319.","apa":"Chatterjee, K., Goharshady, A. K., & Pourdamghani, A. (2019). Hybrid Mining: Exploiting blockchain’s computational power for distributed problem solving. In Proceedings of the 34th ACM Symposium on Applied Computing (Vol. Part F147772, pp. 374–381). Limassol, Cyprus: ACM. https://doi.org/10.1145/3297280.3297319","ama":"Chatterjee K, Goharshady AK, Pourdamghani A. Hybrid Mining: Exploiting blockchain’s computational power for distributed problem solving. In: Proceedings of the 34th ACM Symposium on Applied Computing. Vol Part F147772. ACM; 2019:374-381. doi:10.1145/3297280.3297319","ista":"Chatterjee K, Goharshady AK, Pourdamghani A. 2019. Hybrid Mining: Exploiting blockchain’s computational power for distributed problem solving. Proceedings of the 34th ACM Symposium on Applied Computing. ACM Symposium on Applied Computing vol. Part F147772, 374–381.","short":"K. Chatterjee, A.K. Goharshady, A. Pourdamghani, in:, Proceedings of the 34th ACM Symposium on Applied Computing, ACM, 2019, pp. 374–381.","mla":"Chatterjee, Krishnendu, et al. “Hybrid Mining: Exploiting Blockchain’s Computational Power for Distributed Problem Solving.” Proceedings of the 34th ACM Symposium on Applied Computing, vol. Part F147772, ACM, 2019, pp. 374–81, doi:10.1145/3297280.3297319."},"year":"2019","isi":1,"external_id":{"isi":["000474685800049"]},"volume":"Part F147772","ddc":["004"]},{"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Okati","first_name":"Nastaran","full_name":"Okati, Nastaran"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis"}],"issue":"POPL","_id":"6380","pubrep_id":"1056","title":"Efficient parameterized algorithms for data packing","intvolume":" 3","publication_status":"published","date_created":"2019-05-06T12:18:17Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:47:29Z","quality_controlled":"1","ec_funded":1,"publisher":"ACM","date_updated":"2024-03-25T23:30:18Z","citation":{"short":"K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 3 (2019).","mla":"Chatterjee, Krishnendu, et al. “Efficient Parameterized Algorithms for Data Packing.” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 53, ACM, 2019, doi:10.1145/3290366.","ista":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. 2019. Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. 3(POPL), 53.","ama":"Chatterjee K, Goharshady AK, Okati N, Pavlogiannis A. Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. 2019;3(POPL). doi:10.1145/3290366","apa":"Chatterjee, K., Goharshady, A. K., Okati, N., & Pavlogiannis, A. (2019). Efficient parameterized algorithms for data packing. Proceedings of the ACM on Programming Languages. ACM. https://doi.org/10.1145/3290366","ieee":"K. Chatterjee, A. K. Goharshady, N. Okati, and A. Pavlogiannis, “Efficient parameterized algorithms for data packing,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL. ACM, 2019.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis. “Efficient Parameterized Algorithms for Data Packing.” Proceedings of the ACM on Programming Languages. ACM, 2019. https://doi.org/10.1145/3290366."},"year":"2019","abstract":[{"text":"There is a huge gap between the speeds of modern caches and main memories, and therefore cache misses account for a considerable loss of efficiency in programs. The predominant technique to address this issue has been Data Packing: data elements that are frequently accessed within time proximity are packed into the same cache block, thereby minimizing accesses to the main memory. We consider the algorithmic problem of Data Packing on a two-level memory system. Given a reference sequence R of accesses to data elements, the task is to partition the elements into cache blocks such that the number of cache misses on R is minimized. The problem is notoriously difficult: it is NP-hard even when the cache has size 1, and is hard to approximate for any cache size larger than 4. Therefore, all existing techniques for Data Packing are based on heuristics and lack theoretical guarantees. In this work, we present the first positive theoretical results for Data Packing, along with new and stronger negative results. We consider the problem under the lens of the underlying access hypergraphs, which are hypergraphs of affinities between the data elements, where the order of an access hypergraph corresponds to the size of the affinity group. We study the problem parameterized by the treewidth of access hypergraphs, which is a standard notion in graph theory to measure the closeness of a graph to a tree. Our main results are as follows: We show there is a number q* depending on the cache parameters such that (a) if the access hypergraph of order q* has constant treewidth, then there is a linear-time algorithm for Data Packing; (b)the Data Packing problem remains NP-hard even if the access hypergraph of order q*-1 has constant treewidth. Thus, we establish a fine-grained dichotomy depending on a single parameter, namely, the highest order among access hypegraphs that have constant treewidth; and establish the optimal value q* of this parameter. Finally, we present an experimental evaluation of a prototype implementation of our algorithm. Our results demonstrate that, in practice, access hypergraphs of many commonly-used algorithms have small treewidth. We compare our approach with several state-of-the-art heuristic-based algorithms and show that our algorithm leads to significantly fewer cache-misses. ","lang":"eng"}],"doi":"10.1145/3290366","day":"01","ddc":["004"],"volume":3,"publication":"Proceedings of the ACM on Programming Languages","has_accepted_license":"1","month":"01","article_number":"53","oa_version":"Published Version","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"language":[{"iso":"eng"}],"date_published":"2019-01-01T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"issn":["2475-1421"]},"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"date_created":"2019-05-06T12:23:11Z","file_size":1294962,"checksum":"c157752f96877b36685ad7063ada4524","date_updated":"2020-07-14T12:47:29Z","file_name":"2019_ACM_POPL_Chatterjee.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"6381","creator":"dernst"}]},{"article_processing_charge":"No","date_created":"2021-10-27T14:57:06Z","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"publication_status":"published","intvolume":" 3","title":"Value-centric dynamic partial order reduction","_id":"10190","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","first_name":"Viktor","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"publisher":"ACM","quality_controlled":"1","file_date_updated":"2021-11-12T11:41:56Z","day":"10","arxiv":1,"doi":"10.1145/3360550","abstract":[{"lang":"eng","text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning."}],"year":"2019","citation":{"apa":"Chatterjee, K., Pavlogiannis, A., & Toman, V. (2019). Value-centric dynamic partial order reduction. In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vol. 3). Athens, Greece: ACM. https://doi.org/10.1145/3360550","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. Vol 3. ACM; 2019. doi:10.1145/3360550","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Athens, Greece, 2019, vol. 3.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Vol. 3. ACM, 2019. https://doi.org/10.1145/3360550.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, vol. 3, 124, ACM, 2019, doi:10.1145/3360550.","ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124."},"date_updated":"2025-07-14T09:10:15Z","external_id":{"arxiv":["1909.00989"]},"acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","volume":3,"ddc":["000"],"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","article_number":"124","month":"10","has_accepted_license":"1","publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","conference":{"name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","start_date":"2019-10-23","location":"Athens, Greece","end_date":"2019-10-25"},"keyword":["safety","risk","reliability and quality","software"],"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["2475-1421"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2019-10-10T00:00:00Z","file":[{"access_level":"open_access","relation":"main_file","success":1,"creator":"cchlebak","file_id":"10278","file_size":570829,"checksum":"2149979c46964c4d117af06ccb6c0834","date_created":"2021-11-12T11:41:56Z","content_type":"application/pdf","file_name":"2019_ACM_Chatterjee.pdf","date_updated":"2021-11-12T11:41:56Z"}],"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3360550","open_access":"1"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","related_material":{"record":[{"id":"10199","relation":"dissertation_contains","status":"public"}]}}]