Evènement pour le groupe Séminaire Méthodes Formelles


Date 2021-03-16  07:00-07:00
TitreSubcubic Certificates for CFL Reachability  
RésuméThe context-free language (CFL) reachability problem on graphs, as well as a closely related problem of language emptiness for pushdown automata, are core problems in interprocedural program analysis and model checking, respectively. Both can be solved in cubic time but, despite years of efforts, there are no truly sub-cubic algorithms known for either. We study the related certification task: given a problem instance, are there small and efficiently checkable certificates for the existence and for the non-existence of a path (or language non-emptiness and emptiness, respectively)? We show that, in both scenarios, there exist succinct certificates (O(n^2) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. A natural question is whether faster algorithms for CFL reachability or PDA emptiness will lead to faster algorithms for other combinatorial problems such as SAT. As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability or PDA emptiness for a conditional lower bound stronger than $n^omega$, unless the nondeterministic strong exponential-time hypothesis (NSETH) fails. This is joint work with Rupak Majumdar and Philipp Schepper. A preprint is available at https://arxiv.org/abs/2102.13095 . Enregistrement : https://u-bordeaux-fr.zoom.us/rec/share/kcrUh-SsH97onePRKAyCrw_B2H7Y2iVQAbGVLdumtgI_0-ZMCnxflRjbBeVv5iCH.Qzri0hDgia6JjQnU 
LieuOnline 
OrateurDmitry Chistikov 
Emailhttps://warwick.ac.uk/fac/sci/dcs/people/dmitry_chistikov/ 
UrlThe University of Warwick 



Aucun document lié à cet événement.

Retour
Retour à l'index