Showing 1–42 of 42 results for author: Virtema, J

Local consistency and axioms of functional dependence

Authors: Timon Barlag, Miika Hannula, Juha Kontinen, Nina Pardal, Jonni Virtema

Abstract: Local consistency arises in diverse areas, including Bayesian statistics, relational databases, and quantum foundations. Likewise, the notion of functional dependence arises in all of these areas. We adopt a general approach to study logical inference in a setting that enables both global inconsistency and local consistency. Our approach builds upon pairwise consistent families of K-relations, i.e… ▽ More Local consistency arises in diverse areas, including Bayesian statistics, relational databases, and quantum foundations. Likewise, the notion of functional dependence arises in all of these areas. We adopt a general approach to study logical inference in a setting that enables both global inconsistency and local consistency. Our approach builds upon pairwise consistent families of K-relations, i.e, relations with tuples annotated with elements of some positive commutative monoid. The framework covers, e.g., families of probability distributions arising from quantum experiments and their possibilistic counterparts. As a first step, we investigate the entailment problem for functional dependencies (FDs) in this setting. Notably, the transitivity rule for FDs is no longer sound, but can be replaced by two novel axiom schemes. We provide a complete axiomatisation and a PTIME algorithm for the entailment problem of unary FDs. In addition, we explore when contextual families over the Booleans have realisations as contextual families over various monoids. △ Less

Submitted 16 May, 2025; originally announced May 2025.

MSC Class: 68P15; 81P13

Halting Recurrent GNNs and the Graded $μ$-Calculus

Authors: Jeroen Bollen, Jan Van den Bussche, Stijn Vansummeren, Jonni Virtema

Abstract: Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for… ▽ More Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. A recent breakthrough in the study of the expressivity of graded modal mu-calculus in the finite suggests that conversely, restricted to node classifiers definable in monadic second-order logic, recurrent GNNs can express only node classifiers definable in graded modal mu-calculus. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN. △ Less

Submitted 16 May, 2025; originally announced May 2025.

Rewriting Consistent Answers on Annotated Data

Authors: Phokion G. Kolaitis, Nina Pardal, Jonni Virtema, Jef Wijsen

Abstract: We embark on a study of the consistent answers of queries over databases annotated with values from a naturally ordered positive semiring. In this setting, the consistent answers of a query are defined as the minimum of the semiring values that the query takes over all repairs of an inconsistent database. The main focus is on self-join free conjunctive queries and key constraints, which is the mos… ▽ More We embark on a study of the consistent answers of queries over databases annotated with values from a naturally ordered positive semiring. In this setting, the consistent answers of a query are defined as the minimum of the semiring values that the query takes over all repairs of an inconsistent database. The main focus is on self-join free conjunctive queries and key constraints, which is the most extensively studied case of consistent query answering over standard databases. We introduce a variant of first-order logic with a limited form of negation, define suitable semiring semantics, and then establish the main result of the paper: the consistent query answers of a self-join free conjunctive query under key constraints are rewritable in this logic if and only if the attack graph of the query contains no cycles. This result generalizes an analogous result of Koutris and Wijsen for ordinary databases, but also yields new results for a multitude of semirings, including the bag semiring, the tropical semiring, and the fuzzy semiring. Further, for the bag semiring, we show that computing the consistent answers of any self-join free conjunctive query whose attack graph has a strong cycle is not only NP-hard but also it is NP-hard to even approximate the consistent answers with a constant relative approximation guarantee. △ Less

Submitted 2 April, 2025; v1 submitted 16 December, 2024; originally announced December 2024.

Comments: PODS 2025

MSC Class: 68P15; 03B70 ACM Class: H.2

Synchronous Team Semantics for Temporal Logics

Authors: Andreas Krebs, Arne Meier, Jonni Virtema, Martin Zimmermann

Abstract: We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify t… ▽ More We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete. △ Less

Submitted 27 September, 2024; originally announced September 2024.

A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL

Authors: Juha Kontinen, Max Sandström, Jonni Virtema

Abstract: Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperti… ▽ More Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the Until-operator or within the Global-operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the left-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier. △ Less

Submitted 7 June, 2024; originally announced June 2024.

Graph Neural Networks and Arithmetic Circuits

