Author name cluster

Antti Kuusisto

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.

31 papers

2 author rows

AAAI Conference 2026 Conference Paper

Expressive Power of Graph Transformers via Logic

Veeti Ahvonen
Maurice Funk
Damian Heiman
Antti Kuusisto
Carsten Lutz

Transformers are the basis of modern large language models, but relatively little is known about their precise expressive power on graphs. We study the expressive power of graph transformers (GTs) by Dwivedi and Bresson (2020) and GPS-networks by Rampásek et al. (2022), both under soft-attention and average hard-attention. Our study covers two scenarios: the theoretical setting with real numbers and the more practical case with floats. With reals, we show that in restriction to vertex properties definable in first-order logic (FO), GPS-networks have the same expressive power as graded modal logic (GML) with the global modality. With floats, GPS-networks turn out to be equally expressive as GML with the counting global modality. The latter result is absolute, not restricting to properties definable in a background logic. We also obtain similar characterizations for GTs in terms of propositional logic with the global modality (for reals) and the counting global modality (for floats).

PDF Details DOI

CSL Conference 2025 Conference Paper

Description Complexity of Unary Structures in First-Order Logic with Links to Entropy

Reijo Jaakkola
Antti Kuusisto
Miikka Vilander

The description complexity of a model is the length of the shortest formula that defines the model. We study the description complexity of unary structures in first-order logic FO, also drawing links to semantic complexity in the form of entropy. The class of unary structures provides, e. g. , a simple way to represent tabular Boolean data sets as relational structures. We define structures with FO-formulas that are strictly linear in the size of the model as opposed to using the naive quadratic ones, and we use arguments based on formula size games to obtain related lower bounds for description complexity. For a typical structure the upper and lower bounds in fact match up to a sublinear term, leading to a precise asymptotic result on the expected description complexity of a randomly selected structure. We then give bounds on the relationship between Shannon entropy and description complexity. We extend this relationship also to Boltzmann entropy by establishing an asymptotic match between the two entropies. Despite the simplicity of unary structures, our arguments require the use of formula size games, Stirling’s approximation and Chernoff bounds.

Details

JAIR Journal 2025 Journal Article

Explainability via Short Formulas: the Case of Propositional Logic with Implementation

Reijo Jaakkola
Tomi Janhunen
Antti Kuusisto
Masood Feyzbakhsh Rankooh
Miikka Vilander

We conceptualize explainability in terms of logic and formula size, giving a number of related definitions of explainability in a very general setting. Our main interest is the so-called local explanation problem which aims to explain the truth value of an input formula in an input model. The explanation is a formula of minimal size that (1) obtains the same truth value as the input formula on the input model and (2) transmits that truth value to the input formula globally, i.e., on every model. As an important example case, we study propositional logic in this setting and show that the local explainability problem is complete for the second level of the polynomial hierarchy. The hardness result holds already for DNF-formulas. We also give parameterized versions of these problems leading to NP-completeness. The generality of our definitions allows us to lift complexity results also, e.g., to S5 modal logic and ensembles of decision trees. We also provide an implementation in answer set programming and investigate its capacity in relation to explaining answers to the n-queens and dominating set problems. Furthermore, we give an example of explaining the behavior of a black-box classifier.

PDF Details DOI

CSL Conference 2024 Conference Paper

Descriptive Complexity for Neural Networks via Boolean Networks

Veeti Ahvonen
Damian Heiman
Antti Kuusisto

We investigate the descriptive complexity of a class of neural networks with unrestricted topologies and piecewise polynomial activation functions. We consider the general scenario where the running time is unlimited and floating-point numbers are used for simulating reals. We characterize these neural networks with a rule-based logic for Boolean networks. In particular, we show that the sizes of the neural networks and the corresponding Boolean rule formulae are polynomially related. In fact, in the direction from Boolean rules to neural networks, the blow-up is only linear. We also analyze the delays in running times due to the translations. In the translation from neural networks to Boolean rules, the time delay is polylogarithmic in the neural network size and linear in time. In the converse translation, the time delay is linear in both factors. We also obtain translations between the rule-based logic for Boolean networks, the diamond-free fragment of modal substitution calculus and a class of recursive Boolean circuits where the number of input and output gates match.

Details

NeurIPS Conference 2024 Conference Paper

Logical characterizations of recurrent graph neural networks with reals and floats

Veeti Ahvonen
Damian Heiman
Antti Kuusisto
Carsten Lutz

