Pourquoi la linéarisation est-elle une propriété de sécurité et pourquoi les propriétés de sécurité sont-elles des ensembles fermés?

Dans le chapitre 13 «Objets atomiques» du livre «Algorithmes distribués» de Nancy Lynch, la linéarisation (également connue sous le nom d'atomicité) s'est avérée être une propriété de sécurité. C'est-à-dire que sa propriété de trace correspondante est non vide, fermée par préfixe et fermée par limite , comme défini dans la section 8.5.3. De manière informelle, une propriété de sécurité est souvent interprétée comme disant qu'aucune "mauvaise" chose particulière ne se produit jamais.

Sur cette base, mon premier problème est le suivant:

Quels sont les avantages de la linéarisation en tant que propriété de sécurité? Y a-t-il des résultats basés sur ce fait dans la littérature?

Dans l'étude de la classification des propriétés de sécurité et des propriétés de vivacité, il est bien connu que les propriétés de sécurité peuvent être caractérisées comme l'ensemble fermé dans une topologie appropriée. Dans l'article "The Safety-Progress Classification" @ 1993 par Amir Pnueli et al. , une topologie métrique est adoptée. Plus précisément, une propriété est un ensemble de mots (finis ou infinis) sur l'alphabet . La propriété est constituée de tous les mots infinis tels que tous les préfixes de appartiennent à . Par exemple, si , alors $\Phi$ $\Sigma$ $A(\Phi)$ $\sigma$ $\sigma$ $\Phi$ $\Phi = a^{+}b^{\ast}$ . Une propriété infinitaire est définie comme unepropriété de sécuritési pour une propriété finitaire . La métrique entre les mots infinis et est définie comme étant 0 s'ils sont identiques, et $A(\Phi) = a^{\omega} + a^{+}b^{\omega}$ $\Pi$ $\Pi = A(\Phi)$ $\Phi$ $d(\sigma, \sigma')$ $\sigma$ $\sigma'$ sinon, oùest la longueur du préfixe commun le plus long sur lequel ils sont d'accord. Avec cette métrique, la propriété de sécurité peut être caractérisée comme des ensembles fermés topologiquement. $d(\sigma, \sigma') = 2^{-j}$ $j$

Voici mon deuxième problème:

Comment caractériser la linéarisation comme des ensembles fermés topologiquement? En particulier, quel est l'ensemble sous-jacent et quelle est la topologie?

reference-request fl.formal-languages dc.distributed-comp concurrency hengxin
la source

Réponses:

Quels sont les avantages de la linéarisation en tant que propriété de sécurité? Y a-t-il des résultats basés sur ce fait dans la littérature?

Supposons que vous ayez implémenté une machine à mémoire partagée qui ne satisfait que la linéarisation éventuelle , définie comme suit: à chaque exécution de , il existe un certain point dans le temps , de sorte que la linéarisation se vérifie à partir du temps . Notez qu'il n'y a pas de limite supérieure sur . (*) (Il s'agit d'un équivalent artificiel de la linéarité de la définition des propriétés de sécurité.) $M$ $\alpha$ $M$ $T_\alpha$ $T_\alpha$ $T$

$T$

(*) S'il y avait une telle limite supérieure, la linéarisation éventuelle deviendrait alors une propriété de sécurité.

Comment caractériser la linéarisation comme des ensembles fermés topologiquement? En particulier, quel est l'ensemble sous-jacent et quelle est la topologie?

$ASYNC$ $\alpha \in ASYNC$ $\alpha, \beta \in ASYNC$ $\alpha \ne \beta$

d (α, β) := 2^{- N}

$d(\alpha,\beta) := 2^{-N}$

N

$N$

α

$\alpha$

β

$\beta$

α = β

$\alpha = \beta$

d (α, β) = 0

$d(\alpha,\beta) = 0$

$d$ $ASYNC$ $d$ $\forall \alpha,\beta \in ASYNC$ $d(\alpha,\beta)=d(\beta,\alpha)$ $\alpha,\beta,\gamma \in ASYNC$ $d(\alpha,\beta) \le d(\alpha,\gamma) + d(\gamma,\beta)$ $\gamma=\alpha$ $\gamma=\beta$ $d(\alpha,\gamma) \ge d(\gamma,\beta) > 0$ $d(\alpha,\gamma)=2^{-n_1}$ $d(\gamma,\beta)=2^{-n_2}$ $n_1\le n_2$ $\gamma$ $n_2-1$ $\beta$ $n_1-1$ $\alpha$ $\alpha$ $\beta$ $n_1$ $d(\alpha,\beta) = d(\alpha,\gamma)$ $0<d(\alpha,\gamma) < d(\gamma,\beta)$

$d$ $\epsilon$ $B_\varepsilon(\alpha) = \{ \beta \in ASYNC \mid d(\alpha,\beta) < \varepsilon \}$ $\alpha$ $S\subseteq ASYNC$ $\alpha \notin S$ $N$ $\beta$ $N$ $\alpha$ $S$ $\alpha \notin S$ $N\geq 0$ $\beta \in ASYNC$ $d(\alpha,\beta) < {2^{-N}}\text{,}$ $\alpha$ $\beta$ $\ge N$ $\beta \notin S$ $S$

[1] James Munkres. Topologie.

Peter
la source

Merci pour votre réponse. Je dois y réfléchir. Au fait, faites-vous référence au livre "Topology" de James R. Munkres quand vous dites cela The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...?

hengxin

Oui, j'ai ajouté la référence.

Peter

J'ai remarqué que vous avez suggéré une modification du titre de cet article (si j'ai fait une erreur, veuillez ignorer ce commentaire). Tout d'abord, je suis d'accord pour que les deux sous-problèmes soient reflétés dans le titre. Cependant, je ne demande pas " pourquoi la linéarisation est-elle une propriété de sécurité?". Je pose des questions sur les conséquences de ce fait. Je ne sais pas comment modifier le titre de manière appropriée et j'ai ignoré cette modification. Veuillez me faire savoir si vous avez d'autres commentaires ou idées.

