Author name cluster

Nicolas Waldburger

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.

5 papers

2 author rows

Highlights Conference 2024 Conference Abstract

Reachability in one-counter automata with tests

Nicolas Waldburger

We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as an open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell. This problem has proven over the years to be very challenging. We present some new results on this topic, and in particular a new complexity upper bound at the third level of the polynomial hierarchy. This is a joint work with Dmitry Chistikov, Jerome Leroux and Henry Sinclair-Banks, to be published at CONCUR'24 under the name "Invariants for One-Counter Automata with Disequality Tests".

Details

MFCS Conference 2023 Conference Paper

Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Nicolas Waldburger

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.

Details

Highlights Conference 2023 Conference Abstract

Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Nicolas Waldburger

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines communicating by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives that subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time. Contributed talk given by Nicolas Waldburger

Details

Highlights Conference 2022 Conference Abstract

Parameterized Verification of Round-Based Shared-Memory Systems

Nicolas Waldburger

We consider parameterized verification problems for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm introduced by Aspnes, we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. Verification algorithms thus needs to manage both sources of infinity. In this setting, we study several verification problems, among which safety (the error state cannot be reached) or inevitability (the error state cannot be avoided). This a joint work with Nathalie Bertrand, Nicolas Markey and Ocan Sankur.

Details

Highlights Conference 2020 Conference Abstract

Path search with weight constraints

Nicolas Waldburger

Path search in weighted directed graphs is a fundamental and widely studied algorithmic problem. While it is typical to consider the problem of optimizing the weight of a path between two given points, in practical applications such paths may be subjected to some weight constraints to model resource bounds or broken links in networks. In this talk we consider path problems subject to: (1) Lower-bound constraints requiring that the accumulated weight along a path is always above a bound. As an example, one might require that the energy level along the path is always nonnegative. (2) Equality constraints that allow some vertices to be used only if the accumulated weight is equal to a guard. For instance, an equality constraint on a target point allows to control the exact amount of energy used. (3) Disequality constraints that forbid access to some vertices if the accumulated weight is equal to a guard. This type of constraints helps modeling broken links or flooded paths. The complexity of a path search problem in weighted graphs depends on the combination of constraints that is allowed. The problem is in NC if only lower-bound constraints are allowed(i. e. , as in the counters of a VASS) [Almagoretall, 2019]. It becomes NP-complete if in addition equality constraints are allowed [Haaseetall, 2009], and PSPACE-complete if arbitrary inequality constraints are allowed. The reachability problem with inequality constraints has indeed been related to timed automata and used to resolve a longstanding open question about reachability in that setting [Fearnleyetall, 2013]. An outstanding open problem is the case of path search with lower-bound, equality and disequality constraints. In this case the problem is known to lie between NP and PSPACE. In this talk we show that the problem remains in NP in the case of a single disequality constraint. We conjecture that the problem is in NP in the case of a fixed number k of disequality tests and are working to generalize the above-mentioned proof. This undergoing work is in collaboration with Mahsa Shirmohammadi.

Details