View: session overviewtalk overviewside by side with other conferences

09:00 | SPEAKER: Bruno Courcelle ABSTRACT. A well-known algorithmic meta-theorem states that every graph property expressible by a monadic second-order (MSO in short) sentence possibly using edge set quantifications can be checked in linear time for graphs of bounded tree- width; furthermore, every graph property expressible by an MSO sentence not using edge set quantifications can be checked in linear time for graphs of bounded clique-width given by an appropriate algebraic term. The standard proofs construct from the sentences and the given bounds on tree-width or clique-width automata intended to run on tree-decompositions or clique-width terms. However, they have so many states that these constructions are not usable in practice. This is unavoidable by Frick and Grohe. To overcome this difficulty in cases that are not "toy examples", we have introduced fly-automata that do not store states and transitions but compute them whenever needed. They have been implemented and tested, in particular for checking colorability and so-called acyclic colorability. A subset of the implemented functionalities will be demonstated by using a web interface in the first part of the lecture. |

10:05 | SPEAKER: Lukas Holik ABSTRACT. We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests whether its language is empty. The main novelty is to test the emptiness on the fly, while constructing a symbolic, term-based representation of the automaton, and prune the constructed state space from parts irrelevant to the test. The pruning is done by a generalization of two techniques used in antichain-based language inclusion and universality checking of finite automata: subsumption and early termination. The richer structure of the WS1S decision problem allows us, however, to elaborate on these techniques in novel ways. Our experiments show that the proposed approach can in many cases significantly outperform the classical decision procedure (implemented in the MONA tool) as well as recently proposed alternatives. |

11:00 | Courcelle’s Theorem – A Game-Theoretic Approach SPEAKER: Peter Rossmanith ABSTRACT. Courcelle’s Theorem states that every problem definable in Monadic Second- Order logic can be solved in linear time on structures of bounded treewidth, for example, by constructing a tree automaton that recognizes or rejects a tree decomposition of the structure. Existing, optimized software like the MONA tool can be used to build the corresponding tree automata, which for bounded treewidth are of constant size. Unfortunately, the constants involved can become extremely large – every quantifier alternation requires a power set construction for the automaton. Here, the required space can become a problem in practical applications. We present a direct approach based on model checking games, which avoids the expensive power set construction. The resulting tool solves some problems on graphs quite efficiently if the treewidth is moderate. |

12:05 | ABSTRACT. Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism for specifying regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e., they escape the simple and natural formalism by translating formulas into equally expressive but less concise regular structures such as finite automata. In this talk, I will present a decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle. |

Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).