24.10.2002

Ograniczona Weryfikacja Modelowa dla Uniwersalnego Fragmentu TCTL

Ograniczona Weryfikacja Modelowa, bazujaca na metodach SAT, polega na poszukiwaniu kontrprzykladow o dlugosci ograniczonej przez pewne calkowite k > 0 oraz generowanie formuly zdaniowej, ktora jest spelnialna wtedy i tylko wtedy, gdy taki kontrprzyklad istnieje. Celem referatu jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla Automatow Czasowych reprezentowanych przez siec wspolbieznych i wzajemnie komunikujacych sie komponentow oraz wlasnosci wyrazanych w jezyku logiki TACTL (uniwersalnego fragmentu czasowego rozszerzenia CTL).