I. Tematy raczej praktyczne

Eksperymentalna ocena narzędzia CBMC

CBMC to narządzie do weryfikacji programów w C. Oparte jest na metodzie tzw. ograniczonej weryfikacji modelowej (ang. Bounded Model Checking, BMC), która okazała się bardzo skuteczna w znajdowaniu błędów w oprogramowaniu. Podstawową zasadą BMC jest reprezentacja działania programu przez ścieżkę symboliczną określonej głębokości, zapisaną w postaci formuły boolowskiej. Wystąpienie sytuacji błędnej odpowiada spełnialności formuły, co sprawdzane jest przy pomocy SAT-solvera. Celem pracy jest wykonanie szeregu eksperymentów z narzędziem CBMC, w celu określenie jego mocnych i słabych stron.

Modelowanie systemu sygnalizacji świetlnej

Celem pracy jest stworzenie matematycznego modelu systemu sygalizacji świetlnej, przy użyciu automatów czasowych. Efektywność (przepustowość) modelu zależeć będzie od wielu parametrów, takich jak długość oczekiwania na zielone światło, przesunięcie czasowe pomiędzy zsynchronizowanymi skrzyżowaniami, itp. Wyznaczenie wartości optymalnych dla tych parametrów będzie jednym z celów pracy. Praca ma w dużym stopniu charakter eksperymentalny, eksperymenty będą przeprowadzone w narzędziu UPPAAL.

Rozszerzenie narzędzia Concurrency Workbench: wizualizacja gier

Concurrency Workbench (CWB) to narzędzie do modelowania systemów współbieżnych i do weryfikacji ich wlasności zapisanych w rachunku mu. Narzędzie to ma interesujący interfejs: sprawdzanie poprawności formuły odbywa się poprzez rozegranie pewnej gry pomiędzy użytkownikiem a systemem, (ang. model-checking game). Interfejs narzędzia CWB jest tekstowy -- celem pracy jest rozszerzenie CWB o interfejs graficzny.

Eksperymentalna ewaluacja narzędzia CTX-BLAST

CTX-BLAST to narzędzie do porównawczej analizy sekwencji biologicznych (DNA, białka) opracowane w ramach pracy mgr. w bieżącym roku. Rozszerza on BLAST, szeroko używany przez bioinformatyków, o tzw. kontekstowy model kary. Celem pracy ma być eksperymentalne porównanie CTX-BLAST'a z BLAST'em. Oczekuję, że znajdziemy sytuacje, w których kontekstowość daje wyrażną przewagę. Eksperymenty zostaną przeprowadzone w platformie Taverna, będącej ciekawą propozycją jednolitego środowiska do zarządzania eksperymentami bioinformatycznymi.

Zastosowanie hierarchicznej agregacji w stochastycznej weryfikacji modelowej

Biologia systemów to dziedzina bioinformatyki, w której analizuje się modele matematyczne systemów biologicznych (biochemicznych), takich jak komórka lub jej składowe. Ostatnio coraz szersze zainteresowanie w tej dziedzinie znajdują formalne metody weryfikacji, np. weryfikacja modelowa (ang. model-checking). Najczęściej mamy do czynienia z modelami probabilistycznymi, dla znane których techniki są często nieefektywne. Tematem pracy będzie próba implementacji stochastycznej weryfikacji modelowej w oparciu o hierchiczną agregację łańcuchów Markowa.

II. Tematy raczej teoretyczne

Symulacja pomiędzy automatem skończonym a siecią Petriego

Temat dotyczy zagadnienia symulacji pomiędzy systemem skończom a systemem nieskończonym opisanym przez sieć Petriego. Wiadomo, że symulacja w obydwu kierunkach jest rozstrzygalna, ale niewiele wiadomo nt. złożoności. Wstępne wyniki dają EPXSPACE-trudność, ale pewnie można je łatwo poprawić. Ponadto jest ciekawe pytanie: czy istnieje skończona (ograniczona) symulacja? Problem ten jest motywowany modelami tzw. web serwisów, a jego rozstrzygalność jest wciąż otwarta.

Problemy decyzyjne dla jezykow przemiennych

Chodzi o problem przynaleznosci (czy dane slowo nalezy do jezyka) i rownosci (czy dwa jezyki sa rownowazne) dla bezkontekstowych jezykow przemiennych. Przemiennosc oznacza, ze zamiast slow mamy do czynienia ze skonczonymi multizbiorami. Dla problemu przynaleznosci, w szczegolnym przypadku jezykow regularnych, nie jest wciaz jasne, czy jest on wielomianowy (na pewno jest w NP). Dla problemu rownosci wciaz nie jest znana dokladna zlozonosc (jest w NEXPTIME). Problem przynaleznosci dla jezykow przemiennych to to samo, co osiagalnosc (reachability) w sieciach Petriego bez komunikacji. A problem rownosci to ,,reachability equivalence'' w takich sieciach.

Częściowo przemienne gramatyki bezkontekstowe

Problem przynależności danego słowa do języka generowanego przez daną gramatykę bezkontekstową jest wielomianowy, a w przypadku tzw. przemiennych gramatyk bezkontekstowych jest NP-zupełny. Zadaniem jest zdefiniowanie ogólnego pojęcia częściowo przemiennej gramatyki bezkontekstowej i zbadanie złożoności problemu przynależności. Prawdopodobnie przydatne będą tu techniki używane dla tzw. śladów Mazurkiewicza. Dalszym krokiem może być zbadanie problemu równoważności bisymulacyjnej procesów generowanych przez częściowo przemienne gramatyki bezkontekstowe.

Porownywanie efektywnosci sieci Petriego

Temat dotyczy wariantu rownowaznosci bisymulacyjnej uwzgledniajacego efektywnosc procesow. Podczas gdy zwykla rownowaznosc bisymulacyjna jest nierozsrzygalna dla sieci Petriego, wspomniany jej wariant ma szanse byc rozstrzygalny.

Dane vs. czas: porównanie automatów czasowych i automatów na danych

Ostatnio pojawiło się wiele ciekawych wyników dotyczących automatów czasowych (automaty z zegarami) i automatów akceptujących tzw. słowa z danymi (automaty z rejestrami). Te pierwsze potrafią opisywać systemy zależne od czasu a te drugie stosuje się m.in. do modelowania i analizy dokumentów XML. Zaskakująca jest daleko idąca analogia pomiędzy rezultatami osiągniętymi w dwóch światach: czasu i danych. Celem pracy ma być przyjrzenie się przyczynie tego zjawiska i być może jego wyjaśnienie.

Problemy decyzyjne dla modeli obliczeń z błędami

Maszyny licznikowe albo maszyny (automaty) z FIFO są równoważne maszynom Turinga co do siły wyrazu. Wyobrażmy sobie, że dopuszczamy pewien rodzaj usterek (błędów) podczas obliczeń: wartości liczników (zawartość FIFO) mogą w sposób niekontrolowany zmniejszać się (w innym wariancie mogą się zwiększać). Model z błędami jest słabszy i np. ma rozstrzygalny problem stopu. Praca powinna zawierać przegląd ostatnich wyników. Możemy też spróbować rozwiązać jakiś problem wciąż otwarty. Np. nie wiadomo, czy ograniczoność maszyn ze ,,zwiększającymi się'' licznikami jest rozstrzygalna. Nie wiadamo też, jakie języki są rozpoznawane przez automaty z FIFO.

S.Lasota (2008.10.03)