Arnaud Sangnier

MFCS Conference 2025 Conference Paper

Wait-Only Broadcast Protocols Are Easier to Verify

• Lucie Guillou
• Arnaud Sangnier
• Nathalie Sznajder

We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i. e. , it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in ExpSpace and PSpace-hard.

CSL Conference 2024 Conference Paper

QLTL Model-Checking

• François Laroussinie
• Loriane Leclercq
• Arnaud Sangnier

Quantified LTL (QLTL) extends the temporal logic LTL with quantifications over atomic propositions. Several semantics exist to handle these quantifications, depending on the definition of executions over which formulas are interpreted: either infinite sequences of subsets of atomic propositions (aka the "tree semantics") or infinite sequences of control states combined with a labelling function that associates atomic propositions to the control states (aka the "structure semantics"). The main difference being that in the latter different occurrences of a control state should be labelled similarly. The tree semantics has been intensively studied from the complexity and expressivity point of view (especially in the work of Sistla [Sistla, 1983; Sistla et al. , 1987]) for which the satisfiability and model-checking problems are known to be TOWER-complete. For the structure semantics, French has shown that the satisfiability problem is undecidable [French, 2003]. We study here the model-checking problem for QLTL under this semantics and prove that it is EXPSPACE-complete. We also show that the complexity drops down to PSPACE-complete for two specific cases of structures, namely path and flat ones.

GandALF Workshop 2022 Workshop Paper

On the Existential Fragments of Local First-Order Logics with Data

• Benedikt Bollig
• Arnaud Sangnier
• Olivier Stietel

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain which can be compared wrt. equality. As the satisfiability problem for this logic is undecidable in general, in a previous work, we have introduced a family of local fragments that restrict quantification to neighbourhoods of a given reference point. We provide here the precise complexity characterisation of the satisfiability problem for the existential fragments of this local logic depending on the number of data values carried by each element and the radius of the considered neighbourhoods.

CSL Conference 2021 Conference Paper

Reachability in Distributed Memory Automata

• Benedikt Bollig
• Fedor Ryabinin
• Arnaud Sangnier

We introduce Distributed Memory Automata, a model of register automata suitable to capture some features of distributed algorithms designed for shared-memory systems. In this model, each participant owns a local register and a shared register and has the ability to change its local value, to write it in the global memory and to test atomically the number of occurrences of its value in the shared memory, up to some threshold. We show that the control-state reachability problem for Distributed Memory Automata is Pspace-complete for a fixed number of participants and is in Pspace when the number of participants is not fixed a priori.

TCS Journal 2018 Journal Article

Equivalence between model-checking flat counter systems and Presburger arithmetic

• Stéphane Demri
• Amit Kumar Dhar
• Arnaud Sangnier

We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.

TCS Journal 2016 Journal Article

Parameterized verification of time-sensitive models of ad hoc network protocols

• Parosh Aziz Abdulla
• Giorgio Delzanno
• Othmane Rezine
• Arnaud Sangnier
• Riccardo Traverso

We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

GandALF Workshop 2015 Workshop Paper

ATLsc with partial observation

• François Laroussinie
• Nicolas Markey
• Arnaud Sangnier

Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc.

I&C Journal 2015 Journal Article

Taming past LTL and flat counter systems

• Stéphane Demri
• Amit Kumar Dhar
• Arnaud Sangnier

Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that this problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. As far as past-time operators are concerned, their addition to LTL immediately leads to complications and hence an NP upper bound cannot be deduced by translating formulae into LTL and studying the problem only for this latter logic. We also provide other complexity results obtained by restricting further the class of flat counter systems.

Highlights Conference 2013 Conference Abstract

Solving parity games on integer vectors

• Parosh Aziz Abdulla
• Richard Mayr
• Arnaud Sangnier
• Jeremy Sproston

TCS Journal 2010 Journal Article

Model checking memoryful linear-time logics over one-counter automata

• Stéphane Demri
• Ranko Lazić
• Arnaud Sangnier

We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL ↓ ) and for first-order logic with data equality tests (written FO ( ∼, <, + 1 ) ) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control states). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking LTL ↓ and FO ( ∼, <, + 1 ) over deterministic one-counter automata is PSpace-complete with infinite and finite accepting runs. By contrast, we prove that model checking LTL ↓ in which the until operator U is restricted to the eventually F over nondeterministic one-counter automata is Σ 1 1 -complete [resp. Σ 1 0 -complete] in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for FO ( ∼, <, + 1 ) restricted to two variables (written FO 2 ( ∼, <, + 1 ) ). This makes a difference with respect to the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability problems for LTL ↓ and FO 2 ( ∼, <, + 1 ) are decidable. Our results pave the way for model checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.

MFCS Conference 2008 Conference Paper

Reversal-Bounded Counter Machines Revisited

• Alain Finkel
• Arnaud Sangnier

Abstract We extend the class of reversal-bounded counter machines by authorizing a finite number of alternations between increasing and decreasing mode over a given bound. We prove that extended reversal-bounded counter machines also have effective semi-linear reachability sets. We also prove that the property of being reversal-bounded is undecidable in general even when we fix the bound, whereas this problem becomes decidable when considering Vector Addition System with States.