Local safety and local liveness for distributed systems

Volker Diekert 1 Paul Gastin 2
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We introduce local safety and local liveness for distributed systems whose executions are modeled by Mazurkiewicz traces. We characterize local safety by local closure and local liveness by local density. Restricting to first-order definable properties, we prove a decomposition theorem in the spirit of the separation theorem for linear temporal logic. We then characterize local safety and local liveness by means of canonical local temporal logic formulae.
Type de document :
Chapitre d'ouvrage
Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R. Perspectives in Concurrency Theory, Universities Press, pp.86-106, 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00772643
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 20:35:55
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

  • HAL Id : hal-00772643, version 1

Collections

Citation

Volker Diekert, Paul Gastin. Local safety and local liveness for distributed systems. Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R. Perspectives in Concurrency Theory, Universities Press, pp.86-106, 2009. 〈hal-00772643〉

Partager

Métriques

Consultations de la notice

135