Lista referatów

• 2021-10-27, godz. 14:15, 5050

  Paweł Parys (MIM UW)

  Higher-Order Model Checking Step by Step

  I will show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. Recursion scheme is a formalism to represent/generate an infinite tree, e...

• 2021-10-20, godz. 14:15, 5050

  Jakub Gajarsky (MIM UW)

  Differential games, locality, and model checking for FO logic of graphs

  We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraisse games in which the game is played on one graph only and the moves of both players are restricted. We prove that these games are strong enough to capture essential information about graphs from graph classes whic...

• 2021-10-13, godz. 14:15, 5050

  Michał Skrzypczak (MIM UW)

  Guidable automata and their index problem

  Rabin's theorem relies on the equivalence between Monadic Second-Order logic and non-deterministic automata over infinite trees. The non-determinism of the involved model is known to be "inherent", both in terms of descriptive complexity and from the standpoint of uniformisability / unambiguity. As ...

• 2021-10-06, godz. 14:15, 5050

  Szymon Toruńczyk (MIM UW)

  Model checking separator logic on graphs that exclude a fixed topological minor.

  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 ver...

• 2021-06-30, godz. 14:15, online

  Albert Gutowski (MIM UW)

  Finite entailment of non-local queries in description logics

  We study the problem of finite entailment of ontology-mediated queries. In particular, we are interested in non-local queries. Recent studies show that a vast majority of user-issued CRPQs only use Kleene star over unions of roles. We show how to answer such simple CRPQs, mediated by ontologies exp...

• 2021-06-23, godz. 14:15, online

  Andrzej Murawski (University of Oxford)

  Verifying higher-order concurrency with data automata

  Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model. Our first contribution is an aut...

• 2021-06-16, godz. 14:15, online

  Lê Thành Dũng (Tito) Nguyễn (LIPN (Paris Nord))

  Comparison-free polyregular functions

  We introduce a new automata-theoretic class of string-to-string functions with polynomial growth. Several equivalent definitions are provided: a machine model which is a restricted variant of pebble transducers, and a few inductive definitions that close the class of regular functions under certain ...

• 2021-06-09, godz. 14:15, online

  Amina Doumane (CNRS-ENS Lyon)

  Regular expressions for languages of graphs of tree-width 2

  I propose a syntax of regular expressions which capture exactly CMSO definable languages of graphs of tree-width 2. A similar syntax is given for CMSO definable languages of series-parallel graphs and of connected tree-width 2 graphs....

• 2021-06-02, godz. 14:15, online

  Gaëtan Douéneau (IRIF, Université de Paris)

  Pebble transducers with unary output

  Bojańczyk recently initiated an intensive study of deterministic pebble transducers, which are two-way automata that can drop marks (named "pebbles") on their input word, and produce an output word. They describe functions from words to words. Two natural restrictions of this definition have been i...

• 2021-05-26, godz. 14:15, online

  Sandra Kiefer (MIM UW)

  Logarithmic Weisfeiler-Leman Identifies All Planar Graphs

  The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs that is widely used in graph-isomorphism tests. It proceeds by iteratively computing vertex colours. The number of iterations needed to obtain the final output is crucial for the parallelis...

Strony