Author name cluster

Lauri Hella

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

16 papers

2 author rows

CSL Conference 2026 Conference Paper

Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms

Anuj Dawar
Lauri Hella
Benedikt Pago

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 (𝓁+1)-ary quantifiers closed under 𝓁-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity 𝓁-1 and 𝓁. 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ürer-Immerman and the quantifier pebble games of Dawar and Hella (2024).

Details

CSL Conference 2024 Conference Paper

Quantifiers Closed Under Partial Polymorphisms

Anuj Dawar
Lauri Hella

We study Lindström 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 𝔅 satisfies certain equations, this gives rise to a natural closure condition on the class of structures that map homomorphically to 𝔅. 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 𝒫, we define a pebble game that delimits the distinguishing power of the infinitary logic with all quantifiers that are 𝒫-closed. We use the pebble game to show that the problem of deciding whether a system of linear equations is solvable in ℤ / 2ℤ is not expressible in the infinitary logic with all quantifiers closed under a near-unanimity condition.

Details

MFCS Conference 2023 Conference Paper

Descriptive Complexity for Distributed Computing with Circuits

Veeti Ahvonen
Damian Heiman
Lauri Hella
Antti Kuusisto

We consider distributed algorithms in the realistic scenario where distributed message passing is operated by circuits. We show that within this setting, modal substitution calculus MSC precisely captures the expressive power of circuits. The result is established via constructing translations that are highly efficient in relation to size. We also observe that the coloring algorithm based on Cole-Vishkin can be specified by logarithmic size programs (and thus also logarithmic size circuits) in the bounded-degree scenario.

Details

CSL Conference 2023 Conference Paper

The Expressive Power of CSP-Quantifiers

Lauri Hella

A generalized quantifier Q_𝒦 is called a CSP-quantifier if its defining class 𝒦 consists of all structures that can be homomorphically mapped to a fixed finite template structure. For all positive integers n ≥ 2 and k, we define a pebble game that characterizes equivalence of structures with respect to the logic L^k_{∞ω}(CSP^+_n), where CSP^+_n is the union of the class Q₁ of all unary quantifiers and the class CSP_n of all CSP-quantifiers with template structures that have at most n elements. Using these games we prove that for every n ≥ 2 there exists a CSP-quantifier with template of size n+1 which is not definable in L^ω_{∞ω}(CSP^+_n). The proof of this result is based on a new variation of the well-known Cai-Fürer-Immerman construction.

Details

I&C Journal 2022 Journal Article

Bounded game-theoretic semantics for modal mu-calculus

Lauri Hella
Antti Kuusisto
Raine Rönnholm

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. 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. We also use the GTS to identify new alternative variants of the mu-calculus, including close variants of the logic with PTime model checking; variants with iteration limited to finite ordinals; and other systems where the semantic or syntactic specification of the mu-calculus has been modified in a natural way suggested by the GTS.

Details DOI

I&C Journal 2022 Journal Article

Complexity thresholds in inclusion logic

Miika Hannula
Lauri Hella

Inclusion logic differs from many other logics of dependence and independence in that it can only describe polynomial-time properties. In this article we examine more closely connections between syntactic fragments of inclusion logic and different complexity classes. Our focus is on 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. We also present a safety game for the maximal subteam membership problem and use it to investigate this problem over teams in which one variable is a key. Furthermore, we relate our findings to consistent query answering over inclusion dependencies, and present a fragment of inclusion logic that captures non-deterministic logarithmic space in ordered models.

Details DOI

GandALF Workshop 2020 Workshop Paper

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

Lauri Hella
Antti Kuusisto
Raine Rönnholm

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.

PDF Details DOI

MFCS Conference 2017 Conference Paper

Model Checking and Validity in Propositional and Modal Inclusion Logics

Lauri Hella
Antti Kuusisto
Arne Meier
Jonni Virtema

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 basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.

Details

CSL Conference 2016 Conference Paper

Dependence Logic vs. Constraint Satisfaction

Lauri Hella
Phokion G. Kolaitis

During the past decade, dependence logic has emerged as a formalism suitable for expressing and analyzing notions of dependence and independence that arise in different scientific areas. The sentences of dependence logic have the same expressive power as those of existential second-order logic, hence dependence logic captures NP on the class of all finite structures. In this paper, we identify a natural fragment of universal dependence logic and show that, in a precise sense, it captures constraint satisfaction. This tight connection between dependence logic and constraint satisfaction contributes to the descriptive complexity of constraint satisfaction and elucidates the expressive power of universal dependence logic.

Details

I&C Journal 2016 Journal Article

Existential second-order logic and modal logic with quantified accessibility relations

Lauri Hella
Antti Kuusisto

This article investigates the role of arity of second-order quantifiers in existential second-order logic, also known as Σ 1 1. We identify fragments L of Σ 1 1 where second-order quantification of relations of arity k > 1 is (nontrivially) vacuous in the sense that each formula of L can be translated to a formula of (a fragment of) monadic Σ 1 1. Let polyadic Boolean modal logic with identity ( PBML = ) be the logic obtained by extending standard polyadic multimodal logic with built-in identity modalities and with constructors that allow for the Boolean combination of accessibility relations. Let Σ 1 1 ( PBML = ) be the extension of PBML = with existential prenex quantification of accessibility relations and proposition symbols. The principal result of the article is that Σ 1 1 ( PBML = ) translates into monadic Σ 1 1. As a corollary, we obtain a variety of decidability results for multimodal logic. The translation can also be seen as a step towards establishing whether every property of finite directed graphs expressible in Σ 1 1 ( FO 2 ) is also expressible in monadic Σ 1 1. This question was left open in the 1999 paper of Grädel and Rosen in the 14th Annual IEEE Symposium on Logic in Computer Science.

