NDLI: Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition

Content Provider	ACM Digital Library
Author	Chatterjee, Krishnendu Henzinger, Monika
Copyright Year	2014
Abstract	The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is $\textit{Õ}(\textit{n}$ ṡ $\textit{m}),$ where $\textit{n}$ is the number of vertices and $\textit{m}$ is the number of edges in the graph. We are the first to break the $\textit{Õ}(\textit{n}$ ṡ $\textit{m})$ boundary by presenting a new technique that reduces the running time to $O(n^{2}).$ This bound also leads to $O(n^{2})-time$ algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of $\textit{Õ}(\textit{n}$ ṡ $\textit{m})),$ (2) in concurrent graph games with constant actions (improving an earlier bound of $O(n^{3})),$ and (3) in Markov decision processes (improving for $m>n^{4/3}$ an earlier bound of $\textit{O}(\textit{m}$ ṡ $√\textit{m})).$ We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in $\textit{O}(\textit{n})$ amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an $\textit{O}(\textit{m}$ ṡ $√\textit{m})-time$ algorithm, and our second algorithm is an $O(n^{2})-time$ algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an $\textit{O}(min$ &lcu;m ṡ $√m,n^{2}})-time$ algorithm improving the long-standing $\textit{O}(\textit{n}$ ṡ $\textit{m})$ time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in $\textit{O}(\textit{n})$ amortized time per edge deletion, and $\textit{O}(\textit{m})$ worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.
Starting Page	1
Ending Page	40
Page Count	40
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/2597631
Journal	Journal of the ACM (JACM)
Volume Number	61
Issue Number	3
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-06-02
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Büchi objectives Graph games Dynamic graph algorithms Graph algorithms Verification and synthesis
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence 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

Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification

Subexponential Algorithms for Unique Games and Related Problems

Randomized fully dynamic graph algorithms with polylogarithmic time per operation

Efficient implementation of graph algorithms using contraction

A VLSI decomposition of the deBruijn graph

Sparsification—a technique for speeding up dynamic graph algorithms

Fully dynamic planarity testing with applications

Alternating-time temporal logic

Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification.

Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition

Similar Documents

Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification

Subexponential Algorithms for Unique Games and Related Problems

Randomized fully dynamic graph algorithms with polylogarithmic time per operation

Efficient implementation of graph algorithms using contraction

A VLSI decomposition of the deBruijn graph

Sparsification—a technique for speeding up dynamic graph algorithms

Fully dynamic planarity testing with applications

Alternating-time temporal logic

Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification.

Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition