--- _id: '2329' abstract: - lang: eng text: 'Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work, we consider both finite-state game graphs, and recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion. The objectives we study are multidimensional mean-payoff objectives, where the goal of player 1 is to ensure that the mean-payoff is non-negative in all dimensions. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation. Our main contributions are as follows: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of the weights are fixed; whereas if the number of dimensions is arbitrary, then the problem is known to be coNP-complete. (2) We show that pushdown graphs with multidimensional mean-payoff objectives can be solved in polynomial time. For both (1) and (2) our algorithms are based on hyperplane separation technique. (3) For pushdown games under global strategies both one and multidimensional mean-payoff objectives problems are known to be undecidable, and we show that under modular strategies the multidimensional problem is also undecidable; under modular strategies the one-dimensional problem is NP-complete. We show that if the number of modules, the number of exits, and the maximal absolute value of the weights are fixed, then pushdown games under modular strategies with one-dimensional mean-payoff objectives can be solved in polynomial time, and if either the number of exits or the number of modules is unbounded, then the problem is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for finite-state multidimensional mean-payoff games or pushdown games under modular strategies with one-dimensional mean-payoff objectives would imply the fixed parameter tractability of parity games.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Yaron full_name: Velner, Yaron last_name: Velner citation: ama: Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional mean-payoff games. 2013;8052:500-515. doi:10.1007/978-3-642-40184-8_35 apa: 'Chatterjee, K., & Velner, Y. (2013). Hyperplane separation technique for multidimensional mean-payoff games. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentinia: Springer. https://doi.org/10.1007/978-3-642-40184-8_35' chicago: Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_35. ieee: K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional mean-payoff games,” vol. 8052. Springer, pp. 500–515, 2013. ista: Chatterjee K, Velner Y. 2013. Hyperplane separation technique for multidimensional mean-payoff games. 8052, 500–515. mla: Chatterjee, Krishnendu, and Yaron Velner. Hyperplane Separation Technique for Multidimensional Mean-Payoff Games. Vol. 8052, Springer, 2013, pp. 500–15, doi:10.1007/978-3-642-40184-8_35. short: K. Chatterjee, Y. Velner, 8052 (2013) 500–515. conference: end_date: 2013-08-30 location: Buenos Aires, Argentinia name: 'CONCUR: Concurrency Theory' start_date: 2013-08-27 date_created: 2018-12-11T11:57:01Z date_published: 2013-08-01T00:00:00Z date_updated: 2023-02-23T13:00:42Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-40184-8_35 ec_funded: 1 external_id: arxiv: - '1210.3141' intvolume: ' 8052' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1210.3141 month: '08' oa: 1 oa_version: Preprint page: 500 - 515 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '4597' quality_controlled: '1' related_material: record: - id: '717' relation: later_version status: public scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Hyperplane separation technique for multidimensional mean-payoff games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8052 year: '2013' ...