Details DOI

GandALF Workshop 2015 Workshop Paper

The expressive power of modal logic with inclusion atoms

Lauri Hella
Johanna Stumpf

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.

PDF Details DOI

CSL Conference 2013 Conference Paper

Inclusion Logic and Fixed Point Logic

Pietro Galliani
Lauri Hella

We investigate the properties of Inclusion Logic, that is, First Order Logic with Team Semantics extended with inclusion dependencies. We prove that Inclusion Logic is equivalent to Greatest Fixed Point Logic, and we prove that all union-closed first-order definable properties of relations are definable in it. We also provide an Ehrenfeucht-Fraïssé game for Inclusion Logic, and give an example illustrating its use.

Details

CSL Conference 2006 Conference Paper

Complete Problems for Higher Order Logics

Lauri Hella
Jose Maria Turull Torres

Abstract Let i, j ≥1, and let Σ \(^{i}_{j}\) denote the class of the higher order logic formulas of order i +1 with j –1 alternations of quantifier blocks of variables of order i +1, starting with an existential quantifier block. There is a precise correspondence between the non deterministic exponential time hierarchy and the different fragments of higher order logics Σ \(^{i}_{j}\), namely NEXP \(^{j}_{i}\) = Σ \(^{i+1}_{j}\). In this article we present a complete problem for each level of the non deterministic exponential time hierarchy, with a very weak sort of reductions, namely quantifier-free first order reductions. Moreover, we don’t assume the existence of an order in the input structures in this reduction. From the logical point of view, our main result says that every fragment Σ \(^{i}_{j}\) of higher order logics can be captured with a first order logic Lindström quantifier. Moreover, as our reductions are quantifier-free first order formulas, we get a normal form stating that each Σ \(^{i}_{j}\) sentence is equivalent to a single occurrence of the quantifier and a tuple of quantifier-free first order formulas. Our complete problems are a generalization of the well known problem quantified Boolean formulas with bounded alternation ( QBF j ).

Details

TCS Journal 2006 Journal Article

Computing queries with higher-order logics

Lauri Hella
José María Turull-Torres

In the present article, we study the expressive power of higher-order logics on finite relational structures or databases. First, we give a characterization of the expressive power of the fragments Σ j i and Π j i, for each i ⩾ 1 and each number of alternations of quantifier blocks j. Then, we get as a corollary the expressive power of HO i for each order i ⩾ 2. From our results, as well as from the results of R. Hull and J. Su, it turns out that no higher-order logic can be complete. Even if we consider the union of higher-order logics of all natural orders, i. e. , ⋃ i ⩾ 2 HO i, we still do not get a complete logic. So, we define a logic which we call variable order logic (VO) which permits the use of untyped relation variables, i. e. , variables of variable order, by allowing quantification over orders. We show that this logic is complete, though even non-recursive queries can be expressed in VO. Then we define a fragment of VO and we prove that it expresses exactly the class of r. e. queries. We finally give a characterization of the class of computable queries through a fragment of VO, which is undecidable.

Details DOI

TCS Journal 2003 Journal Article

Approximate pattern matching and transitive closure logics

Kjell Lemström
Lauri Hella

A sartorial query language facilitates the formulation of queries to a (string) database. One step towards an implementation of such a query language can be taken by defining a logical formalism expressing a known solution for the particular problem at hand. The simplicity of the logic is a desired property, because the simpler the logic that the query language is based on, the more efficiently it can be implemented. We introduce a logical formalism for expressing approximate pattern matching. The formalism uses properties of the dynamic programming approach; a minimizing path of a dynamic programming table is expressed by using a formula in an extension of first order logic (FO). We consider the well-known problems of k-mismatches and k-differences. Assuming first that k is given as a part of the input, those problems are expressed by using deterministic transitive closure logic (FO(DTC)) and transitive closure logic (FO(TC)), respectively. We show how to adapt the formalisms to allow individual costs for the editing operations, and consider music information retrieval (MIR) as a case study. We believe that in the general case k-differences is not expressible in FO(DTC). However, we show that proving this is at least as hard as separating LOGSPACE from NLOGSPACE. On the other hand, we show that if k is fixed, the k-differences problem can be expressed by an FO(DTC) formula.

Details DOI

I&C Journal 1996 Journal Article

Logical Hierarchies in PTIME

Lauri Hella

We consider the problem of finding a characterization for polynomial time computable queries on finite structures in terms of logical definability. It is well known that fixpoint logic provides such a characterization in the presence of a built-in linear order, but without linear order even very simple polynomial time queries involving counting are not expressible in fixpoint logic. Our approach to the problem is based on generalized quantifiers. A generalized quantifier isn-ary if it binds any number of formulas, but at mostnvariables in each formula. We prove that, for each natural numbern, there is a query on finite structures which is expressible in fixpoint logic, but not in the extension of first-order logic by any set ofn-ary quantifiers. It follows that the expressive power of fixpoint logic cannot be captured by adding finitely many quantifiers to first-order logic. Furthermore, we prove that, for each natural numbern, there is a polynomial time computable query which is not definable in any extension of fixpoint logic byn-ary quantifiers. In particular, this rules out the possibility of characterizing PTIME in terms of definability in fixpoint logic extended by a finite set of generalized quantifiers.

Details DOI