8.01.2004

Ograniczona weryfikacja modelowa dla własności ACTL* i systemów modelowanych przez Dyskretne Automaty Czasowe

Głównym celem referatu jest wykazanie, że metoda ograniczonej weryfikacji modelowej (OWM) jest rozszerzalna do własności wyrażalnych w ACTL* (uniwersalnym fragmencie logiki CTL*). Język ten zawiera zarówno logikę ACTL jak i logikę LTL.
Rozszerzenie metody OWM do ACTL* polega na przedefiniowaniu funkcji zwracającej wystarczającą liczbę wykonań systemu, w zbiorze których formuła ACTL* jest sprawdzana, a następnie na zdefiniowaniu translacji do SAT będącej kombinacją traslacji dla formuł LTL i ACTL. Zaproponowana translacja dla ACTL* istotnie różni się od tych istniejących dla LTL i ACTL oraz wydaje się, że język ACTL* jest największym zbiorem własności temporalnych, które mogą być weryfikowane za pomocą metody OWM.

Zaproponowany algorytm został zaimplementowany dla elementarnych sieci Petriego oraz dla dyskretnych automatów czasowych, a uzyskane wstępne wyniki eksperymentalne dowodzą jego efektywności. Ponato, zaproponowana translacja i wykonana implementacja jest bazą dla nowego modulu w symbolicznym weryfikatorze VerICS, rozwijanym w IPI PAN przez grupę prof. dr hab. P. Dembińskiego i doc. dr hab. W. Penczka.