Checking Presence Reachability Properties on Parameterized Shared-Memory Systems - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2023

Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Abstract

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.
Fichier principal
Vignette du fichier
mfcs_full_version.pdf (1012.12 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Licence : CC BY - Attribution

Dates and versions

hal-04394124 , version 1 (15-01-2024)

Licence

Attribution

Identifiers

Cite

Nicolas Waldburger. Checking Presence Reachability Properties on Parameterized Shared-Memory Systems. MFCS 2023 - Mathematical Foundations of Computer Science, Aug 2023, Bordeaux, France. pp.88:1-88:15, ⟨10.4230/LIPIcs.MFCS.2023.88⟩. ⟨hal-04394124⟩
16 View
11 Download

Altmetric

Share

Gmail Facebook X LinkedIn More