Checking Presence Reachability Properties on Parameterized Shared-Memory Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Licence : CC BY - Paternité

Dates et versions

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

Licence

Paternité

Identifiants

Citer

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 Consultations
11 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More