hengxin

J'ai réalisé que la caractérisation (preuve) de la linéarisation comme un ensemble fermé n'a fondamentalement rien à voir avec la notion de points de linéarisation. Cela semble être une preuve plus générale qui caractérise toute propriété de sécurité comme un ensemble fermé. Ai-je oublié quelque chose?

hengxin

Oui, toutes les propriétés de sécurité sont des ensembles fermés, tandis que les propriétés de vivacité sont des ensembles denses dans cette topologie. En fait, chaque propriété (c'est-à-dire un ensemble de pistes) peut être exprimée comme une conjonction (c'est-à-dire une intersection) de propriétés de sécurité et de vivacité.

Peter

Concernant votre première question - les propriétés de sécurité sont, en quelque sorte, les propriétés "les plus faciles" à gérer, en ce qui concerne des problèmes tels que la vérification des modèles et la synthèse.

La raison principale en est que dans l'approche automate-théorique des méthodes formelles, le raisonnement sur les propriétés de sécurité se réduit au raisonnement sur les traces finies, ce qui est plus facile que le paramètre standard de trace infinie.

Voir le travail d' Orna Kupferman ici comme point de départ.

Shaull
la source

\ddot{u}

$\ddot{u}$

Je suis à peu près sûr qu'Iv'e a vu des documents traitant de la linéarisation via LTL, au moins dans des cas spécifiques. Si je les trouve, je commenterai.

Shaull

Ce sera génial. Je suis toujours curieux de savoir comment gérer la linéarisation via LTL, en particulier avec la notion de points de linéarisation. À la suite de votre suggestion, je trouve l'article Prouver la linéarisation avec la logique temporelle . Je vais essayer de le lire ces jours-ci. Cependant, je ne suis pas sûr de sa qualité. J'ai hâte de lire vos commentaires.

hengxin

Peut-être que ce sera utile. A en juger par les auteurs, il s'agit d'un article sérieux. Cependant, je ne sais pas à quel point la connexion au LTL est étroite.

Shaull