-
Verification of Population Protocols with Unordered Data
Authors:
Steffen van Bergerem,
Roland Guttenberg,
Sandra Kiefer,
Corto Mascle,
Nicolas Waldburger,
Chana Weil-Kennedy
Abstract:
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin…
▽ More
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power.
We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in EXPSPACE. We also provide a lower complexity bound, namely coNEXPTIME-hardness.
△ Less
Submitted 1 May, 2024;
originally announced May 2024.
-
The Parameterized Complexity of Learning Monadic Second-Order Logic
Authors:
Steffen van Bergerem,
Martin Grohe,
Nina Runde
Abstract:
Within the model-theoretic framework for supervised learning introduced by Grohe and Turán (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO).
We show that the problem of learning an MSO-definable concept from a training sequence of labeled examples is fixed-parameter tractable on graphs of bounded clique-width, and that it is ha…
▽ More
Within the model-theoretic framework for supervised learning introduced by Grohe and Turán (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO).
We show that the problem of learning an MSO-definable concept from a training sequence of labeled examples is fixed-parameter tractable on graphs of bounded clique-width, and that it is hard for the parameterized complexity class para-NP on general graphs.
It turns out that an important distinction to be made is between 1-dimensional and higher-dimensional concepts, where the instances of a k-dimensional concept are k-tuples of vertices of a graph. The tractability results we obtain for the 1-dimensional case are stronger and more general, and they are much easier to prove. In particular, our learning algorithm in the higher-dimensional case is only fixed-parameter tractable in the size of the graph, but not in the size of the training sequence, and we give a hardness result showing that this is optimal. By comparison, in the 1-dimensional case, we obtain an algorithm that is fixed-parameter tractable in both.
△ Less
Submitted 12 February, 2024; v1 submitted 19 September, 2023;
originally announced September 2023.
-
Simulating Logspace-Recursion with Logarithmic Quantifier Depth
Authors:
Steffen van Bergerem,
Martin Grohe,
Sandra Kiefer,
Luca Oeljeklaus
Abstract:
The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-o…
▽ More
The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-order logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth. This yields that any pair of graphs separable by the property can be distinguished with the k-dimensional Weisfeiler-Leman algorithm in a logarithmic number of iterations. In particular, it implies that a constant dimension of the algorithm identifies every interval graph and every chordal claw-free graph in logarithmically many iterations, since every such graph admits LREC=-definable canonisation.
△ Less
Submitted 25 April, 2023;
originally announced April 2023.
-
On the Parameterized Complexity of Learning First-Order Logic
Authors:
Steffen van Bergerem,
Martin Grohe,
Martin Ritzert
Abstract:
We analyse the complexity of learning first-order queries in a model-theoretic framework for supervised learning introduced by (Grohe and Turán, TOCS 2004). Previous research on the complexity of learning in this framework focussed on the question of when learning is possible in time sublinear in the background structure.
Here we study the parameterized complexity of the learning problem. We hav…
▽ More
We analyse the complexity of learning first-order queries in a model-theoretic framework for supervised learning introduced by (Grohe and Turán, TOCS 2004). Previous research on the complexity of learning in this framework focussed on the question of when learning is possible in time sublinear in the background structure.
Here we study the parameterized complexity of the learning problem. We have two main results. The first is a hardness result, showing that learning first-order queries is at least as hard as the corresponding model-checking problem, which implies that on general structures it is hard for the parameterized complexity class AW[*]. Our second main contribution is a fixed-parameter tractable agnostic PAC learning algorithm for first-order queries over sparse relational data (more precisely, over nowhere dense background structures).
△ Less
Submitted 28 June, 2021; v1 submitted 24 February, 2021;
originally announced February 2021.
-
Learning Concepts Described by Weight Aggregation Logic
Authors:
Steffen van Bergerem,
Nicole Schweikardt
Abstract:
We consider weighted structures, which extend ordinary relational structures by assigning weights, i.e. elements from a particular group or ring, to tuples present in the structure. We introduce an extension of first-order logic that allows to aggregate weights of tuples, compare such aggregates, and use them to build more complex formulas. We provide locality properties of fragments of this logic…
▽ More
We consider weighted structures, which extend ordinary relational structures by assigning weights, i.e. elements from a particular group or ring, to tuples present in the structure. We introduce an extension of first-order logic that allows to aggregate weights of tuples, compare such aggregates, and use them to build more complex formulas. We provide locality properties of fragments of this logic including Feferman-Vaught decompositions and a Gaifman normal form for a fragment called FOW1, as well as a localisation theorem for a larger fragment called FOWA1. This fragment can express concepts from various machine learning scenarios. Using the locality properties, we show that concepts definable in FOWA1 over a weighted background structure of at most polylogarithmic degree are agnostically PAC-learnable in polylogarithmic time after pseudo-linear time preprocessing.
△ Less
Submitted 22 September, 2020;
originally announced September 2020.
-
Learning Concepts Definable in First-Order Logic with Counting
Authors:
Steffen van Bergerem
Abstract:
We study Boolean classification problems over relational background structures in the logical framework introduced by Grohe and Turán (TOCS 2004). It is known (Grohe and Ritzert, LICS 2017) that classifiers definable in first-order logic over structures of polylogarithmic degree can be learned in sublinear time, where the degree of the structure and the running time are measured in terms of the si…
▽ More
We study Boolean classification problems over relational background structures in the logical framework introduced by Grohe and Turán (TOCS 2004). It is known (Grohe and Ritzert, LICS 2017) that classifiers definable in first-order logic over structures of polylogarithmic degree can be learned in sublinear time, where the degree of the structure and the running time are measured in terms of the size of the structure. We generalise the results to the first-order logic with counting FOCN, which was introduced by Kuske and Schweikardt (LICS 2017) as an expressive logic generalising various other counting logics. Specifically, we prove that classifiers definable in FOCN over classes of structures of polylogarithmic degree can be consistently learned in sublinear time. This can be seen as a first step towards extending the learning framework to include numerical aspects of machine learning. We extend the result to agnostic probably approximately correct (PAC) learning for classes of structures of degree at most $(\log \log n)^c$ for some constant $c$. Moreover, we show that bounding the degree is crucial to obtain sublinear-time learning algorithms. That is, we prove that, for structures of unbounded degree, learning is not possible in sublinear time, even for classifiers definable in plain first-order logic.
△ Less
Submitted 23 March, 2024; v1 submitted 9 September, 2019;
originally announced September 2019.