In pioneering work from 2019, Barceló and coauthors identified logics that precisely match the expressive power of constant iteration-depth graph neural networks (GNNs) relative to properties definable in first-order logic. In this article, we give exact logical characterizations of recurrent GNNs in two scenarios: (1) in the setting with floating-point numbers and (2) with reals. For floats, the formalism matching recurrent GNNs is a rule-based modal logic with counting, while for reals we use a suitable infinitary modal logic, also with counting. These results give exact matches between logics and GNNs in the recurrent setting without relativising to a background logic in either case, but using some natural assumptions about floating-point arithmetic. Applying our characterizations, we also prove that, relative to graph properties definable in monadic second-order logic (MSO), our infinitary and rule-based logics are equally expressive. This implies that recurrent GNNs with reals and floats have the same expressive power over MSO-definable properties and shows that, for such properties, also recurrent GNNs with reals are characterized by a (finitary! ) rule-based modal logic. In the general case, in contrast, the expressive power with floats is weaker than with reals. In addition to logic-oriented results, we also characterize recurrent GNNs, with both reals and floats, via distributed automata, drawing links to distributed computing models.

PDF Details DOI

CSL Conference 2023 Conference Paper

Complexity Classifications via Algebraic Logic

Reijo Jaakkola
Antti Kuusisto

Complexity and decidability of logics is an active research area involving a wide range of different logical systems. We introduce an algebraic approach to complexity classifications of computational logics. Our base system GRA, or general relation algebra, is equiexpressive with first-order logic FO. It resembles cylindric algebra but employs a finite signature with only seven different operators, thus also giving a very succinct characterization of the expressive capacities of first-order logic. We provide a comprehensive classification of the decidability and complexity of the systems obtained by limiting the allowed sets of operators of GRA. We also discuss variants and extensions of GRA, and we provide algebraic characterizations of a range of well-known decidable logics.

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

JELIA Conference 2023 Conference Paper

Short Boolean Formulas as Explanations in Practice

Reijo Jaakkola
Tomi Janhunen
Antti Kuusisto
Masood Feyzbakhsh Rankooh
Miikka Vilander

Abstract We investigate explainability via short Boolean formulas in the data model based on unary relations. As an explanation of length k, we take a Boolean formula of length k that minimizes the error with respect to the target attribute to be explained. We first provide novel quantitative bounds for the expected error in this scenario. We then also demonstrate how the setting works in practice by studying three concrete data sets. In each case, we calculate explanation formulas of different lengths using an encoding in Answer Set Programming. The most accurate formulas we obtain achieve errors similar to other methods on the same data sets. However, due to overfitting, these formulas are not necessarily ideal explanations, so we use cross validation to identify a suitable length for explanations. By limiting to shorter formulas, we obtain explanations that avoid overfitting but are still reasonably accurate and also, importantly, human interpretable.

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 2021 Journal Article

Game-theoretic semantics for ATL+ with applications to model checking

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

We develop a game-theoretic semantics ( GTS ) for the fragment AT L + of the alternating-time temporal logic AT L ⁎, thereby extending the recently introduced GTS for ATL. We show that the game-theoretic semantics is equivalent to the standard compositional semantics of AT L + with perfect-recall strategies. Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking AT L + and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS, we provide a new algorithm for model checking AT L + and identify a natural hierarchy of tractable fragments of AT L + that substantially extend ATL.

Details DOI

GandALF Workshop 2021 Workshop Paper

The Optimal Way to Play the Most Difficult Repeated Coordination Games

Antti Kuusisto
Raine Rönnholm

This paper investigates repeated win-lose coordination games (WLC-games). We analyse which protocols are optimal for these games, covering both the worst case and average case scenarios, i, e. , optimizing the guaranteed and expected coordination times. We begin by analysing Choice Matching Games (CM-games) which are a simple yet fundamental type of WLC-games, where the goal of the players is to pick the same choice from a finite set of initially indistinguishable choices. We give a fully complete classification of optimal expected and guaranteed coordination times in two-player CM-games and show that the corresponding optimal protocols are unique in every case - except in the CM-game with four choices, which we analyse separately. Our results on CM-games are essential for proving a more general result on the difficulty of all WLC-games: we provide a complete analysis of least upper bounds for optimal expected coordination times in all two-player WLC-games as a function of game size. We also show that CM-games can be seen as the most difficult games among all two-player WLC-games, as they turn out to have the greatest optimal expected coordination times.

PDF 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

I&C Journal 2020 Journal Article

Emptiness problems for distributed automata

Antti Kuusisto
Fabian Reiter

