arXiv subjects

Jonni Virtema

Publications and source records attributed to Jonni Virtema.

At least 37 records · Page 2Linked to original sources

arXiv2023

Strongly complete axiomatization for a logic with probabilistic interventionist counterfactuals

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.

cs.LO↗

arXiv2023

Unified Foundations of Team Semantics via Semirings

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.

cs.LO↗

arXiv2021

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

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.

cs.LO↗

arXiv2021

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

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.

cs.LO↗

arXiv2020

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

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.

cs.LO↗

arXiv2020

Descriptive complexity of real computation and probabilistic independence logic

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.

cs.LO↗

arXiv2020

Polyteam Semantics

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.

cs.LO↗

arXiv2019

Descriptive Complexity of Deterministic Polylogarithmic Time and Space

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.

cs.LO↗

arXiv2019

Facets of Distribution Identities in Probabilistic Team Semantics

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.

cs.LO↗

arXiv2018

Team Semantics for the Specification and Verification of Hyperproperties

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.

cs.LO↗

arXiv2018

Expressivity within second-order transitive-closure logic

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.

cs.LO↗

arXiv2018

Probabilistic team semantics

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.

cs.LO↗

arXiv2018

Characterizing Relative Frame Definability in Team Semantics via the Universal Modality

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.

math.LO↗

arXiv2018

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

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.

math.LO↗

arXiv2017

Model Checking and Validity in Propositional and Modal Inclusion Logics

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

cs.LO↗

arXiv2017

Complexity of Propositional Logics in Team Semantics

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.

cs.LO↗

arXiv2016

On Quantified Propositional Logics and the Exponential Time Hierarchy

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.

cs.LO↗

arXiv2016

Decidability of predicate logics with team semantics

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.

cs.LO↗