Author name cluster

Alessio Mansutti

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

AIJ Journal 2026 Journal Article

An optimal pastification algorithm for LTL[X,F] and LTL[X,G]

Alessandro Artale
Luca Geatti
Nicola Gigante
Alessio Mansutti
Andrea Mazzullo
Angelo Montanari

We investigate a fragment of Linear Temporal Logic ( LTL ) comprising the tomorrow ( X ) and eventually ( F ) modalities, and present a singly exponential time algorithm for the pastification problem within this fragment. The pastification problem consists of constructing, for a given LTL formula, an equivalent formula that exclusively employs past temporal operators. While the best known algorithms for this task in full LTL –and in the fragment under consideration–exhibit triply exponential time complexity, our approach achieves optimal complexity for this fragment. The proposed algorithm proceeds in two main stages: (i) the input formula is first translated into a tailored normal form, and then (ii) a pure past formula is synthesized from a tree-like structure derived from the normalized formula. With minor adaptations, the algorithm extends to handle the fragment of LTL featuring the tomorrow and globally modalities. We provide an implementation of the algorithm in the temporal reasoning tool BLACK, and report on an experimental evaluation of its performance. 1

Details DOI

MFCS Conference 2025 Conference Paper

One-Parametric Presburger Arithmetic Has Quantifier Elimination

Alessio Mansutti
Mikhail R. Starchak

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function x ↦ t ⋅ x, where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al. , Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions x ↦ ⌊x/(f(t))⌋, one for each integer polynomial f. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring ℤ[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.

Details

SODA Conference 2024 Conference Paper

Integer Programming with GCD Constraints

Rémy Défossez
Christoph Haase
Alessio Mansutti
Guillermo A. Pérez

We study the non-linear extension of integer programming with greatest common divisor constraints of the form gcd( f, g) ~ d, where f and g are linear polynomials, d is a positive integer, and ~ is a relation among ≤, = ≠, = and ≥. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it exists, has polynomial bit length. To show these results, we identify an expressive fragment of the existential theory of the integers with addition and divisibility that admits solutions of polynomial bit length. It was shown by Lipshitz [Trans. Am. Math. Soc. , 235, pp. 271-283, 1978] that this theory adheres to a local-to-global principle in the following sense: a formula Φ is equi-satisfiable with a formula Ψ in this theory such that Ψ has a solution if and only if Ψ has a solution modulo every prime p. We show that in our fragment, only a polynomial number of primes of polynomial bit length need to be considered, and that the solutions modulo prime numbers can be combined to yield a solution to Φ of polynomial bit length. As a technical by-product, we establish a Chinese-remainder-type theorem for systems of congruences and non-congruences showing that solution sizes do not depend on the magnitude of the moduli of non-congruences.

Details

MFCS Conference 2023 Conference Paper

On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

Christoph Haase
Alessio Mansutti
Amaury Pouly

This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1-31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time.

Details

I&C Journal 2022 Journal Article

An auxiliary logic on trees: On the tower-hardness of logics featuring reachability and submodel reasoning

Alessio Mansutti

We describe a set of simple features that are sufficient in order to make the satisfiability problem of logics interpreted on trees Tower -hard. We exhibit these features through an Auxiliary Logic on Trees (ALT ), a modal logic that essentially deals with reachability of a fixed node inside a forest and features modalities from sabotage modal logic to reason on submodels. After showing that ALT admits a Tower -complete satisfiability problem, we prove that this logic is captured by four other logics that were independently found to be Tower -complete: two-variables separation logic, quantified computation tree logic, modal logic of heaps and modal separation logic. As a by-product of establishing these connections, we discover strict fragments of these logics that are still non-elementary.

Details DOI

MFCS Conference 2022 Conference Paper

Higher-Order Quantified Boolean Satisfiability

Dmitry Chistikov 0001
Christoph Haase
Zahra Hadizadeh
Alessio Mansutti

The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for k-NEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k, d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWER-complete, and that HOSAT(k, d) is complete for the weak k-EXP hierarchy with d alternations for fixed k, d ≥ 1 and d odd. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.

Details

MFCS Conference 2021 Conference Paper

On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes

Christoph Haase
Alessio Mansutti

Given an existential formula Φ of linear arithmetic over p-adic integers together with valuation constraints, we study the p-universality problem which consists of deciding whether Φ is satisfiable for all primes p, and the analogous problem for the closely related existential theory of Büchi arithmetic. Our main result is a coNEXP upper bound for both problems, together with a matching lower bound for existential Büchi arithmetic. On a technical level, our results are obtained from analysing properties of a certain class of p-automata, finite-state automata whose languages encode sets of tuples of natural numbers.

Details

IJCAI Conference 2020 Conference Paper

A Framework for Reasoning about Dynamic Axioms in Description Logics

Bartosz Bednarczyk
Stephane Demri
Alessio Mansutti

Description logics are well-known logical formalisms for knowledge representation. We propose to enrich knowledge bases (KBs) with dynamic axioms that specify how the satisfaction of statements from the KBs evolves when the interpretation is decomposed or recomposed, providing a natural means to predict the evolution of interpretations. Our dynamic axioms borrow logical connectives from separation logics, well-known specification languages to verify programs with dynamic data structures. In the paper, we focus on ALC and EL augmented with dynamic axioms, or to their subclass of positive dynamic axioms. The knowledge base consistency problem in the presence of dynamic axioms is investigated, leading to interesting complexity results, among which the problem for EL with positive dynamic axioms is tractable, whereas EL with dynamic axioms is undecidable.

PDF Details DOI

CSL Conference 2020 Conference Paper

Internal Calculi for Separation Logics

Stéphane Demri
Étienne Lozes
Alessio Mansutti

We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(∗, -*). We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.

Details

JELIA Conference 2019 Conference Paper

Axiomatising Logics with Separating Conjunction and Modalities

Stéphane Demri
Raul Fervari
Alessio Mansutti

Abstract Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics \(\text {MSL} ^{}(*, \langle \ne \rangle )\) and \(\text {MSL} ^{}(*, \Diamond )\), where \(*\) is the separating conjunction, \(\Diamond \) is the standard modal operator and \(\langle \ne \rangle \) is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

Details