Authors: Timon Barlag, Vivian Holzapfel, Laura Strieker, Jonni Virtema, Heribert Vollmer

Abstract: We characterize the computational power of neural networks that follow the graph neural network (GNN) architecture, not restricted to aggregate-combine GNNs or other particular types. We establish an exact correspondence between the expressivity of GNNs using diverse activation functions and arithmetic circuits over real numbers. In our results the activation function of the network becomes a gate… ▽ More We characterize the computational power of neural networks that follow the graph neural network (GNN) architecture, not restricted to aggregate-combine GNNs or other particular types. We establish an exact correspondence between the expressivity of GNNs using diverse activation functions and arithmetic circuits over real numbers. In our results the activation function of the network becomes a gate type in the circuit. Our result holds for families of constant depth circuits and networks, both uniformly and non-uniformly, for all common activation functions. △ Less

Submitted 21 November, 2024; v1 submitted 27 February, 2024; originally announced February 2024.

ACM Class: F.1.1; F.1.3; I.2.m

Computing Repairs Under Functional and Inclusion Dependencies via Argumentation

Authors: Yasir Mahmood, Jonni Virtema, Timon Barlag, Axel-Cyrille Ngonga Ngomo

Abstract: We discover a connection between finding subset-maximal repairs for sets of functional and inclusion dependencies, and computing extensions within argumentation frameworks (AFs). We study the complexity of the existence of a repair and deciding whether a given tuple belongs to some (or every) repair, by simulating the instances of these problems via AFs. We prove that subset-maximal repairs under… ▽ More We discover a connection between finding subset-maximal repairs for sets of functional and inclusion dependencies, and computing extensions within argumentation frameworks (AFs). We study the complexity of the existence of a repair and deciding whether a given tuple belongs to some (or every) repair, by simulating the instances of these problems via AFs. We prove that subset-maximal repairs under functional dependencies correspond to the naive extensions, which also coincide with the preferred and stable extensions in the resulting AFs. For inclusion dependencies, one needs a pre-processing step on the resulting AFs in order for the extensions to coincide. Allowing both types of dependencies breaks this relationship between extensions, and only preferred semantics captures the repairs. Finally, we establish that the complexities of the above decision problems are NP-complete and Pi_2^P-complete, when both functional and inclusion dependencies are allowed. △ Less

Submitted 4 December, 2023; originally announced December 2023.

Comments: Pre-print

A logic-based framework for database repairs

Authors: Nicolas Fröhlich, Arne Meier, Nina Pardal, Jonni Virtema

Abstract: We introduce a general abstract framework for database repairs, where the repair notions are defined using formal logic. We distinguish between integrity constraints and so-called query constraints. The former are used to model consistency and desirable properties of the data (such as functional dependencies and independencies), while the latter relate two database instances according to their ans… ▽ More We introduce a general abstract framework for database repairs, where the repair notions are defined using formal logic. We distinguish between integrity constraints and so-called query constraints. The former are used to model consistency and desirable properties of the data (such as functional dependencies and independencies), while the latter relate two database instances according to their answers to the query constraints. The framework allows for a distinction between hard and soft queries, allowing the answers to a core set of queries to be preserved, as well as defining a distance between instances based on query answers. We illustrate how different notions of repairs from the literature can be modelled within our unifying framework. The framework generalises both set-based and cardinality based repairs to semiring annotated databases. Furthermore, we initiate a complexity-theoretic analysis of consistent query answering and checking existence of a repair within the framework. △ Less

Submitted 28 March, 2025; v1 submitted 27 June, 2023; originally announced June 2023.

Comments: 9 pages + 2 pages references + 5 pages appendix; updated definitions and results

MSC Class: 68P15; 68T27

Logics with probabilistic team semantics and the Boolean negation

Authors: Miika Hannula, Minna Hirvonen, Juha Kontinen, Yasir Mahmood, Arne Meier, Jonni Virtema

Abstract: We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic FOPT. We give a comprehensive picture of the relative expressivity of these logics together with the most studied logics in probabilistic team se… ▽ More We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic FOPT. We give a comprehensive picture of the relative expressivity of these logics together with the most studied logics in probabilistic team semantics setting, as well as relating their expressivity to a numerical variant of second-order logic. In addition, we introduce novel entropy atoms and show that the extension of first-order logic by entropy atoms subsumes probabilistic independence logic. Finally, we obtain some results on the complexity of model checking, validity, and satisfiability of our logics. △ Less

