I. Tematy raczej praktyczne
Zastosowanie (hierarchicznej) agregacji w stochastycznej weryfikacji modelowej
| Probabilistyczna weryfikacja modelowa (ang. probabilistic model-checking) to metoda weryfikacji modeli probabilistycznych, takich jak łańcuch Markowa. Oprócz aspektu jakościowego (coś się wydarzy lub nie) mamy tu na ogół do czynienia również z aspektem ilościowym (coś się wydarzy z jakimś prawdopodobieństwem), dlatego weryfikacja modelowa wymaga rozwiązywania układów równań liniowych. Używane są najczęściej algorytmy iteracyjne, tak jest np. w narzędziu PRISM. Celem pracy jest implementacja wybranego algorytmu agregacyjnego, zintegrowanie go z narzędziem PRISM, i eksperymentalna ewaluacja tego rozszerzenia na wybranych case-studies. Kontynuacją tej pracy, np. w ramach doktoratu, będzie implementacja algorytmu hierarchicznej agregacji zaproponowanego w pracy doktorskiej P. Pokarowskiego. |
Analiza wrażliwości ścieżek sygnałowych
| 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), głownie probabilistyczna. Celem pracy będzie analiza wrażliwości probabilistycznego modelu szlaku sygnałowego przy użyciu narzędzia PRISM. Eksperymenty przeprowadzone zostaną w środowisku Taverna. |
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. |
Weryfikacja programów binarnych
| Ostatnio coraz większe zainteresowanie skupia weryfikacja programów, w sytuacji gdy dysponujemy tylko kodem binarnym, a kod źródłowy jest niedostępny. Celem pracy jest analiza wykonalności takiej weryfikacji, tj. identyfikacja trudności i oszacowanie możliwości ich rozwiązania. Do eksperymentów użyjemy (lub zaadaptujemy) narzędzie CBMC służące do weryfikacji programów w C. Naturalną kontynuacją tej pracy, np. w ramach doktoratu, może być opracowanie nowego narzędzia, opartego prawdopodobnie, tak jak CBMC, na metodzie ograniczonej weryfikacji modelowej. |
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. |
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 (2009.04.22)