W rozdziale 13 „Obiekty atomowe” książki „Algorytmy rozproszone” Nancy Lynch udowodniono, że linearyzowalność (znana również jako atomowość) jest właściwością bezpieczeństwa. To znaczy, że jego odpowiednia właściwość śledzenia jest niepusta, zamknięta z prefiksem i zamknięta z ograniczeniem , jak zdefiniowano w sekcji 8.5.3. Nieformalnie właściwość bezpieczeństwa jest często interpretowana jako powiedzenie, że pewne szczególne „złe” rzeczy nigdy się nie zdarzają.
Na tej podstawie mój pierwszy problem jest następujący:
Jakie są zalety linearyzowalności jako właściwości bezpieczeństwa? Czy są jakieś wyniki oparte na tym fakcie w literaturze?
W badaniu klasyfikacji właściwości bezpieczeństwa i właściwości żywotności wiadomo, że właściwość bezpieczeństwa można scharakteryzować jako zbiór zamknięty w odpowiedniej topologii. W pracy „The Safety-Progress Classification” @ 1993 autorstwa Amira Pnueli i in. , przyjęta jest topologia metryczna. Mówiąc dokładniej, właściwość jest zbiorem (skończonych lub nieskończonych) słów nad alfabetem Σ . Właściwość A ( Φ ) składa się ze wszystkich nieskończonych słów σ, tak że wszystkie prefiksy σ należą do Φ . Na przykład, jeśli Φ = a + b ∗ , to . Właściwość nieskończona Π jest definiowana jakowłaściwość bezpieczeństwa,jeżeli Π = A ( Φ ) dla niektórych właściwości skończonych Φ . Metryka d ( σ , σ ′ ) między nieskończonymi słowami σ i σ ′ jest zdefiniowana jako 0, jeśli są one identyczne, a d ( σ , σ ′ ) = 2 - przeciwnym razie, gdziejjest długością najdłuższego wspólnego przedrostka, na który się zgadzają. Dzięki tej metodzie właściwość bezpieczeństwa można topologicznie scharakteryzować jako zestawy zamknięte.
Oto mój drugi problem:
Jak topologicznie scharakteryzować liniowość jako zestawy zamknięte? W szczególności, jaki jest podstawowy zestaw i jaka jest topologia?
The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...
?Jeśli chodzi o twoje pierwsze pytanie - właściwości bezpieczeństwa są w pewnym sensie „najłatwiejszymi” właściwościami w odniesieniu do problemów takich jak sprawdzanie modelu i synteza.
Podstawowym tego powodem jest to, że w podejściu opartym na teorii automatów do metod formalnych rozumowanie o właściwościach bezpieczeństwa sprowadza się do rozumowania o śladach skończonych, co jest łatwiejsze niż standardowe ustawienie śledzenia nieskończonego.
Zobacz pracę Orny Kupferman tutaj jako punkt wyjścia.
źródło