Submitted 22 May, 2024; v1 submitted 1 June, 2023; originally announced June 2023.

Complexity of Neural Network Training and ETR: Extensions with Effectively Continuous Functions

Authors: Teemu Hankala, Miika Hannula, Juha Kontinen, Jonni Virtema

Abstract: We study the complexity of the problem of training neural networks defined via various activation functions. The training problem is known to be existsR-complete with respect to linear activation functions and the ReLU activation function. We consider the complexity of the problem with respect to the sigmoid activation function and other effectively continuous functions. We show that these trainin… ▽ More We study the complexity of the problem of training neural networks defined via various activation functions. The training problem is known to be existsR-complete with respect to linear activation functions and the ReLU activation function. We consider the complexity of the problem with respect to the sigmoid activation function and other effectively continuous functions. We show that these training problems are polynomial-time many-one bireducible to the existential theory of the reals extended with the corresponding activation functions. In particular, we establish that the sigmoid activation function leads to the existential theory of the reals with the exponential function. It is thus open, and equivalent with the decidability of the existential theory of the reals with the exponential function, whether training neural networks using the sigmoid activation function is algorithmically solvable. In contrast, we obtain that the training problem is undecidable if sinusoidal activation functions are considered. Finally, we obtain general upper bounds for the complexity of the training problem in the form of low levels of the arithmetical hierarchy. △ Less

Submitted 19 May, 2023; originally announced May 2023.

Comments: Revised version of a manuscript sent for review in April 2023

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

Authors: Juha Kontinen, Max Sandström, Jonni Virtema

Abstract: We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We establish fascinating connections between the original semantics based on multisets and the new set-based semantics as well as show one of the first positive complexity theoretic results in th… ▽ More We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We establish fascinating connections between the original semantics based on multisets and the new set-based semantics as well as show one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics. We also relate and apply our results to recently defined logics whose asynchronicity is formalized via time evaluation functions. △ Less

Submitted 21 April, 2023; originally announced April 2023.

Strongly complete axiomatization for a logic with probabilistic interventionist counterfactuals

Authors: Fausto Barbero, Jonni Virtema

Abstract: Causal multiteam semantics is a framework where probabilistic notions and causal inference can be studied in a unified setting. We study a logic (PCO) that features marginal probabilities and interventionist counterfactuals, and allows expressing conditional probability statements, do expressions and other mixtures of causal and probabilistic reasoning. Our main contribution is a strongly complete… ▽ More Causal multiteam semantics is a framework where probabilistic notions and causal inference can be studied in a unified setting. We study a logic (PCO) that features marginal probabilities and interventionist counterfactuals, and allows expressing conditional probability statements, do expressions and other mixtures of causal and probabilistic reasoning. Our main contribution is a strongly complete infinitary axiomatisation for PCO. △ Less

Submitted 6 April, 2023; originally announced April 2023.

Comments: 15 pages

MSC Class: 03B48; 03F99 ACM Class: F.4; G.3

Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

Authors: Fausto Barbero, Jonni Virtema

Abstract: Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be together formalized and studied logically. We consider several logics in the setting of causal multiteam semantics that can express probability comparisons concerning formulae and constants, and encompass interventionist counterfactuals and selective implications that… ▽ More Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be together formalized and studied logically. We consider several logics in the setting of causal multiteam semantics that can express probability comparisons concerning formulae and constants, and encompass interventionist counterfactuals and selective implications that describe consequences of actions and consequences of learning from observations, respectively. We discover complete characterizations of expressivity of the logics in terms of families of linear equations that define the corresponding classes of causal multiteams (together with some closure conditions). The characterizations yield a strict hierarchy of expressive power. Finally, we present some undefinability results based on the characterizations. △ Less

Submitted 21 March, 2023; originally announced March 2023.

Unified Foundations of Team Semantics via Semirings

Authors: Timon Barlag, Miika Hannula, Juha Kontinen, Nina Pardal, Jonni Virtema