We investigate the decidability of the emptiness problem for three classes of distributed automata. These devices operate on finite directed graphs, acting as networks of identical finite-state machines that communicate in an infinite sequence of synchronous rounds. The problem is shown to be decidable in LogSpace for a class of forgetful automata, where the nodes see the messages received from their neighbors but cannot remember their own state. When restricted to the appropriate families of graphs, these forgetful automata are equivalent to classical finite word automata, but strictly more expressive than finite tree automata. On the other hand, we also show that the emptiness problem is undecidable in general. This already holds for two heavily restricted classes of distributed automata: those that reject immediately if they receive more than one message per round, and those whose state diagram must be acyclic except for self-loops. Additionally, to demonstrate the flexibility of distributed automata in simulating different models of computation, we provide a characterization of constraint satisfaction problems by identifying a class of automata with exactly the same computational power.

Details DOI

ECAI Conference 2020 Conference Paper

Gradual Guaranteed Coordination in Repeated Win-Lose Coordination Games

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

We investigate repeated win-lose coordination games and analyse when and how rational players can guarantee eventual coordination in such games. Our study involves both the setting with a protocol shared in advance as well as the scenario without an agreed protocol. In both cases, we focus on the case without any communication amongst the players once the particular game to be played has been revealed to them. We identify classes of coordination games in which coordination cannot be guaranteed in a single round, but can eventually be achieved in several rounds by following suitable coordination protocols. In particular, we study coordination using protocols invariant under structural symmetries of games under some natural assumptions, such as: priority hierarchies amongst players, different patience thresholds, use of focal groups, and gradual coordination by contact.

Details

TCS Journal 2019 Journal Article

Alternating-time temporal logic ATL with finitely bounded semantics

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

We study a variant ATL FB of the alternating-time temporal logic ATL with a non-standard, ‘finitely bounded’ semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL FB differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL FB. The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL FB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL FB and prove its soundness and completeness.

Details DOI

TIME Conference 2017 Conference Paper

CTL with Finitely Bounded Semantics

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.

Details

GandALF Workshop 2017 Workshop Paper

Emptiness Problems for Distributed Automata

Antti Kuusisto
Fabian Reiter

PDF Details DOI

AAMAS Conference 2017 Conference Paper

Game-Theoretic Semantics for ATL+ with Applications to Model Checking

Valentin Goranko
Antti Kuusisto
Raine Rö nnholm

We develop a game-theoretic semantics (GTS) for the fragment ATL+ of the Alternating-time Temporal Logic ATL∗, essentially extending a recently introduced GTS for ATL. We show that the new game-theoretic semantics is equivalent to the standard compositional semantics of ATL+ (with perfectrecall strategies). Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking ATL+ and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS we provide a new algorithm for model checking ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.

PDF

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

MFCS Conference 2017 Conference Paper

One-Dimensional Logic over Trees

Emanuel Kieronski
Antti Kuusisto

A one-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. This fragment contains two-variable logic, and it is known that over words both formalisms have the same complexity and expressive power. Here we investigate the one-dimensional fragment over trees. We consider unranked unordered trees accessible by one or both of the descendant and child relations, as well as ordered trees equipped additionally with sibling relations. We show that over unordered trees the satisfiability problem is ExpSpace-complete when only the descendant relation is available and 2ExpTime-complete with both the descendant and child or with only the child relation. Over ordered trees the problem remains 2ExpTime-complete. Regarding expressivity, we show that over ordered trees and over unordered trees accessible by both the descendant and child the one-dimensional fragment is equivalent to the two-variable fragment with counting quantifiers.

Details

EUMAS Conference 2017 Conference Paper

Rational Coordination in Games with Enriched Representations

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

Abstract We consider pure win-lose coordination games where the representation of the game structure has additional features that are commonly known to the players, such as colouring, naming, or ordering of the available choices or of the players. We study how the information provided by such enriched representations affects the solvability of these games by means of principles of rational reasoning in coordination scenarios with no prior communication or conventions.

Details DOI

LORI Conference 2017 Conference Paper

Rational Coordination with no Communication or Conventions

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

Abstract We study pure coordination games where in every outcome, all players have identical payoffs, ‘win’ or ‘lose’. We identify and discuss a range of ‘purely rational principles’ guiding the reasoning of rational players in such games and analyse which classes of coordination games can be solved by such players with no preplay communication or conventions. We observe that it is highly nontrivial to delineate a boundary between purely rational principles and other decision methods, such as conventions, for solving such coordination games.

Details

MFCS Conference 2016 Conference Paper

Decidability of Predicate Logics with Team Semantics

Juha Kontinen
Antti Kuusisto
Jonni Virtema

We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of 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

AAMAS Conference 2016 Conference Paper

