Witam, nie wiem czy zamieściłem temat w odpowiedniej sekcji (jeśli nie to z góry przepraszam). Mam pytanie dotyczące modelu Kripkego. Model ten można przedstawić za pomocą grafu, gdzie wierzchołkami to możliwe światy, a krawędzie określają, czy dany świat jest osiągalny (jeśli prowadzi do niego krawędź w grafie to jest osiągalny). I tutaj moje pytanie, co jeśli mam sytuację typu: A -> B -> C ( to cały graf). Istnieją krawędzie do światów B oraz C natomiast nie ma krawędzi do świata A (z którego pozostałe światy są osiągalne). Czy ma to jakiś wpływ? Tzn. czy zasada: Istnieje krawędź do świata = świat jest osiągalny jest zawsze prawdziwa? Czy musimy dodatkowo sprawdzić świat z którego inny świat jest osiągalny (np. w przykładzie powyżej sprawdzamy świat B: prowadzi do niego krawędź ze świata A, ale dodatkowo sprawdzamy, czy świat A jest osiągalny)?
Zależy co chcesz wiedzieć. Ja się spotkałem z określeniem stany i przejścia, więc jest to typ automatu skończonego. Więc co chcesz wiedzieć? Czy stan jest osiągalny w ogóel, czy jest osiągalny z danego stanu? Pamiętaj, że FSM jest grafem skierowanym, więc nie każdy stan może być osiągalny z dowolnego innego stanu.
Przeczytaj sobie to https://www.cs.utexas.edu/users/browne/uvvf2008/IntroductiontoModelsandAbstractions.pdf. Masz ładnie przedstawione tona przykładzie mikrofalówki.
Ja chce wiedzieć czy jest osiągalny w ogóle, ale jeśli jest sytuacja A -> B -> C, to czy stan A można okreslić jako osiągalny? A co za tym idzie czy stan B jest osiągalny (niby jest do niego krawędź ze stanu A, ale czy stan A jest osiągalny?)? W skrócie jeśli chce tylko wiedzieć czy dany stan jest osiągalny (nie interesuje mnie z którego) to wystarczy, że bede patrzył na wchodzące do niego krawędzie?
No widzisz, w FSM masz zawsze zaznaczony jeden stan, jako stan początkowy. Więc jeśli stan A w tym przypadku jest stanem początkowym, to tak, jest osiągalny, jeśli nie jest stanem początkowym, to jest nieosiągalny. Jeśli chcesz wiedzieć jakie wierzchołki masz osiągalne z danego stanu początkowego to musisz odpalić jakąś szukajkę przez graf, albo BFS albo DFS i tam będziesz miał informację, które wierzchołki idzie osiągnąć.