Abstract: Semiring semantics for first-order logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula. Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending first-order logic with atoms that describe dependencies between variables. Combining thes… ▽ More Semiring semantics for first-order logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula. Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending first-order logic with atoms that describe dependencies between variables. Combining these two, we propose a unifying approach for analysing the concepts of dependence and independence via a novel semiring team semantics, which subsumes all the previously considered variants for first-order team semantics. In particular, we study the preservation of satisfaction of dependencies and formulae between different semirings. In addition we create links to reasoning tasks such as provenance, counting, and repairs. △ Less

Submitted 14 March, 2023; originally announced March 2023.

Temporal Team Semantics Revisited

Authors: Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, Jonni Virtema

Abstract: Temporal logics have been studied as an approach to the specification of hyperproperties, resulting in the conception of "hyperlogics". With a few recent exceptions, the hyperlogics thus far developed can only relate different traces of a transition system synchronously. However, important information is contained in the relation between different points in their asynchronous interaction. To speci… ▽ More Temporal logics have been studied as an approach to the specification of hyperproperties, resulting in the conception of "hyperlogics". With a few recent exceptions, the hyperlogics thus far developed can only relate different traces of a transition system synchronously. However, important information is contained in the relation between different points in their asynchronous interaction. To specify such "asynchronous hyperproperties", new trace quantifier based hyperlogics have been developed. Yet, hyperlogics with trace quantification cannot express certain requirements that describe the relationships between all executions of a system. Also, these logics induce model checking problems (MC) with prohibitively high complexity costs in the number of quantifier alternations. We study an alternative approach to asynchronous hyperproperties by introducing a novel foundation of temporal team semantics. Team semantics is a logical framework that specifies properties of sets of traces of unbounded size directly, and thus does not have the same limitation as the quantifier based logics mentioned above. We consider temporal team logics which employ quantification over so-called "time evaluation functions" (TEFs) controlling the asynchronous progress of traces instead of quantification over traces. TEFs constitute a novel approach to defining expressive logics for hyperproperties where diverse asynchronous interactions between computations can be formalised and enforced. We show embeddings of synchronous TeamLTL into our new logics. We show that MC for some TeamCTL fragment is highly undecidable. We present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata, and obtain decidability results for the path checking problem and restrictions of MC and SAT. Our translation constitutes the first approach to team semantics based on automata-theoretic methods. △ Less

Submitted 5 February, 2024; v1 submitted 25 October, 2021; originally announced October 2021.

Comments: extended version

Parameterised Complexity of Propositional Inclusion and Independence Logic

Authors: Yasir Mahmood, Jonni Virtema

Abstract: We give a comprehensive account on the parameterized complexity of model checking and satisfiability of propositional inclusion and independence logic. We discover that for most parameterizations the problems are either in FPT or paraNP-complete. We give a comprehensive account on the parameterized complexity of model checking and satisfiability of propositional inclusion and independence logic. We discover that for most parameterizations the problems are either in FPT or paraNP-complete. △ Less

Submitted 13 July, 2023; v1 submitted 31 May, 2021; originally announced May 2021.

Comments: A revised version

Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals

Authors: Miika Hannula, Jonni Virtema

Abstract: Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore r… ▽ More Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additive real arithmetic can only express NP properties. Lastly, we present a sound and complete axiomatization for probabilistic inclusion logic at the atomic level. △ Less

Submitted 21 December, 2021; v1 submitted 23 December, 2020; originally announced December 2020.

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

Authors: Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, Fan Yang

Abstract: We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the… ▽ More We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL-extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable. △ Less

Submitted 23 November, 2021; v1 submitted 7 October, 2020; originally announced October 2020.

ACM Class: F.4.1; D.2.4

On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Authors: Miika Hannula, Juha Kontinen, Martin Lück, Jonni Virtema

Abstract: Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use o… ▽ More Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k=1 and both restrictions of the first sort are in effect. △ Less

Submitted 7 July, 2020; originally announced July 2020.

Descriptive complexity of real computation and probabilistic independence logic

Authors: Miika Hannula, Juha Kontinen, Jan Van den Bussche, Jonni Virtema

