NDLI: Mean-Payoff Pushdown Games

Content Provider	IEEE Xplore Digital Library
Author	Chatterjee, K. Velner, Y.
Copyright Year	2012
Abstract	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 solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and parity objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean payoff objectives. 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, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two-player pushdown games. Finally we also show that all the problems have the same computational complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.
Starting Page	195
Ending Page	204
File Size	302355
Page Count	10
File Format	PDF
ISBN	9781467322638
ISSN	10436871
DOI	10.1109/LICS.2012.30
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2012-06-25
Publisher Place	Croatia
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Games Polynomials Complexity theory History Heuristic algorithms Automata Computer science Pushdown automata Games on graphs Pushdown games Meanpayoff objectives
Content Type	Text
Resource Type	Article
Subject	Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Mean-Payoff Pushdown Games

Winning Regions of Higher-Order Pushdown Games

Star Height via Games

Reachability Games and Game Semantics: Comparing Nondeterministic Programs

Defining Winning Strategies in Fixed-Point Logic

Multidimensional beyond Worst-Case and Almost-Sure Problems for Mean-Payoff Objectives

Symmetry Coincides with Nondeterminism for Time-Bounded Auxiliary Pushdown Automata

Mean-Payoff Pushdown Games

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Mean-Payoff Pushdown Games

Similar Documents

Mean-Payoff Pushdown Games

Winning Regions of Higher-Order Pushdown Games

Star Height via Games

Reachability Games and Game Semantics: Comparing Nondeterministic Programs

Defining Winning Strategies in Fixed-Point Logic

Multidimensional beyond Worst-Case and Almost-Sure Problems for Mean-Payoff Objectives

Symmetry Coincides with Nondeterminism for Time-Bounded Auxiliary Pushdown Automata

Mean-Payoff Pushdown Games

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Mean-Payoff Pushdown Games