Skip to Main content Skip to Navigation
Book sections

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], Inria Saclay - Ile de France
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.
Document type :
Book sections
Complete list of metadata

https://hal.inria.fr/hal-00772643
Contributor : Stefan Haar <>
Submitted on : Thursday, January 10, 2013 - 8:35:55 PM
Last modification on : Monday, February 15, 2021 - 10:51:36 AM

Identifiers

  • HAL Id : hal-00772643, version 1

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⟩

Share

Metrics

Record views

164