Abstract: We introduce a novel variant of BSS machines called Separate Branching BSS machines (S-BSS in short) and develop a Fagin-type logical characterisation for languages decidable in non-deterministic polynomial time by S-BSS machines. We show that NP on S-BSS machines is strictly included in NP on BSS machines and that every NP language on S-BSS machines is a countable union of closed sets in the usua… ▽ More We introduce a novel variant of BSS machines called Separate Branching BSS machines (S-BSS in short) and develop a Fagin-type logical characterisation for languages decidable in non-deterministic polynomial time by S-BSS machines. We show that NP on S-BSS machines is strictly included in NP on BSS machines and that every NP language on S-BSS machines is a countable union of closed sets in the usual topology of R^n. Moreover, we establish that on Boolean inputs NP on S-BSS machines without real constants characterises a natural fragment of the complexity class existsR (a class of problems polynomial time reducible to the true existential theory of the reals) and hence lies between NP and PSPACE. Finally we apply our results to determine the data complexity of probabilistic independence logic. △ Less

Submitted 7 July, 2020; v1 submitted 1 March, 2020; originally announced March 2020.

Journal ref: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2020. Association for Computing Machinery, New York, NY, USA, 550-563

Descriptive Complexity of Deterministic Polylogarithmic Time and Space

Authors: Flavio Ferrarotti, Senén González, José María Turull Torres, Jan Van den Bussche, Jonni Virtema

Abstract: We propose logical characterizations of problems solvable in deterministic polylogarithmic time (PolylogTime) and polylogarithmic space (PolylogSpace). We introduce a novel two-sorted logic that separates the elements of the input domain from the bit positions needed to address these elements. We prove that the inflationary and partial fixed point vartiants of this logic capture PolylogTime and Po… ▽ More We propose logical characterizations of problems solvable in deterministic polylogarithmic time (PolylogTime) and polylogarithmic space (PolylogSpace). We introduce a novel two-sorted logic that separates the elements of the input domain from the bit positions needed to address these elements. We prove that the inflationary and partial fixed point vartiants of this logic capture PolylogTime and PolylogSpace, respectively. In the course of proving that our logic indeed captures PolylogTime on finite ordered structures, we introduce a variant of random-access Turing machines that can access the relations and functions of a structure directly. We investigate whether an explicit predicate for the ordering of the domain is needed in our PolylogTime logic. Finally, we present the open problem of finding an exact characterization of order-invariant queries in PolylogTime. △ Less

Submitted 1 December, 2019; v1 submitted 8 March, 2019; originally announced March 2019.

Comments: Submitted to the Journal of Computer and System Sciences

Facets of Distribution Identities in Probabilistic Team Semantics

Authors: Miika Hannula, Åsa Hirvonen, Juha Kontinen, Vadim Kulikov, Jonni Virtema

Abstract: We study probabilistic team semantics which is a semantical framework allowing the study of logical and probabilistic dependencies simultaneously. We examine and classify the expressive power of logical formalisms arising by different probabilistic atoms such as conditional independence and different variants of marginal distribution equivalences. We also relate the framework to the first-order th… ▽ More We study probabilistic team semantics which is a semantical framework allowing the study of logical and probabilistic dependencies simultaneously. We examine and classify the expressive power of logical formalisms arising by different probabilistic atoms such as conditional independence and different variants of marginal distribution equivalences. We also relate the framework to the first-order theory of the reals and apply our methods to the open question on the complexity of the implication problem of conditional independence. △ Less

Submitted 25 February, 2019; v1 submitted 14 December, 2018; originally announced December 2018.

Expressivity within second-order transitive-closure logic

Authors: Flavio Ferrarotti, Jan Van den Bussche, Jonni Virtema

Abstract: Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is intere… ▽ More Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(E); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(E) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO. △ Less

Submitted 16 April, 2018; originally announced April 2018.

Probabilistic team semantics

Authors: Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, Jonni Virtema

Abstract: Team semantics is a semantical framework for the study of dependence and independence concepts ubiquitous in many areas such as databases and statistics. In recent works team semantics has been generalised to accommodate also multisets and probabilistic dependencies. In this article we study a variant of probabilistic team semantics and relate this framework to a Tarskian two-sorted logic. We also… ▽ More Team semantics is a semantical framework for the study of dependence and independence concepts ubiquitous in many areas such as databases and statistics. In recent works team semantics has been generalised to accommodate also multisets and probabilistic dependencies. In this article we study a variant of probabilistic team semantics and relate this framework to a Tarskian two-sorted logic. We also show that very simple quantifier-free formulae of our logic give rise to NP-hard model checking problems. △ Less

