Nie jesteś zalogowany | Zaloguj się

Huge lower bounds of weak logics for data words

Prelegent(ci)
Diego Figueira
Afiliacja
Laboratoire Spécification et Vérification (LSV)
Termin
28 października 2009 14:15
Pokój
p. 5870
Seminarium
Seminarium „Teoria automatów”

I will show how to code very hard problems into the satisfiability of the linear temporal logic (LTL) equipped with one register to store and test data values from positions of a data word. I will show that this lower bound holds even when there only navigational modality is the Future. I will mention some of the consequences this entails for the satisfiability of some fragments of XPath over XML documents. Joint work with Luc Segoufin.