arXiv subjects

Lauri Hella

Publications and source records attributed to Lauri Hella.

At least 19 recordsLinked to original sources

arXiv2025

Arity hierarchies for quantifiers closed under partial polymorphisms

We investigate the expressive power of generalized quantifiers closed under partial polymorphism conditions motivated by the study of constraint satisfaction problems. We answer a number of questions arising from the work of Dawar and Hella (CSL 2024) where such quantifiers were introduced. For quantifiers closed under partial near-unanimity polymorphisms, we establish hierarchy results clarifying the interplay between the arity of the polymorphisms and of the quantifiers: The expressive power of $(\ell+1)$-ary quantifiers closed under $\ell$-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity $\ell-1$ and $\ell$. We also establish an infinite hierarchy based on the arity of quantifiers with a fixed arity of partial near-unanimity polymorphisms. Finally, we prove inexpressiveness results for quantifiers with a partial Maltsev polymorphism. The separation results are proved using novel algebraic constructions in the style of Cai-F\"urer-Immerman and the quantifier pebble games of Dawar and Hella (2024).

cs.LO↗

arXiv2023

Regular Representations of Uniform TC^0

The circuit complexity class DLOGTIME-uniform AC^0 is known to be a modest subclass of DLOGTIME-uniform TC^0. The weakness of AC^0 is caused by the fact that AC^0 is not closed under restricting AC^0-computable queries into simple subsequences of the input. Analogously, in descriptive complexity, the logics corresponding to DLOGTIME-uniform AC^0 do not have the relativization property and hence they are not regular. This weakness of DLOGTIME-uniform AC^0 has been elaborated in the line of research on the Crane Beach Conjecture. The conjecture (which was refuted by Barrington, Immerman, Lautemann, Schweikardt and Th{\'e}rien) was that if a language L has a neutral letter, then L can be defined in first-order logic with the collection of all numerical built-in relations, if and only if L can be already defined in FO with order. In the first part of this article we consider logics in the range of AC^0 and TC^0. First we formulate a combinatorial criterion for a cardinality quantifier C_S implying that all languages in DLOGTIME-uniform TC^0 can be defined in FO(C_S). For instance, this criterion is satisfied by C_S if S is the range of some polynomial with positive integer coefficients of degree at least two. In the second part of the paper we first adapt the key properties of abstract logics to accommodate built-in relations. Then we define the regular interior R-int(L) and regular closure R-cl(L), of a logic L, and show that the Crane Beach Conjecture can be interpreted as a statement concerning the regular interior of first-order logic with built-in relations B. We show that if B={+}, or B contains only unary relations besides the order, then R-int(FO_B) collapses to FO with order. In contrast, our results imply that if B contains the order and the range of a polynomial of degree at least two, then R-cl(FO_B) includes all languages in DLOGTIME-uniform TC^0.

cs.LO↗

arXiv2023

Quantifiers closed under partial polymorphisms

We study Lindstrom quantifiers that satisfy certain closure properties which are motivated by the study of polymorphisms in the context of constraint satisfaction problems (CSP). When the algebra of polymorphisms of a finite structure B satisfies certain equations, this gives rise to a natural closure condition on the class of structures that map homomorphically to B. The collection of quantifiers that satisfy closure conditions arising from a fixed set of equations are rather more general than those arising as CSP. For any such conditions P, we define a pebble game that delimits the distinguishing power of the infinitary logic with all quantifiers that are P-closed. We use the pebble game to show that the problem of deciding whether a system of linear equations is solvable in Z2 is not expressible in the infinitary logic with all quantifiers closed under a near-unanimity condition.

cs.LO↗

arXiv2023

Dimension in team semantics

We introduce three measures of complexity for families of sets. Each of the three measures, that we call dimensions, is defined in terms of the minimal number of convex subfamilies that are needed for covering the given family: for upper dimension, the subfamilies are required to contain a unique maximal set, for dual upper dimension a unique minimal set, and for cylindrical dimension both a unique maximal and a unique minimal set. In addition to considering dimensions of particular families of sets we study the behaviour of dimensions under operators that map families of sets to new families of sets. We identify natural sufficient criteria for such operators to preserve the growth class of the dimensions. We apply the theory of our dimensions for proving new hierarchy results for logics with team semantics. First, we show that the standard logical operators preserve the growth classes of the families arising from the semantics of formulas in such logics. Second, we show that the upper dimension of k+1-ary dependence, inclusion, independence, anonymity, and exclusion atoms is in a strictly higher growth class than that of any k-ary atoms, whence the k+1-ary atoms are not definable in terms of any atoms of smaller arity.

math.LO↗

arXiv2023

Descriptive complexity for distributed computing with circuits

We consider distributed algorithms in the realistic scenario where distributed message passing is operated via circuits. We show that within this setting, modal substitution calculus MSC captures the expressive power of circuits. The translations between circuits and MSC-programs are linear in both directions. Furthermore, we show that the colouring algorithm based on Cole-Vishkin can be specified via logarithmic size programs.

cs.LO↗

arXiv2022

Defining long words succinctly in FO and MSO

We consider the length of the longest word definable in FO and MSO via a formula of size n. For both logics we obtain as an upper bound for this number an exponential tower of height linear in n. We prove this by counting types with respect to a fixed quantifier rank. As lower bounds we obtain for both FO and MSO an exponential tower of height in the order of a rational power of n. We show these lower bounds by giving concrete formulas defining word representations of levels of the cumulative hierarchy of sets. In addition, we consider the L\"owenheim-Skolem and Hanf numbers of these logics on words and obtain similar bounds for these as well.

cs.LO↗

arXiv2021

A Completeness Proof for A Regular Predicate Logic with Undefined Truth Value

We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of "is defined" is extended to terms and formulas via a straightforward recursive algorithm. The "is defined" formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the formula, its negation, and the negation of its "is defined" formula is true on the constructed model. Many other ternary logics in the literature can be reduced to ours. Partial functions are ubiquitous in computer science and even in (in)equation solving at schools. Our work was motivated by an attempt to explain, precisely in terms of logic, typical informal methods of reasoning in such applications.

math.LO↗

arXiv2020

Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.

cs.LO↗

arXiv2020

Bounded game-theoretic semantics for modal mu-calculus

math.LO↗

arXiv2019

Formula size games for modal logic and $μ$-calculus

We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke-models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler-Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler-Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\mathrm{FO}$ and (basic) modal logic $\mathrm{ML}$. We also present a version of the game for the modal $μ$-calculus $\mathrm{L}_μ$ and show that $\mathrm{FO}$ is also non-elementarily more succinct than $\mathrm{L}_μ$.

cs.LO↗

arXiv2019

Complexity Thresholds in Inclusion Logic

Logics with team semantics provide alternative means for logical characterization of complexity classes. Both dependence and independence logic are known to capture non-deterministic polynomial time, and the frontiers of tractability in these logics are relatively well understood. Inclusion logic is similar to these team-based logical formalisms with the exception that it corresponds to deterministic polynomial time in ordered models. In this article we examine connections between syntactical fragments of inclusion logic and different complexity classes in terms of two computational problems: maximal subteam membership and the model checking problem for a fixed inclusion logic formula. We show that very simple quantifier-free formulae with one or two inclusion atoms generate instances of these problems that are complete for (non-deterministic) logarithmic space and polynomial time. Furthermore, we present a fragment of inclusion logic that captures non-deterministic logarithmic space in ordered models.

cs.LO↗

arXiv2017

Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics

We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for the strict and another one for the lax semantics. Both problems turn out to be EXPTIME-complete on general structures. Finally, we show how for a specific class of structures NEXPTIME-completeness for these problems under strict semantics can be achieved.

cs.LO↗

arXiv2017

Model Checking and Validity in Propositional and Modal Inclusion Logics

Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the central reasoning problems for modal and propositional dependence, independence, and inclusion logics.

cs.LO↗

arXiv2016

The Succinctness of First-order Logic over Modal Logic via a Formula Size Game

We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke-models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler-Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player (duplicator) does not have a trivial optimal strategy. Thus, unlike the Adler-Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a nonelementary succinctness gap between bisimulation invariant first-order logic FO and (basic) modal logic ML.

math.LO↗

arXiv2015

The expressive power of modal logic with inclusion atoms

Modal inclusion logic is the extension of basic modal logic with inclusion atoms, and its semantics is defined on Kripke models with teams. A team of a Kripke model is just a subset of its domain. In this paper we give a complete characterisation for the expressive power of modal inclusion logic: a class of Kripke models with teams is definable in modal inclusion logic if and only if it is closed under k-bisimulation for some integer k, it is closed under unions, and it has the empty team property. We also prove that the same expressive power can be obtained by adding a single unary nonemptiness operator to modal logic. Furthermore, we establish an exponential lower bound for the size of the translation from modal inclusion logic to modal logic with the nonemptiness operator.

cs.LO↗

arXiv2014

Boolean Dependence Logic and Partially-Ordered Connectives

We introduce a new variant of dependence logic called Boolean dependence logic. In Boolean dependence logic dependence atoms are of the type =(x_1,...,x_n,α), where αis a Boolean variable. Intuitively, with Boolean dependence atoms one can express quantification of relations, while standard dependence atoms express quantification over functions. We compare the expressive power of Boolean dependence logic to dependence logic and first-order logic enriched by partially-ordered connectives. We show that the expressive power of Boolean dependence logic and dependence logic coincide. We define natural syntactic fragments of Boolean dependence logic and show that they coincide with the corresponding fragments of first-order logic enriched by partially-ordered connectives with respect to expressive power. We then show that the fragments form a strict hierarchy.

math.LO↗

arXiv2014

The Expressive Power of Modal Dependence Logic

We study the expressive power of various modal logics with team semantics. We show that exactly the properties of teams that are downward closed and closed under team k-bisimulation, for some finite k, are definable in modal logic extended with intuitionistic disjunction. Furthermore, we show that the expressive power of modal logic with intuitionistic disjunction and extended modal dependence logic coincide. Finally we establish that any translation from extended modal dependence logic into modal logic with intuitionistic disjunction increases the size of some formulas exponentially.

cs.LO↗

arXiv2014

One-dimensional fragment of first-order logic

We introduce a novel decidable fragment of first-order logic. The fragment is one-dimensional in the sense that quantification is limited to applications of blocks of existential (universal) quantifiers such that at most one variable remains free in the quantified formula. The fragment is closed under Boolean operations, but additional restrictions (called uniformity conditions) apply to combinations of atomic formulae with two or more variables. We argue that the notions of one-dimensionality and uniformity together offer a novel perspective on the robust decidability of modal logics. We also establish that minor modifications to the restrictions of the syntax of the one-dimensional fragment lead to undecidable formalisms. Namely, the two-dimensional and non-uniform one-dimensional fragments are shown undecidable. Finally, we prove that with regard to expressivity, the one-dimensional fragment is incomparable with both the guarded negation fragment and two-variable logic with counting. Our proof of the decidability of the one-dimensional fragment is based on a technique involving a direct reduction to the monadic class of first-order logic. The novel technique is itself of an independent mathematical interest.

math.LO↗