Submitted 6 March, 2018; originally announced March 2018.

Team Semantics for the Specification and Verification of Hyperproperties

Authors: Andreas Krebs, Arne Meier, Jonni Virtema, Martin Zimmermann

Abstract: We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and mod… ▽ More We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. △ Less

Submitted 25 June, 2018; v1 submitted 25 September, 2017; originally announced September 2017.

Comments: Minor corrections

Polyteam Semantics

Authors: Miika Hannula, Juha Kontinen, Jonni Virtema

Abstract: Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define "Polyteam Semantics" in which formulae are evaluated over a family of teams. We… ▽ More Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define "Polyteam Semantics" in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatisation for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterise the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (ESO). The analogous result is shown to hold for poly-independence logic and all ESO-definable properties. We also relate poly-inclusion logic to greatest fixed point logic. △ Less

Submitted 26 March, 2020; v1 submitted 7 April, 2017; originally announced April 2017.

Model Checking and Validity in Propositional and Modal Inclusion Logics

Authors: Lauri Hella, Antti Kuusisto, Arne Meier, Jonni Virtema

Abstract: 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 o… ▽ More 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. △ Less

Submitted 24 April, 2017; v1 submitted 22 September, 2016; originally announced September 2016.

On Quantified Propositional Logics and the Exponential Time Hierarchy

Authors: Miika Hannula, Juha Kontinen, Martin Lück, Jonni Virtema

Abstract: We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the expo… ▽ More We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the exponential hierarchy. Second we study propositional team-based logics. We show that DQBF formulae correspond naturally to quantified propositional dependence logic and present a general NEXPTIME upper bound for quantified propositional logic with a large class of generalized dependence atoms. Moreover we show AEXPTIME(poly)-completeness for extensions of propositional team logic with generalized dependence atoms. △ Less

Submitted 13 September, 2016; originally announced September 2016.

Comments: In Proceedings GandALF 2016, arXiv:1609.03648

ACM Class: F.1.3; F.4.1

Journal ref: EPTCS 226, 2016, pp. 198-212

Characterizing Relative Frame Definability in Team Semantics via the Universal Modality

Authors: Katsuhiko Sano, Jonni Virtema

