Trakhtenbrot's centenary

In this paper, we give an overview of some recent work on applying tools fromcategory theory in finite model theory, descriptive complexity, constraintsatisfaction, and combinatorics. The motivations for this work come fromComputer Science, but there may also be something of interest for modeltheorists and other logicians. The basic setting involves studying the category of relational structures viaa resource-indexed family of adjunctions with some process category - whichunfolds relational structures into treelike forms, allowing natural resourceparameters to be assigned to these unfoldings. One basic instance of thisscheme allows us to recover, in a purely structural, syntax-free way: theEhrenfeucht-Fraisse~game; the quantifier rank fragments of first-order logic;the equivalences on structures induced by (i) the quantifier rank fragments,(ii) the restriction of this fragment to the existential positive part, and(iii) the extension with counting quantifiers; and the combinatorial parameterof tree-depth (Nesetril and Ossona de Mendez). Another instance recovers thek-pebble game, the finite-variable fragments, the corresponding equivalences,and the combinatorial parameter of treewidth. Other instances cover modal,guarded and hybrid fragments, generalized quantifiers, and a wide range ofcombinatorial parameters. This whole scheme has been axiomatized in a verygeneral setting, of arboreal categories and arboreal covers. Beyond this basic level, a landscape is beginning to […]

A function on an algebra is congruence preserving if, for any congruence, itmaps pairs of congruent elements onto pairs of congruent elements. An algebrais said to be affine complete if every congruence preserving function is apolynomial function. We show that the algebra of (possibly empty) binary treeswhose leaves are labeled by letters of an alphabet containing at least oneletter, and the free monoid on an alphabet containing at least two letters areaffine complete.

Traditionally, Epistemic Logic represents epistemic scenarios using a singlemodel. This, however, covers only complete descriptions that specify truthvalues of all assertions. Indeed, many -- and perhaps most -- epistemicdescriptions are not complete. Syntactic Epistemic Logic, SEL, suggests viewingan epistemic situation as a set of syntactic conditions rather than as a model.This allows us to naturally capture incomplete descriptions; we discuss a casestudy in which our proposal is successful. In Epistemic Game Theory, thiscloses the conceptual and technical gap, identified by R. Aumann, between thesyntactic character of game-descriptions and semantic representations of games.

Infinite games (in the form of Gale-Stewart games) are studied where a playis a sequence of natural numbers chosen by two players in alternation, thewinning condition being a subset of the Baire space $\omega^\omega$. Weconsider such games defined by a natural kind of parity automata over thealphabet $\mathbb{N}$, called $\mathbb{N}$-MSO-automata, where transitions arespecified by monadic second-order formulas over the successor structure of thenatural numbers. We show that the classical Büchi-Landweber Theorem (forfinite-state games in the Cantor space $2^\omega$) holds again for the presentgames: A game defined by a deterministic parity $\mathbb{N}$-MSO-automaton isdetermined, the winner can be computed, and an $\mathbb{N}$-MSO-transducerrealizing a winning strategy for the winner can be constructed.

An order-theoretic forest is a countable partial order such that the set ofelements larger than any element is linearly ordered. It is an order-theoretictree if any two elements have an upper-bound. The order type of a branch can beany countable linear order. Such generalized infinite trees yield convenientdefinitions of the rank-width and the modular decomposition of countablegraphs. We define an algebra based on only four operations that generate up toisomorphism and via infinite terms these order-theoretic trees and forests. Weprove that the associated regular objects, those defined by regular terms, areexactly the ones that are the unique models of monadic second-order sentences.

To an extent, the 1966 congress was a hole in the iron curtain. At least thathow a young Soviet mathematician saw it.

We present two deductively equivalent calculi for non-deterministicmany-valued logics. One is defined by axioms and the other - by rules ofinference. The two calculi are obtained from the truth tables of the logicunder consideration in a straightforward manner. We prove soundness and strongcompleteness theorems for both calculi and also prove the cut eliminationtheorem for the calculi defined by rules of inference.

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 non-negative integers, and show thatfor every $\mu \in \N$ the sequence $t_{a,b}(n)$ is ultimately periodic modulo$\mu$ provided $a \neq 1 \mod{\mu}$ and $b \neq 1 \mod{\mu}$. This result isrelated to a conjecture by A. Mani and R. Stones from 2016. The theorem is aconsequence of a more general theorem which holds for a wide class of graphpolynomials definable in Monadic Second Order Logic and some of its extensions,such as the the independence polynomial, the clique polynomial, etc. We alsoshow similar results for the various substitution instances of the bivariatematching polynomial and the trivariate edge elimination polynomial$\xi(G;X,Y,Z)$ introduced by I. Averbouch, B. Godlin and the second author in2008. All our results depend on the Specker-Blatter Theorem from 1981, whichstudies modular recurrence relations of combinatorial sequences which count thenumber of labeled graphs.

Petri nets are a popular formalism for modeling and analyzing distributedsystems. Tokens in Petri net models can represent the control flow state orresources produced/consumed by transition firings. We define a resource as apart (a submultiset) of Petri net markings and call two resources equivalentwhen replacing one of them with another in any marking does not change theobservable Petri net behavior. We consider resource similarity and resourcebisimilarity, two congruent restrictions of bisimulation equivalence on Petrinet markings. Previously it was proved that resource similarity (the largestcongruence included in bisimulation equivalence) is undecidable. Here wepresent an algorithm for checking resource bisimilarity, thereby proving thatthis relation (the largest congruence included in bisimulation equivalence thatis a bisimulation) is decidable. We also give an example of two resources in aPetri net that are similar but not bisimilar.

This paper studies the algorithms for the minimisation of weighted automata.It starts with the definition of morphisms-which generalises and unifies thenotion of bisimulation to the whole class of weighted automata-and the unicityof a minimal quotient for every automaton, obtained by partition refinement.From a general scheme for the refinement of partitions, two strategies areconsidered for the computation of the minimal quotient: the Domain Split andthe Predecesor Class Split algorithms. They correspond respectivly to theclassical Moore and Hopcroft algorithms for the computation of the minimalquotient of deterministic Boolean automata. We show that these two strategiesyield algorithms with the same quadratic complexity and we study the cases whenthe second one can be improved in order to achieve a complexity similar to theone of Hopcroft algorithm.

This memorial paper tells the story of the beginning of Boris (Boaz)Trakhtenbrot's long and rich life path, full of unusual and sometimes tragicevents. This path led a boy from a Jewish settlement in Eastern Europe to berecognized as one of the founding fathers of theoretical computer science.