Fundamenta Informaticae - Volume 186, issue 1-4

Authors: Avron, Arnon | Dershowitz, Nachum | Rabinovich, Alexander

Article Type: Other

DOI: 10.3233/FI-222115

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. v-viii, 2022

Authors: Abramsky, Samson

Article Type: Research Article

Abstract: In this paper, we give an overview of some recent work on applying tools from category theory in finite model theory, descriptive complexity, constraint satisfaction, and combinatorics. The motivations for this work come from Computer Science, but there may also be something of interest for model theorists and other logicians. The basic setting involves studying the category of relational structures via a resource-indexed family of adjunctions with some process category - which unfolds relational structures into tree-like forms, allowing natural resource parameters to be assigned to these unfoldings. One basic instance of this scheme allows us to recover, in …a purely structural, syntax-free way: the Ehrenfeucht-Fraïssé 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 parameter of tree-depth (Nesetril and Ossona de Mendez). Another instance recovers the k-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 of combinatorial parameters. This whole scheme has been axiomatized in a very general setting, of arboreal categories and arboreal covers. Beyond this basic level, a landscape is beginning to emerge, in which structural features of the resource categories, adjunctions and comonads are reflected in degrees of logical and computational tractability of the corresponding languages. Examples include semantic characterisation and preservation theorems, and Lovász-type results on counting homomorphisms. Show more

DOI: 10.3233/FI-222116

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 1-26, 2022

Authors: Arnold, André | Cégielski, Patrick | Guessarian, Irène

Article Type: Research Article

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.

DOI: 10.3233/FI-222117

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 27-44, 2022

Authors: Artemov, Sergei

Article Type: Research Article

Abstract: Traditionally, Epistemic Logic represents epistemic scenarios using a single model. This, however, covers only complete descriptions that specify truth values of all assertions. Indeed, many—and perhaps most—epistemic descriptions are not complete. Syntactic Epistemic Logic, SEL , suggests viewing an epistemic situation as a set of syntactic conditions rather than as a model. This allows us to naturally capture incomplete descriptions; we discuss a case study in which our proposal is successful. In Epistemic Game Theory, this closes the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game-descriptions and semantic representations of games.

DOI: 10.3233/FI-222118

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 45-62, 2022

Authors: Brütsch, Benedikt | Thomas, Wolfgang

Article Type: Research Article

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 ω^ω. We consider such games defined by a natural kind of parity automata over the alphabet ℕ, called ℕ-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical Büchi-Landweber Theorem (for finite-state games in the Cantor space 2^ω) holds again for the present games: A game defined by a deterministic parity ℕ-MSO-automaton is …determined, the winner can be computed, and an ℕ-MSO-transducer realizing a winning strategy for the winner can be constructed. Show more

Keywords: infinite games, Gale-Stewart games, determinacy, automata over infinite alphabets, transducers, monadic second-order logic, Church’s synthesis problem, pushdown systems

DOI: 10.3233/FI-222119

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 63-88, 2022

Authors: Courcelle, Bruno

Article Type: Research Article

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 (a maximal linearly ordered subset) can be any countable linear order. Such generalized infinite trees yield convenient definitions of the rank-width and the modular decomposition of countable graphs. We define an algebra based on only four operations that generate up to isomorphism and via infinite terms these order-theoretic trees and forests.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. We adapt some tools that we have used in a previous article for proving a similar result for join-trees , i.e. , for order-theoretic trees such that any two nodes have a least upper-bound. Show more

Keywords: Order-theoretic tree, algebra, regular term, monadic second-order logic

DOI: 10.3233/FI-222120

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 89-120, 2022

Authors: Francez, Nissim

Article Type: Research Article

DOI: 10.3233/FI-222121

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 121-132, 2022

Authors: Gurevich, Yuri

Article Type: Research Article

DOI: 10.3233/FI-222122

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 133-141, 2022

Authors: Kaminski, Michael

Article Type: Research Article

Abstract: We present two deductively equivalent calculi for non-deterministic many-valued logics. One is defined by axioms and the other – by rules of inference. The two calculi are obtained from the truth tables of the logic under consideration in a straightforward manner. We prove soundness and strong completeness theorems for both calculi and also prove the cut elimination theorem for the calculi defined by rules of inference.

DOI: 10.3233/FI-222123

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 143-153, 2022

Authors: Kotek, Tomer | Makowsky, Johann A.

Article Type: Research Article

Abstract: Let T (G ; X , Y ) be the Tutte polynomial for graphs. We study the sequence ta,b (n ) = T (Kn ; a , b ) where a , b are integers, and show that for every μ ∈ ℕ the sequence ta,b (n ) is ultimately periodic modulo μ provided a ≠ 1 mod μ and b ≠ 1 mod μ . This result is related to a conjecture by A. Mani and R. Stones from 2016. The theorem is a consequence of a more general theorem …which holds for a wide class of graph polynomials definable in Monadic Second Order Logic. This gives also similar results for the various substitution instances of the bivariate matching polynomial and the trivariate edge elimination polynomial ξ (G ; X , Y , Z ) introduced by I. Averbouch, B. Godlin and the second author in 2008. 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. Show more

DOI: 10.3233/FI-222124

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 155-173, 2022

Authors: Lomazova, Irina A. | Bashkin, Vladimir A. | Jančar, Petr

Article Type: Research Article

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 (a submultiset) of Petri net markings and call two resources equivalent when replacing one of them with another in any marking does not change the observable Petri net behavior. We consider resource similarity and resource bisimilarity, two congruent restrictions of bisimulation equivalence on Petri net markings. Previously it was proved that resource similarity (the largest congruence included in bisimulation equivalence) is undecidable. Here we …present an algorithm for checking resource bisimilarity, thereby proving that this relation (the largest congruence included in bisimulation equivalence that is a bisimulation) is decidable. We also give an example of two resources in a Petri net that are similar but not bisimilar. Show more

Keywords: labeled Petri nets, bisimulation, congruence, decidability, resource bisimilarity

DOI: 10.3233/FI-222125

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 175-194, 2022

Authors: Lombardy, Sylvain | Sakarovitch, Jacques

Article Type: Research Article

Abstract: This paper studies the algorithms for the minimisation of weighted automata. It starts with the definition of morphisms — which generalises and unifies the notion of bisimulation to the whole class of weighted automata — and the unicity of a minimal quotient for every automaton, obtained by partition refinement. From a general scheme for the refinement of partitions, two strategies are considered for the computation of the minimal quotient: the Domain Split and the Predecesor Class Split algorithms. They correspond respectivly to the classical Moore and Hopcroft algorithms for the computation of the minimal quotient of …deterministic Boolean automata. We show that these two strategies yield algorithms with the same quadratic complexity and we study the cases when the second one can be improved in order to achieve a complexity similar to the one of Hopcroft algorithm. Show more

DOI: 10.3233/FI-222126

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 195-218, 2022

Authors: Trakhtenbrot, Mark

Article Type: Research Article

DOI: 10.3233/FI-222127

Citation: Fundamenta Informaticae, vol. 186, no. 1-4, pp. 219-236, 2022