Abstract: Let ML(U^+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We characterize the relative definability of ML(U^+) relative to finite transitive frames in the spirit of the well-known Goldblatt-Thomason theorem. We show that a class F of Kripke frames is definable in ML(U^+) relative to finite transitive frames if and on… ▽ More Let ML(U^+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We characterize the relative definability of ML(U^+) relative to finite transitive frames in the spirit of the well-known Goldblatt-Thomason theorem. We show that a class F of Kripke frames is definable in ML(U^+) relative to finite transitive frames if and only if F is closed under taking generated subframes and bounded morphic images. In addition, we study modal definability in team-based logics. We study (extended) modal dependence logic, (extended) modal inclusion logic, and modal team logic. With respect to global model definability we obtain a trichotomy and with respect to frame definability a dichotomy. As a corollary we obtain relative Goldblatt--Thomason -style theorems for each of the logics listed above. △ Less

Submitted 22 February, 2018; v1 submitted 16 June, 2016; originally announced June 2016.

Comments: Preprint of a WoLLIC 2016 paper. This preprint has been merged with and superseded by a preprint arXiv:1502.07884

Approximation and Dependence via Multiteam Semantics

Authors: Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, Jonni Virtema

Abstract: We define a variant of team semantics called multiteam semantics based on multisets and study the properties of various logics in this framework. In particular, we define natural probabilistic versions of inclusion and independence atoms and certain approximation operators motivated by approximate dependence atoms of Väänänen. We define a variant of team semantics called multiteam semantics based on multisets and study the properties of various logics in this framework. In particular, we define natural probabilistic versions of inclusion and independence atoms and certain approximation operators motivated by approximate dependence atoms of Väänänen. △ Less

Submitted 21 December, 2015; v1 submitted 30 October, 2015; originally announced October 2015.

Comments: Accepted paper for FoIKS conference, long version

A Team Based Variant of CTL

Authors: Andreas Krebs, Arne Meier, Jonni Virtema

Abstract: We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prov… ▽ More We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeness for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics. △ Less

Submitted 14 July, 2015; v1 submitted 8 May, 2015; originally announced May 2015.

Comments: TIME 2015 conference version, modified title and motiviation

MSC Class: 03B44

Complexity of Propositional Logics in Team Semantics

Authors: Miika Hannula, Juha Kontinen, Jonni Virtema, Heribert Vollmer

Abstract: We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations. We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations. △ Less

Submitted 5 January, 2017; v1 submitted 23 April, 2015; originally announced April 2015.

Comments: 15 pages + 1 page appendix, the main result is generalised and the title updated to reflect this

Characterising Modal Definability of Team-Based Logics via the Universal Modality

Authors: Katsuhiko Sano, Jonni Virtema

Abstract: We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definabili… ▽ More We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definability of ML(A+) in the spirit of the well-known Goldblatt--Thomason theorem. We show that an elementary class F of Kripke frames is definable in ML(A+) if and only if F is closed under taking generated subframes and bounded morphic images, and reflects ultrafilter extensions and finitely generated subframes. In addition we study frame definability relative to finite transitive frames and give an analogous characterisation of ML(A+)-definability relative to finite transitive frames. Finally, we initiate the study of model and frame definability in team-based logics. We study (extended) modal dependence logic, (extended) modal inclusion logic, and modal team logic. We establish strict linear hierarchies with respect to model definability and frame definability, respectively. We show that, with respect to model and frame definability, the before mentioned team-based logics, except modal dependence logic, either coincide with ML(A+) or plain modal logic ML. Thus as a corollary we obtain model theoretic characterisation of model and frame definability for the team-based logics. △ Less

Submitted 21 February, 2018; v1 submitted 27 February, 2015; originally announced February 2015.

Comments: 30 pages. This is a preprint of a journal article to appear in Annals of Pure and Applied Logic. The preprint combines and extends two conference papers arXiv:1502.07884v1 and arXiv:1606.05140. The title of this preprint is changed to reflect this

Axiomatizing Propositional Dependence Logics

Authors: Katsuhiko Sano, Jonni Virtema

Abstract: We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled cal… ▽ More We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi. △ Less

Submitted 19 October, 2014; originally announced October 2014.

Comments: 15 pages

Decidability of predicate logics with team semantics

Authors: Juha Kontinen, Antti Kuusisto, Jonni Virtema

Abstract: 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 t… ▽ More 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-Schönfinkel-Ramsey prefix classes of dependence logic. △ Less

Submitted 18 June, 2016; v1 submitted 19 October, 2014; originally announced October 2014.

Comments: Extended version of a MFCS 2016 article. Changes on the earlier arXiv version: title changed, added the result on validity of two-variable dependence logic, restructuring

Boolean Dependence Logic and Partially-Ordered Connectives

Authors: Johannes Ebbing, Lauri Hella, Peter Lohmann, Jonni Virtema

Abstract: 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 depende… ▽ More 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. △ Less

Submitted 27 June, 2014; originally announced June 2014.

Comments: 41 pages

The Expressive Power of Modal Dependence Logic

Authors: Lauri Hella, Kerkko Luosto, Katsuhiko Sano, Jonni Virtema

Abstract: 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 log… ▽ More 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. △ Less

Submitted 24 June, 2014; originally announced June 2014.

Comments: 19 pages

Complexity of validity for propositional dependence logics

Authors: Jonni Virtema

Abstract: We study the validity problem for propositional dependence logic, modal dependence logic and extended modal dependence logic. We show that the validity problem for propositional dependence logic is NEXPTIME-complete. In addition, we establish that the corresponding problem for modal dependence logic and extended modal dependence logic is NEXPTIME-hard and in NEXPTIME^NP. We study the validity problem for propositional dependence logic, modal dependence logic and extended modal dependence logic. We show that the validity problem for propositional dependence logic is NEXPTIME-complete. In addition, we establish that the corresponding problem for modal dependence logic and extended modal dependence logic is NEXPTIME-hard and in NEXPTIME^NP. △ Less

Submitted 25 August, 2014; v1 submitted 24 June, 2014; originally announced June 2014.

Comments: In Proceedings GandALF 2014, arXiv:1408.5560

Journal ref: EPTCS 161, 2014, pp. 18-31

Undecidable First-Order Theories of Affine Geometries

Authors: Antti Kuusisto, Jeremy Meyers, Jonni Virtema

Abstract: Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable.… ▽ More Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,β) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,β), and show that for each structure (T,β) in C, the FO-theory of the class of expansions of (T,β) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,β) with a restricted unary predicate, for example a finite predicate, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivities of universal MSO and weak universal MSO over expansions of (R^n,β). While the logics are incomparable in general, over expansions of (R^n,β), formulae of weak universal MSO translate into equivalent formulae of universal MSO. △ Less

