-
Specification and Automatic Verification of Computational Reductions
Authors:
Julien Grange,
Fabian Vehlken,
Nils Vortmeier,
Thomas Zeume
Abstract:
We are interested in the following validation problem for computational reductions: for algorithmic problems $P$ and $P^\star$, is a given candidate reduction indeed a reduction from $P$ to $P^\star$? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation pro…
▽ More
We are interested in the following validation problem for computational reductions: for algorithmic problems $P$ and $P^\star$, is a given candidate reduction indeed a reduction from $P$ to $P^\star$? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
Synthesis for prefix first-order logic on data words
Authors:
Julien Grange,
Mathieu Lehaut
Abstract:
We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties…
▽ More
We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.
△ Less
Submitted 22 April, 2024;
originally announced April 2024.
-
First order synthesis for data words revisited
Authors:
Julien Grange,
Mathieu Lehaut
Abstract:
We carry on the study of the synthesis problem on data words for fragments of first order logic, and delineate precisely the border between decidability and undecidability.
We carry on the study of the synthesis problem on data words for fragments of first order logic, and delineate precisely the border between decidability and undecidability.
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
About the Expressive Power and Complexity of Order-Invariance with Two Variables
Authors:
Bartosz Bednarczyk,
Julien Grange
Abstract:
Order-invariant first-order logic is an extension of first-order logic (FO) where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity an…
▽ More
Order-invariant first-order logic is an extension of first-order logic (FO) where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. While we were not able to provide a satisfactory answer to the question, we suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. On the other hand, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO.
△ Less
Submitted 12 February, 2024; v1 submitted 17 April, 2023;
originally announced April 2023.
-
Order-Invariance in the Two-Variable Fragment of First-Order Logic
Authors:
Julien Grange
Abstract:
We study the expressive power of the two-variable fragment of order-invariant first-order logic. This logic departs from first-order logic in two ways: first, formulas are only allowed to quantify over two variables. Second, formulas can use an additional binary relation, which is interpreted in the structures under scrutiny as a linear order, provided that the truth value of a sentence over a fin…
▽ More
We study the expressive power of the two-variable fragment of order-invariant first-order logic. This logic departs from first-order logic in two ways: first, formulas are only allowed to quantify over two variables. Second, formulas can use an additional binary relation, which is interpreted in the structures under scrutiny as a linear order, provided that the truth value of a sentence over a finite structure never depends on which linear order is chosen on its domain. We prove that on classes of structures of bounded degree, any property expressible in this logic is definable in first-order logic. We then show that the situation remains the same when we add counting quantifiers to this logic.
△ Less
Submitted 11 July, 2022;
originally announced July 2022.
-
On the nonexistence of FO-continuous path and tree-decompositions
Authors:
Julien Grange
Abstract:
Bojanczyk and Pilipczuk showed in their celebrated article "Definability equals recognizability for graphs of bounded treewidth" (LICS 2016) that monadic second-order logic can define tree-decompositions in graphs of bounded treewidth. This raises the question whether such decompositions can already be defined in first-order logic (FO).
We start by introducing the notion of tree-decompositions o…
▽ More
Bojanczyk and Pilipczuk showed in their celebrated article "Definability equals recognizability for graphs of bounded treewidth" (LICS 2016) that monadic second-order logic can define tree-decompositions in graphs of bounded treewidth. This raises the question whether such decompositions can already be defined in first-order logic (FO).
We start by introducing the notion of tree-decompositions of bounded span, which restricts the diameter of the subtree consisting of the bags containing a same node of the structure. Having a bounded span is a natural property of tree-decompositions when dealing with FO, since equality of nodes cannot in general be recovered in FO when it doesn't hold. In particular, it encompasses the notion of domino tree-decompositions.
We show that path-decompositions of bounded span are not FO-continuous, in the sense that there exist arbitrarily FO-similar graphs of bounded pathwidth which do not possess FO-similar path-decompositions of bounded span. Then, we show that tree-decompositions of bounded span are not FO-continuous either.
△ Less
Submitted 8 June, 2021;
originally announced June 2021.
-
Successor-Invariant First-Order Logic on Classes of Bounded Degree
Authors:
Julien Grange
Abstract:
We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of an additional successor relation on the structure is allowed, as long as the validity of formulas is independent of the choice of a particular successor on finite structures.
We show that when the degree is bounded, successor-invariant first-order logic is no more…
▽ More
We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of an additional successor relation on the structure is allowed, as long as the validity of formulas is independent of the choice of a particular successor on finite structures.
We show that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.
△ Less
Submitted 11 August, 2021; v1 submitted 24 September, 2020;
originally announced September 2020.
