Thumbnail
Access Restriction
Subscribed

Author Chatterjee, Krishnendu ♦ Henzinger, Monika
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2014
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Büchi objectives ♦ Graph games ♦ Dynamic graph algorithms ♦ Graph algorithms ♦ Verification and synthesis
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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2014-06-02
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 61
Issue Number 3
Page Count 40
Starting Page 1
Ending Page 40


Open content in new tab

   Open content in new tab
Source: ACM Digital Library