Submitted 25 December, 2013; v1 submitted 28 October, 2013; originally announced October 2013.

Comments: 23 pages, 4 figures. arXiv admin note: substantial text overlap with arXiv:1208.4930

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 4 (December 30, 2013) lmcs:728

Undecidable First-Order Theories of Affine Geometries

Authors: Antti Kuusisto, Jeremy Meyers, Jonni Virtema

Abstract: Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (β) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidabl… ▽ More Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (β) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of monadic expansions of (R^2,β) is Π^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,β), where T is a subset of R^2, and show that for each structure (T,β) in C, the FO-theory of the class of monadic expansions of (T,β) is undecidable. We then consider classes of expansions of structures (T,β) 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,β). While the logics are incomparable in general, over expansions of (R^n,β), formulae of weak universal MSO translate into equivalent formulae of universal MSO. This is an extended version of a publication in the proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012). △ Less

Submitted 24 August, 2012; originally announced August 2012.

Comments: 21 pages, 3 figures

ACM Class: F.4.1; F.1.3; F.2.2

Weak Models of Distributed Computing, with Connections to Modal Logic

Authors: Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, Jonni Virtema

Abstract: This work presents a classification of weak models of distributed computing. We focus on deterministic distributed algorithms, and study models of computing that are weaker versions of the widely-studied port-numbering model. In the port-numbering model, a node of degree d receives messages through d input ports and sends messages through d output ports, both numbered with 1,2,...,d. In this work,… ▽ More This work presents a classification of weak models of distributed computing. We focus on deterministic distributed algorithms, and study models of computing that are weaker versions of the widely-studied port-numbering model. In the port-numbering model, a node of degree d receives messages through d input ports and sends messages through d output ports, both numbered with 1,2,...,d. In this work, VVc is the class of all graph problems that can be solved in the standard port-numbering model. We study the following subclasses of VVc: VV: Input port i and output port i are not necessarily connected to the same neighbour. MV: Input ports are not numbered; algorithms receive a multiset of messages. SV: Input ports are not numbered; algorithms receive a set of messages. VB: Output ports are not numbered; algorithms send the same message to all output ports. MB: Combination of MV and VB. SB: Combination of SV and VB. Now we have many trivial containment relations, such as SB \subseteq MB \subseteq VB \subseteq VV \subseteq VVc, but it is not obvious if, for example, either of VB \subseteq SV or SV \subseteq VB should hold. Nevertheless, it turns out that we can identify a linear order on these classes. We prove that SB \subsetneq MB = VB \subsetneq SV = MV = VV \subsetneq VVc. The same holds for the constant-time versions of these classes. We also show that the constant-time variants of these classes can be characterised by a corresponding modal logic. Hence the linear order identified in this work has direct implications in the study of the expressibility of modal logic. Conversely, one can use tools from modal logic to study these classes. △ Less

Submitted 21 December, 2013; v1 submitted 9 May, 2012; originally announced May 2012.

Comments: 1 + 40 pages, 9 figures

Complexity of two-variable Dependence Logic and IF-Logic

Authors: Juha Kontinen, Antti Kuusisto, Peter Lohmann, Jonni Virtema

Abstract: 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 undecidable. We also show that D^2 is strictly less expressive than IF^2 and that already in D^2, equicardinality of two… ▽ More 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 undecidable. 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). △ Less

Submitted 15 April, 2011; originally announced April 2011.

Comments: 27 pages, extended version of LICS 2011 paper

ACM Class: F.4.1; F.1.3