Abstract. There is a remarkable divide in the field of logic in Computer Science, between two distinct strands: one focussing on semantics and compositionality (``Structure''), the other on expressiveness and complexity (``Power''). It is remarkable because these two fundamental aspects are studied using almost disjoint technical languages and methods, by almost disjoint research communities. We believe that bridging this divide is a major issue in Computer Science, and may hold the key to fundamental advances in the field.
In this talk, we describe a novel approach to relating categorical semantics, which exemplifies the first strand, to finite model theory, which exemplifies the second.
We also note that Boaz Trakhtenbrot was a pioneer of both these approaches, and had a unified vision of the field, which is a continuing source of inspiration.
Abstract: A function on an algebra is congruence preserving if, for any congruence, it maps pairs of congruent elements onto pairs of congruent elements. An algebra is said to be affine complete if every congruence preserving function is a polynomial function. We show that the algebra of (possibly empty) binary trees whose leaves are labeled by letters of an alphabet containing at least one letter, and the free monoid on an alphabet containing at least two letters are affine complete.
Abstract: Given a verbal description of a situation, a typical epistemic user cherry-picks a "natural model" (Kripke or Aumann's) and regards it as a formalization of the original description. This approach carries two fundamental deficiencies:
- It covers only complete descriptions, whereas many (intuitively most) epistemic situations are partially described and cannot be adequately specified by a single model.
- The traditional epistemic reading of Kripke/Aumann models tacitly requires common knowledge of the model which restricts their generality and utility even further.
To cure these defects, we suggest a framework of epistemic theories: hypertheories. Hypertheories and their models offer a well-principled foundation for epistemic reasoning with incomplete information.
Automata are typically used to define languages, but they can also compute functions (in which case they are called transducers). Sometimes, the functional view is more fruitful. In fact, one of the early supporters of the functional view was Trakhtenbrot himself, who writes thus in his 2008 Festschrift: "Counterbalancing this algebra of languages philosophy, I followed a logic of operators view on the subject, suggested by A. Burks and J. Wright.”
In my talk, I will survey some recent developments in the study of transducers. Mostly, I will talk about two classes of transductions, called regular and polyregular. In both cases, the transductions can be characterised in many different ways, using automata, logic, regular expressions, etc.
Abstract: An order-theoretic forest is a countable partial order such that the set of elements larger than any element is linearly ordered. It is an order-theoretic tree if any two elements have an upper-bound. The order type of a branch can be any countable linear order. Such generalized infinite trees yield convenient definitions of the rank-width and of the modular decomposition of a countable graph. We define an algebra with finitely many operations that generates (via infinite terms) these order-theoretic trees and forests, up to isomorphism. We prove that the associated regular objects, i.e., those defined by regular terms, are exactly the ones that are the unique models of monadic second-order sentences.
Abstract: the talk will have two parts:
1. Boaz (Boris) and me – 1972, 1981 and beyond
2. The Georgia Tech (GT) online experiment and online teaching – BC, DC and AC (before Corona, during corona and after corona).
Footnote: you can learn more on the GT experiment from three recent interviews I had in the Wall Street Journal, Forbes and Wiley (audio podcast). You can find them by Googling my name with WSJ, Forbes and Wiley.
Abstract: To an extent, the 1966 congress was a hole in the iron curtain. At least that was how a young Soviet mathematician saw it.
Abstract: Some computational methods of logic programming rely on a theorem on the relationship between stable models and program completion, proved by François Fages thirty years ago. This talk will describe this line of work, including a new result, joint with Jorge Fandinno.
Abstract: Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (submultiset) of the Petri net marking and call two resources equivalent iff replacing one of them with another in any reachable marking does not change the observable Petri net behavior. We study resource similarity and resource bisimilarity -- congruent restrictions of the bisimulation equivalence on Petri nets markings, and prove that, in contrast to the resource similarity, the resource bisimilarity is decidable.
Joint work with Vladimir BashkinAbstract: Let $T(G;X,Y)$ be the Tutte polynomial for graphs. We study the sequence $t_{a,b}(n) = T(K_n;a,b)$ where $a,b$ are integers, and show that for every $m \in \Z$ the sequence $t_{a,b}(n)$ is ultimately periodic modulo $m$ provided $a \neq 1 \mod{m}$ and $b \neq 1 \mod{m}$. This result is related to a conjecture by A. Mani and R. Stones from 2016. It is a consequence of a more general theorem which holds for a wide class of graph polynomials definable in Monadic Second Order Logic, such as the generating matching polynomial, the independence polynomial, the clique polynomial, etc. All our results depend on the Specker-Blatter Theorem from 1981, which studies modular recurrence relations of combinatorial sequences which count the number of labeled graphs.
Joint work with T. KotekAbstract: Tarski structures provide the semantical basis not only for first order logic, but also for specification languages such as VDM, Z, event-B, ASM and TLA. Essentially, a specification employs terms of a signature Σ to characterize a set of Σ–structures. Such a structure then contains data and forms a state. Predicates are used to describe properties of data and states. Dynamic behavior and steps are less pronounced; in most such languages, constant symbols of Σ are used as variables, and assignment statements update those symbols by fresh values.
We suggest a specification to use Σ–structures in a different way: Σ–terms retain their meaning; dynamic behavior and steps are described by updating the predicates. This has a number of advantages: Most important, updates are locally confined; thus, global states can be avoided, and distributed steps and systems are defined more naturally. A notion of modules and their composition allows for designing really big systems, as we will show by examples.
Abstract: The topic of this talk is the transformation of rational expressions into finite automata, a much laboured subject indeed. The starting point is the derived term automaton (aka partial derivative, or Antimirov, automaton) of a rational (or regular) expression, a modification of Brzozowski derivative automaton. By taking a shifted perspective, I shall present a construction of this automaton based on a sole induction on the depth of the expression and that does not make reference to any operation of derivation of the expression.
It is particularly well-suited to the case of weighted rational expressions and it broadens the scope of the method to (weighted) expressions over non free monoids.
Joint work with Sylvain Lombardy (Labri, U. Bordeaux))Abstract: Infinite games (in the form of Gale-Stewart games) are studied where a play is a sequence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space $\omega^\omega$. We consider such games defined by a natural kind of parity automata over the alphabet $\mathbb{N}$, called $\mathbb{N}$-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. It is shown that the classical Büchi-Landweber Theorem (for finite-state games in the Cantor space $2^\omega$) holds again for the present games: A game defined by a parity $\mathbb{N}$-MSO-automaton is determined, the winner can be decided, and a winning strategy of the winner can be constructed that is realizable by an $\mathbb{N}$-MSO-transducer.
Joint work with Benedikt Brutsch
Abstract: Concerns about computational problems requiring brute-force or exhaustive search methods have gained particular attention in recent decades because of the widespread research on the “P = NP? ” question. The Russian word for “bruteforce search ” is “perebor. ” This topic has been an active research area in the Soviet Union for several decades. The main progress over the past 25 years has been to augment exhaustive search with heuristics that are aimied at speeding up the search, for example, via conflict-driven clause learning. In this talk I will describe another approach, whose focus is on succinct representation of the search space.