Krishnendu Chatterjee
ABSTRACT
Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental ω-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical ω-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives.
- A. Abboud and V. Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. In FOCS, pages 434--443, 2014. Google Scholar
Digital Library
- A. Abboud, V. Vassilevska Williams, and O. Weimann. Consequences of faster alignment of sequences. In ICALP, Proceedings, Part I, pages 39--51, 2014.Google Scholar
- A. Abboud, A. Backurs, and V. Vassilevska Williams. If the current clique algorithms are optimal, so is Valiant's parser. In FOCS, pages 98--117, 2015. Google ScholarDigital Library
- A. Abboud, A. Backurs, and V. Vassilevska Williams. Tight hardness results for LCS and other sequence similarity measures. In FOCS, pages 59--78, 2015. Google ScholarDigital Library
- A. Abboud, V. Vassilevska Williams, and H. Yu. Matching triangles and basing hardness on an extremely popular conjecture. In STOC, pages 41--50, 2015. Google ScholarDigital Library
- A. Abboud, V. Vassilevska Williams, and J. R. Wang. Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs. In SODA, pages 377--391, 2016. Google ScholarDigital Library
- A. Backurs and P. Indyk. Edit distance cannot be computed in strongly subquadratic time (unless SETH is false). In STOC, pages 51--58, 2015. Google ScholarDigital Library
- C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google ScholarDigital Library
- K. Bringmann. Why walking the dog takes time: Frechet distance has no strongly subquadratic algorithms unless SETH fails. In FOCS, pages 661--670, 2014. Google ScholarDigital Library
- K. Bringmann and M. Künnemann. Quadratic conditional lower bounds for string problems and dynamic time warping. In FOCS, pages 79--97, 2015. Google ScholarDigital Library
- C. Calabro, R. Impagliazzo, and R. Paturi. The complexity of satisfiability of small depth circuits. In IWPEC, pages 75--85, 2009. Google ScholarDigital Library
- K. Chatterjee and L. Doyen. Partial-observation stochastic games: How to win when belief fails. ACM Trans. Comput. Log., 15(2):16, 2014. Google ScholarDigital Library
- K. Chatterjee and M. Henzinger. An O(n2) time algorithm for alternating Büchi games. In SODA, pages 1386--1399, 2012. Google ScholarDigital Library
- K. Chatterjee and M. Henzinger. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. Journal of the ACM, 61(3):15, 2014. Google ScholarDigital Library
- K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple stochastic parity games. In CSL, pages 100--113, 2003.Google ScholarCross Ref
- K. Chatterjee, T. A. Henzinger, and N. Piterman. Generalized parity games. In FOSSACS, volume 4423, pages 153--167, 2007. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Qualitative analysis of partially-observable Markov decision processes. In MFCS, pages 258--269, 2010. Google ScholarDigital Library
- K. Chatterjee, L. de Alfaro, and R. Majumdar. The complexity of coverage. Int. J. Found. Comput. Sci., 24(2):165--186, 2013.Google ScholarCross Ref
- K. Chatterjee, M. Henzinger, and V. Loitzenbauer. Improved algorithms for one-pair and k-pair Streett objectives. In LICS, pages 269--280, 2015. Google ScholarDigital Library
- A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: a new symbolic model checker. Int. J. STTT, 2:410--425, 2000.Google ScholarCross Ref
- E. A. Emerson and C. S. Jutla. The complexity of tree automata and logics of programs. SIAM J. Comput., 29(1):132--158, 1999. Google ScholarDigital Library
- N. Fijalkow and F. Horn. The surprizing complexity of reachability games. CoRR, abs/1010.2420, 2010.Google Scholar
- A. Gajentaan and M. H. Overmars. On a class of O(n2) problems in computational geometry. Comput. Geom., 45(4):140--152, 2012. Google ScholarDigital Library
- M. Henzinger, V. King, and T. Warnow. Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology. Algorithmica, 24(1):1--13, 1999.Google ScholarCross Ref
- M. Henzinger and J. A. Telle. Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In SWAT, pages 16--27, 1996. Google ScholarDigital Library
- M. Henzinger, S. Krinninger, D. Nanongkai, and T. Saranurak. Unifying and strengthening hardness for dynamic problems via the online matrix-vector multiplication conjecture. In STOC, pages 21--30, 2015. Google ScholarDigital Library
- G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23 (5):279--295, May 1997. Google ScholarDigital Library
- R. Impagliazzo, R. Paturi, and F. Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512--530, 2001. Google ScholarDigital Library
- M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification of probabilistic real-time systems. In CAV, LNCS 6806, pages 585--591, 2011. Google ScholarDigital Library
- F. Le Gall. Powers of tensors and fast matrix multiplication. In ISSAC, pages 296--303, 2014. Google ScholarDigital Library
- L. Lee. Fast context-free grammar parsing requires fast boolean matrix multiplication. J. ACM, 49(1):1--15, Jan. 2002. Google ScholarDigital Library
- M. Patrascu and R. Williams. On the possibility of faster SAT algorithms. In SODA, pages 1065--1075, 2010. Google ScholarDigital Library
- L. Roditty and U. Zwick. On dynamic shortest paths problems. Algorithmica, 61(2):389--401, 2011. Google ScholarDigital Library
- W. Thomas. On the synthesis of strategies in infinite games. In STACS, LNCS 900, pages 1--13. Springer, 1995.Google Scholar
- W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, vol. 3, Beyond Words, chapter 7, pages 389--455. Springer, 1997. Google ScholarCross Ref
- V. Vassilevska Williams and R. Williams. Subcubic equivalences between path, matrix and triangle problems. In FOCS, pages 645--654, 2010. Google ScholarDigital Library
- R. Williams. A new algorithm for optimal 2-constraint satisfaction and its implications. TCS, 348(2-3):357--365, 2005. Google ScholarDigital Library
- R. Williams. Faster decision of first-order graph properties. In CSL-LICS, pages 80:1--80:6, 2014. Google ScholarDigital Library
- R. Williams. Faster all-pairs shortest paths via circuit complexity. In STOC, pages 664--673, 2014. Google ScholarDigital Library
- P. Wolper. Constructing automata from temporal logic formulas: A tutorial. In Lectures on Formal Methods and Performance Analysis, pages 261--277, 2000. Google ScholarDigital Library
Index Terms
- Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction
Recommendations
Lower Bounds: From Circuits to QBF Proof Systems
ITCS '16: Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer ScienceA general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although ...
Finding even cycles faster via capped k-walks
STOC 2017: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of ComputingFinding cycles in graphs is a fundamental problem in algorithmic graph theory. In this paper, we consider the problem of finding and reporting a cycle of length 2k in an undirected graph G with n nodes and m edges for constant k≥ 2. A classic result by ...
Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds
We give a general transformation that turns polynomial-size Frege proofs into subexponential-size AC0-Frege proofs. This indicates that proving truly exponential lower bounds for AC0-Frege is hard, as it is a long-standing open problem to prove ...
Comments