Model checking separator logic on graphs that exclude a fixed topological minor.
- Prelegent(ci)
- Szymon Toruńczyk
- Afiliacja
- MIM UW
- Termin
- 6 października 2021 14:15
- Pokój
- p. 5050
- Seminarium
- Seminarium „Teoria automatów”
We consider separator logic on graphs introduced recently
by Bojańczyk, and independently by Siebertz, Shrader, and Vigny.
This logic extends first-order logic by atomic predicates of arity k+2, for each k, expressing
that every path from a vertex s to a vertex t must pass through one of the vertices v_1,...,v_k.
We prove that the model checking problem for this logic is fixed parameter tractable
on every class of graphs that excludes a fixed topological minor.
To this end, we decompose each graph from such a class in a treelike
fashion and run a variant of a tree automaton on the obtained tree decomposition.
This is joint work with Siebertz, Shrader, Mi. Pilipczuk, and Vigny.