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.