Game-Theoretic Semantics for Alternating-Time Temporal Logic

Valentin Goranko
Antti Kuusisto
Raine Rönnholm

We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where gametheoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The novel game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game; we introduce and analyse an unbounded and bounded GTS and prove these to be equivalent to the standard (Tarskistyle) compositional semantics. We also introduce a nonequivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

PDF

CSL Conference 2015 Conference Paper

Uniform One-Dimensional Fragments with One Equivalence Relation

Emanuel Kieronski
Antti Kuusisto

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.

Details

I&C Journal 2014 Journal Article

Complexity of two-variable dependence logic and IF-logic

Juha Kontinen
Antti Kuusisto
Peter Lohmann
Jonni Virtema

We study the two-variable fragments D 2 and IF 2 of dependence logic and independence-friendly logic. We consider the satisfiability and finite satisfiability problems of these logics and show that for D 2, both problems are NEXPTIME-complete, whereas for IF 2, the problems are Π 1 0 and Σ 1 0 -complete, respectively. We also show that D 2 is strictly less expressive than IF 2 and that already in D 2, equicardinality of two unary predicates and infinity can be expressed (the latter in the presence of a constant symbol). This is an extended version of a publication in the proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011).

Details DOI

GandALF Workshop 2014 Workshop Paper

Infinite Networks, Halting and Local Algorithms

Antti Kuusisto

The immediate past has witnessed an increased amount of interest in local algorithms, i. e. , constant time distributed algorithms. In a recent survey of the topic (Suomela, ACM Computing Surveys, 2013), it is argued that local algorithms provide a natural framework that could be used in order to theoretically control infinite networks in finite time. We study a comprehensive collection of distributed computing models and prove that if infinite networks are included in the class of structures investigated, then every universally halting distributed algorithm is in fact a local algorithm. To contrast this result, we show that if only finite networks are allowed, then even very weak distributed computing models can define nonlocal algorithms that halt everywhere. The investigations in this article continue the studies in the intersection of logic and distributed computing initiated in (Hella et al. , PODC 2012) and (Kuusisto, CSL 2013).

PDF Details DOI

GandALF Workshop 2014 Workshop Paper

Some Turing-Complete Extensions of First-Order Logic

Antti Kuusisto

We introduce a natural Turing-complete extension of first-order logic FO. The extension adds two novel features to FO. The first one of these is the capacity to add new points to models and new tuples to relations. The second one is the possibility of recursive looping when a formula is evaluated using a semantic game. We first define a game-theoretic semantics for the logic and then prove that the expressive power of the logic corresponds in a canonical way to the recognition capacity of Turing machines. Finally, we show how to incorporate generalized quantifiers into the logic and argue for a highly natural connection between oracles and generalized quantifiers.

PDF Details DOI

CSL Conference 2013 Conference Paper

Modal Logic and Distributed Message Passing Automata

Antti Kuusisto

In a recent article, Lauri Hella and co-authors identify a canonical connection between modal logic and deterministic distributed constant-time algorithms. The paper reports a variety of highly natural logical characterizations of classes of distributed message passing automata that run in constant time. The article leaves open the question of identifying related logical characterizations when the constant running time limitation is lifted. We obtain such a characterization for a class of finite message passing automata in terms of a recursive bisimulation invariant logic which we call modal substitution calculus (MSC). We also give a logical characterization of the related class A of infinite message passing automata by showing that classes of labelled directed graphs recognizable by automata in A are exactly the classes co-definable by a modal theory. A class C is co-definable by a modal theory if the complement of C is definable by a possibly infinite set of modal formulae. We also briefly discuss expressivity and decidability issues concerning MSC. We establish that MSC contains the Sigma^\mu_1 fragment of the modal \mu-calculus in the finite. We also observe that the single variable fragment MSC^1 of MSC is not contained in MSO, and that the SAT and FINSAT problems of MSC^1 are complete for PSPACE.

Details

CSL Conference 2012 Conference Paper

Undecidable First-Order Theories of Affine Geometries

Antti Kuusisto
Jeremy Meyers
Jonni Virtema

Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2, \beta, \equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2, \beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FO-theory of monadic expansions of (R^n, \beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T, \beta), where T is a subset of R^n, and show that for each structure (T, \beta) in C, the FO-theory of the class of monadic expansions of (T, \beta) is undecidable. We then consider classes of expansions of structures (T, \beta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n, \beta). While the logics are incomparable in general, over expansions of (R^n, \beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. An extended version of this article can be found on the ArXiv (arXiv: 1208. 4930v1).

Details