6 papers
Temporal Hyperproperties for Population Protocols
Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty +1
Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since,…
Invariants for One-Counter Automata with Disequality Tests
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks +1
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.…
Verification of Population Protocols with Unordered Data
Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer +3
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 dec…
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 rea…
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
Lucie Guillou, Corto Mascle, Nicolas Waldburger
We consider the parameterized verification of arbitrarily large networks of agents which communicate by broadcasting and receiving messages. In our model, the broadcast topology is…
Parameterized safety verification of round-based shared-memory systems
Nathalie Bertrand, Nicolas Markey, Ocan Sankur +1
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of th…