WYKORZYSTANIE LOGIKI TEMPORALNEJ DO
WERYFIKACJI MODELU
F. Sobczak, M. Bł˛edowski
10.1. Wprowadzenie
Obserwuj ˛ac rozwój naszej cywilizacji bez trudu mo˙zna zauwa˙zy´c jak daleko si˛ega informatyzacja i automatyzacja ró˙znego rodzaju procesów i zjawisk. To dzi˛eki nim zmienia si˛e technologiczne oblicze otaczaj ˛acego nas ´swiata. Jednak ˙zaden post˛ep w tych kierunkach nie byłby mo˙zliwy bez wcze´sniejszego opra-cowania metod formalnych, pozwalaj ˛ace modelowa´c i opisywa´c rzeczywisto´s´c w postaci nadaj ˛acej si˛e do maszynowego przetwarzania.
Modelowanie polega na tworzeniu dokładnego opisu rzeczywisto´sci, z pomi-ni˛eciem czynników niemaj ˛acych wpływu na badane zjawiska w danym kontek-´scie (jak np. własno´sci dynamicznych manipulatora przemysłowego podczas bu-dowy modelu opisuj ˛acego jego czynno´sci w postaci nast˛epuj ˛acych po sobie zda-rze ´n). Na bazie takiego opisu mo˙zna uruchamia´c symulacje, wyznacza´c bie˙z ˛ace sterowania oraz dokonywa´c predykcji przyszłych zachowa ´n ró˙znorodnych sys-temów. Modeluj ˛ac jaki´s system mo˙zna opisa´c zale˙zno´sci panuj ˛ace mi˛edzy jego zmiennymi oraz dopuszczalne zachowania. Opis ten mo˙zna analizowa´c pod ró˙z-nymi k ˛atami, zaczynaj ˛ac od weryfikacji jego poprawno´sci, tj. zgodno´sci modelu systemu z jego specyfikacj ˛a. U podstaw tych analiz le˙z ˛a ró˙zne aparaty matema-tyczne (np. automaty sko ´nczone, sieci Petriego, logika temporalna).
W niniejszym rozdziale zostan ˛a omówione cechy wybranych metod formal-nych. Przedstawiony zostanie równie˙z przykład ich praktycznego wykorzystania do opisu systemu steruj ˛acego ´swiatłami na prostym skrzy˙zowaniu dróg.
10.2. Metody modelowania
Metody modelowania pozwalaj ˛a opisa´c w sposób formalny i jednoznaczny wszystkie istotne cechy badanych obiektów i zjawisk. Opisane dalej automaty sko ´nczone, sieci Petriego i logika temporalna nale˙z ˛a do uznanych i cz˛esto stoso-wanych metod w tym obszarze.
10.2.1. Automaty sko ´nczone
W metodzie automatów sko ´nczonych (ang. finite-state machine, FSM) stan obiektu jest przedstawiany jako unikalna kombinacja warto´sci zmiennych, a jego zachowanie jako tranzycje – przej´scie mi˛edzy stanami. Wej´sciem automatu jest ci ˛ag elementów nale˙z ˛acych do pewnego akceptowanego alfabetu. Maszyna za-czyna działanie w okre´slonym stanie pocz ˛atkowym i interpretuje symbole wej-´sciowe korzystaj ˛ac przy tym z funkcji przej´scia wywołuj ˛acych tranzycje (przej´scia do nast˛epnych stanów). Je´sli po przeczytaniu całego ci ˛agu wej´sciowego automat zako ´nczy działanie w stanie oznaczonym jako akceptuj ˛acy (ko ´ncowy), to słowo nale˙zy do j˛ezyka rozpoznawanego przez maszyn˛e. Automaty mo˙zna podzieli´c na dwie kategorie:
• deterministyczne - przeczytanie danego elementu w konkretnym stanie powo-duje przej´scie do okre´slonego stanu nast˛epnego,
• niedeterministyczne - przeczytanie danego symbolu w konkretnym stanie mo˙ze skutkowa´c przej´sciem do ró˙znych stanów nast˛epnych.
Ka˙zdy niedeterministyczny automat mo˙zna sprowadzi´c do deterministycz-nego, akceptuj ˛acego ten sam alfabet, poprzez zastosowaniu procesu determi-nizacji automatu sko ´nczonego. Nale˙zy jednak liczy´c si˛e ze znacznym wzrostem liczby stanów z n do nawet 2nw najbardziej pesymistycznym przypadku.
Struktura Kripkego jest rodzajem niedeterministycznego automatu sko ´ nczo-nego [1]. Reprezentuje j ˛a graf skierowany, którego wierzchołki przedstawiaj ˛a stany osi ˛agalne przez system, a kraw˛edzie tranzycje mi˛edzy stanami (rys. 10.1). Formalnie struktur˛e Kripkego definiuje si˛e jako krotk˛e [2]
M = 〈S, I ,σ, AP,L〉 gdzie:
S – to sko ´nczony zbiór stanów,
I – jest zbiorem stanów pocz ˛atkowych (I ⊆ S),
δ ⊆ S × S – to relacja tranzycji taka, ˙ze ∀s ∈ S ∃s0∈ S takie, ˙ze (s, s0) ∈ R, AP – jest zbiorem zda ´n atomowych,
L : S → 2AP– to funkcja interpretacji.
s0 s1
start
{p} { }pq s2
{q}
Rys. 10.1: Przykładowa struktura Kripkego: S = {s0, s1, s2}, I = {s0}, σ =
{(s0, s1), (s1, s2), (s1, s0), (s2, s2)}, AP = {p, q}, L(s0) = {p}, L(s1) = {p, q}, L(s2) = {q}.
Trójka 〈S, I ,δ〉 nazywana jest cz˛esto przestrzeni ˛a stanów systemu lub grafem osi ˛agalnym systemu. AP oraz L doł ˛aczaj ˛a do stanów informacje zdefiniowane przez u˙zytkownika.
10.2. Metody modelowania Struktura Kripkego reprezentuje wszystkie mo˙zliwe ´scie˙zki przej´s´c pomi˛edzy stanami modelowanego ni ˛a systemu. Startuj ˛ac ze stanu pocz ˛atkowego mo˙zna zbudowa´c drzewo obliczeniowe, w którym kolejne w˛ezły wyprowadzane z w˛e-zła bie˙z ˛acego b˛ed ˛a reprezentowa´c wszystkie stany, dla których istnieje tranzycja (przej´scie). Poniewa˙z w strukturze Kripkego istniej ˛a cykle, budowane drzewo b˛e-dzie niesko ´nczone.
Automat Büchiego jest rozwini˛eciem automatu sko ´nczonego przyjmuj ˛acym niesko ´nczone ci ˛agi wej´sciowe (jestω-automatem) [3]. Sekwencja wej´sciowa jest zaakceptowana tylko i wył ˛acznie je´sli w trakcie działania maszyny, przynajmniej jeden ze stanów akceptuj ˛acych jest odwiedzany niesko ´nczenie cz˛esto. Istniej ˛a dwie wersje tego automatu: deterministyczna i niedeterministyczna (rys. 10.2). Zazwyczaj mówi si˛e o wersji niedeterministycznej, opisanej krotk ˛a
M = 〈Q,Σ,∆, q0, F 〉 gdzie:
Q – sko ´nczony zbiór stanów, Σ – sko´nczony zbiór (alfabet),
∆ : Q × Σ → Q – relacja tranzycji zwracaj ˛aca zbiór stanów, q0– stan pocz ˛atkowy,
F ⊆ Q – zbiór stanów akceptuj ˛acych.
q0 f a,b a {q0} b a {q0,f } a b a
Rys. 10.2: Niedeterministyczny (z lewej) i deterministyczny (z prawej) automat Büchiego.
Sie´c Petriego to formalizm uogólniaj ˛acy teori˛e automatów wykorzystywany do modelowania współbie˙znych zdarze ´n zachodz ˛acych w systemach rzeczywistych. Dan ˛a sie´c mo˙zna reprezentowa´c za pomoc ˛a trójki [4]
M = 〈P,T,F 〉 gdzie:
P – sko ´nczony zbiór miejsc, T – sko ´nczony zbiór tranzycji,
F ⊂ (P × T ) ∪ (T × P) – zbiór ukierunkowanych kraw˛edzi.
Do opisu aktualnego stanu sieci wykorzystuje si˛e dodatkowo tokeny znajdu-j ˛ace si˛e w wierzchołkach grafu. Miejsca poprzedzaj ˛ace tranzycje nazywane s ˛a miejscami wej´sciowymi. Aby tranzycja mogła nast ˛api´c, we wszystkich stanach
a) b) t 2 1 2 t 2 1 2
Rys. 10.3: Dwa kolejne stany sieci Petriego: a) przed tranzycj ˛a, b) po tranzycji.
j ˛a poprzedzaj ˛acych musz ˛a znajdowa´c si˛e tokeny. Ilo´s´c tokenów, jaka jest nie-zb˛edna do odpalenia (przej´scia tokenów do kolejnego stanu) jest zdefiniowana przez wagi kraw˛edziach wej´sciowych. Ponadto wagi kraw˛edzi wyj´sciowych defi-niuj ˛a ile tokenów pojawi si˛e w wierzchołkach do których prowadz ˛a w przypadku odpalenia tranzycji. Przykład działania sieci przedstawiono na rysunku 10.3.
10.2.2. Logika temporalna
Logika temporalna nale˙zy do grupy formalizmów wykorzystywanych do re-prezentacji działania systemów. Z jej pomoc ˛a tworzy si˛e specyfikacje okre´slaj ˛ace sposób działania obiektu i weryfikuje si˛e modele stworzone za pomoc ˛a automa-tów stanów sko ´nczonych. Weryfikacja taka jest mo˙zliwa, poniewa˙z specyfika-cj˛e opisan ˛a za pomoc ˛a formuł logicznych z wykorzystaniem logiki temporalnej mo˙zna przekształci´c na FSM [5, 6]. W takim wypadku stany traktowane s ˛a jako punkty w czasie, a poprawno´s´c przej´s´c mi˛edzy nimi mo˙ze by´c sprawdzana zgod-nie z przyj˛etymi wcze´szgod-niej logicznymi zało˙zeniami.
W procesie weryfikacji konieczne jest uwzgl˛ednienie przepływu czasu. Narz˛e-dzia dostarczone przez logik˛e klasyczn ˛a (z operatorami: ¬,∧,∨,→) nie daj ˛a mo˙z-liwo´sci charakteryzowania takich systemów. W wi˛ekszo´sci przypadków wprowa-dzenie ci ˛agłego czasu nie jest konieczne. Wystarczy dokona´c dyskretyzacji i za-pewni´c, ˙ze zdarzenia b˛ed ˛a nast˛epowały w okre´slonym porz ˛adku. Do takich wła-´snie zastosowa ´n stosuje si˛e logik˛e temporaln ˛a. Bior ˛ac pod uwag˛e reprezentacj˛e czasu logiki temporalne mo˙zna podzieli´c na kilka opisanych ni˙zej kategorii.
Liniowa logika temporalna (ang. linear temporal logic, LTL) zakłada, ˙ze ka˙zdy moment ma tylko jedn ˛a nast˛epuj ˛ac ˛a po nim ´scie˙zk˛e przepływu czasu. Rozszerza klasyczn ˛a logik˛e o dodatkowe operatory czasowe:
2φ - zawsze zachodzi φ,
3φ - w bie˙z ˛acym stanie lub w przyszło´sci zajdzie φ, °φ - w nast˛epnej chwili zajdzie φ,
φU ψ - w przyszło´sci zajdzie ψ, do tego momentu zachodzi φ, φRψ - ψ zachodzi tak długo, a˙z zajdzie φ.
10.3. Weryfikacja modelu