Dobrze zorganizowany system przejściowy

W informatyce, szczególnie w dziedzinie weryfikacji formalnej , dobrze ustrukturyzowane systemy przejściowe (WSTS) są ogólną klasą nieskończonych systemów stanów, dla których wiele problemów weryfikacyjnych jest rozstrzygalnych dzięki istnieniu pewnego rodzaju porządku między stanami system, który jest zgodny z przejściami systemu. Wyniki rozstrzygalności WSTS można zastosować do sieci Petriego , systemów kanałów stratnych i innych.

Definicja formalna

, że dobre quasi-uporządkowanie $na$ zbiorze jest quasi-uporządkowaniem (tj. preorderem lub zwrotną przechodnią relacją binarną $) takim, że$ nieskończona sekwencja elementów ${\ Displaystyle x_ {0}, x_ {1}, x_ {2}, \ ldots}$ , od ${\ Displaystyle X}$ zawiera rosnącą parę ${\ Displaystyle x_ {i} \ równoważnik x_ {j}}$ z ja $\ Displaystyle i <j}$ . Mówi się $, że$ zbiór jest dobrze quasi-uporządkowany lub wqo .

Dla naszych celów system przejściowy to struktura, gdzie ${\ Displaystyle {\ mathcal {S}} = \ langle S, \ rightarrow, \ cdots \$$}$ jest dowolnym zbiorem (jego elementy nazywane są stanami ) i ${\ displaystyle \ rightarrow \ subseteq S \ razy S}$ (jego elementy nazywane są przejściami ). Ogólnie system przejściowy może mieć dodatkową strukturę, taką jak stany początkowe, etykiety na przejściach, stany akceptujące itp. (oznaczone kropkami), ale nas one tutaj nie dotyczą.

Dobrze zorganizowany $składa$ systemu że

• ${\ Displaystyle \ leq \ subseteq S \ razy S}$ jest dobrze quasi-uporządkowaniem na zbiorze stanów.
• ${\ Displaystyle \ leq}$ jest kompatybilny w górę z ${\ Displaystyle \ do}$ : to znaczy dla wszystkich przejść ${\ Displaystyle s_ {1} \ do s_ {2}}$ (przez to rozumiemy ${\ Displaystyle (s_ {1}, s_ {2}) \ w \ do}$ ) i dla wszystkich ${\ Displaystyle t_ {1}}$ tak, że ${\ styl wyświetlania s_{1}\równoważnik t_{1}}$${\ displaystyle t_ {2}}$ takie , że ${\ displaystyle t_ {1} {\ xrightarrow {*}} t_ {2}}$ (czyli ${\ displaystyle t_ {2}}$${1}$ osiągnąć z $}$ zero lub więcej przejść) i .

Wymóg kompatybilności w górę

Dobrze zorganizowane systemy

Dobrze zorganizowany system to system przejściowy ze zbiorem ${$ złożonym ze skończonego stanów S $displaystyle S = Q \ razy$$}$ \ displaystyle $rozstrzygalne$ , zestaw wartości danych , wyposażony w zamówienie w przedsprzedaży ${\ Displaystyle \ leq \ subseteq D \ razy D}$ , który jest rozszerzony na stany o ${\ Displaystyle (q, d) \ leq (q', d') \ Leftrightarrow q = q '\ klin d \ leq d'} ,$ który ma dobrą strukturę, jak zdefiniowano powyżej ( ${\ displaystyle \ to}$ jest monotoniczny, tj. kompatybilny w górę, w odniesieniu do $)$ i dodatkowo ma obliczalny zestaw minimów dla zbioru poprzedników dowolnego podzbioru zamkniętego w górę ${\ displaystyle S}$ .

Systemy dobrze ustrukturyzowane adaptują teorię dobrze ustrukturyzowanych systemów przejściowych do modelowania pewnych klas systemów spotykanych w informatyce i stanowią podstawę procedur decyzyjnych do analizy takich systemów, stąd dodatkowe wymagania: sama definicja WSTS nie mówi nic o obliczalność relacji ${\ displaystyle \ leq}$ , ${\ displaystyle \ to}$ .

Zastosowania w informatyce

Dobrze zorganizowane systemy

Pokrywalność można określić dla dowolnego dobrze ustrukturyzowanego systemu, podobnie jak osiągalność danego stanu kontrolnego, za pomocą wstecznego algorytmu Abdulla i in. lub dla określonych podklas dobrze ustrukturyzowanych systemów (podlegających ścisłej monotoniczności, np. w przypadku nieograniczonych sieci Petriego ) przez analizę naprzód opartą na wykresie pokrywalności Karpa-Millera.

Algorytm wsteczny

Algorytm wsteczny pozwala odpowiedzieć na następujące pytanie: mając dobrze ustrukturyzowany system i stan $,$ czy istnieje ścieżka przejścia, która prowadzi od danego stanu początkowego do $displaystyle s_ {0}}$ stan ${\ Displaystyle s' \ geq s}$ (mówi się, że taki stan obejmuje ${\ displaystyle s}$ )?

Intuicyjne wyjaśnienie tego pytania brzmi: jeśli $również$ stan błędu, to każdy zawierający go stan powinien być traktowany jako stan błędu. Jeśli uda się znaleźć dobrze quasi-porządk, który modeluje to „zawieranie” stanów i który również spełnia wymóg monotoniczności w odniesieniu do relacji przejściowej, to można odpowiedzieć na to pytanie.

Zamiast jednego minimalnego stanu błędu $,$ rozważa się zbiór $stanów$ zamknięty w

Algorytm opiera się na faktach, że w dobrze quasi-porządku ${\ Displaystyle (A, \ leq )}$ , każdy zbiór zamknięty w górę ma skończony zbiór minimów i dowolna sekwencja ${\ displaystyle S_ {1} \ subseteq S_ {2} \ subseteq ...}$ zamkniętych w górę podzbiorów ${\ displaystyle A}$ zbiega się po skończonej liczbie kroków (1).

Algorytm musi przechowywać w pamięci zbiór stanów zamknięty w górę $.$ może zrobić, ponieważ zbiór zamknięty w górę można przedstawić jako skończony zbiór minimów Zaczyna się od zamknięcia w górę zbioru stanów błędów i oblicza przy każdej iteracji (przez monotoniczność również zamkniętą w górę) zbiór bezpośrednich poprzedników i dodaje go do zbioru $} styl wyświetlania S_{s}}$$\ displaystyle S_ {e$ . Ta iteracja kończy się po skończonej liczbie kroków, ze względu na właściwość (1) dobrze-quasi-porządków. jeśli ${\ displaystyle s_ {0}} jest w zbiorze ostatecznie uzyskanym, wtedy wyjście to „tak” ($ można osiągnąć stan ${\ displaystyle S_ {e}} ), w przeciwnym razie jest to „nie” (jest$ nie jest możliwe osiągnięcie takiego stanu).