Dr Wojciech Czerwiński z Wydziału Matematyki, Informatyki i Mechaniki UW dołączył do grona laureatów prestiżowych grantów Europejskiej Rady ds. Badań Naukowych. Jego zespół  podejmie kilka ważnych wyzwań dotyczących systemów informatycznych o nieskończonej liczbie stanów.

Czy da się opracować szybszy algorytm odpowiadający na pytanie o osiągalność poszczególnych stanów konkretnego systemu komputerowego? To jedno z pytań, na które w ramach swoich badań  postara się odpowiedzieć dr Wojciech Czerwiński z Instytutu Informatyki UW.

Pytania o osiągalność

Czym jest model? Najogólniej rzecz ujmując – uproszczonym obrazem rzeczywistości, dzięki któremu łatwiej jest przedstawić dany problem. Mamy modele samolotów, osobowości czy Wszechświata. Na modelach pracują meteorolodzy, fizycy, matematycy, psycholodzy i reprezentanci wielu innych dyscyplin naukowych. Także informatycy.

– Istnieją np. modele obliczeń zwane systemami stanowymi  – mówi dr Wojciech Czerwiński, adiunkt w Instytucie Informatyki na Wydziale Matematyki, Informatyki i Mechaniki UW. To właśnie wokół wspomnianych systemów stanowych koncentruje się jego projekt, który został nagrodzony prestiżowym Starting Grant ERC.

„Challenging Problems in Infinite-State Systems” (INFSYS) ma na celu podjęcie kilku ważnych wyzwań dotyczących systemów informatycznych, określanych nieskończenie stanowymi. – Jeśli wyobrazimy sobie program jako coś, co przechodzi z jednego stanu do drugiego, możemy zadać sobie pytanie: czy po wystartowaniu z jednego stanu program może popełnić błąd, dochodząc do pewnego złego stanu końcowego? W ten sposób wykrywa się błędy w programach – tłumaczy dr Czerwiński, dodając: – W praktyce polega to na sprawdzeniu pewnego wycinka programu: podukładu, procesora etc. Można sobie zamodelować wybrany jego aspekt i zobaczyć, czy start z danej konfiguracji pozwala na dalszy ciąg kroków.

Dr Czerwiński podkreśla, że nagrodzony projekt wpisuje się w badania podstawowe, tzn. takie, które mają na celu teoretyczne opracowanie danych zjawisk, wyjaśnienie ich specyfiki, a nie przygotowanie do bezpośredniego komercyjnego zastosowania. – O naszych badaniach fundamentalnych myślę raczej jako o inwestycji długoterminowej, tzn. my nie robimy czegoś, co za rok nagle zmieni świat albo odniesie sukces finansowy, tylko raczej staramy się rozwijać dziedzinę. Może się okazać, że za 10 czy 20 lat to się przyczyni do znaczącego przełomu w technologii – dodaje badacz.

Autor projektu INFSYS zakłada przedstawienie rozwiązań dla największych wyzwań pojawiających się w obszarze systemów nieskończenie stanowych. Cele projektu koncentrują się wokół trzech głównych problemów.

Jednym z nich jest osiągalność w sieciach Petriego i systemach VAS (Vector Addition Systems). – Sieć Petriego jest modelem zakładającym istnienie kilku różnych zasobów. Dla uproszczenia można powiedzieć, że są to jabłka, gruszki i śliwki. W praktyce mogą to być np. substancje chemiczne albo, jeśli chodzi o informatykę, różne rodzaje programów komputerowych. Wracając jednak do uproszczenia, wyobraźmy sobie, że na początku mamy w systemie 5 jabłek, 5 śliwek i 5 gruszek. Możemy wykonywać różnego typu ruchy: dodać 2 jabłka czy zabrać 1 jabłko, 1 gruszkę i 1 śliwkę. Albo dodać 3 jabłka i 3 śliwki naraz. Mamy kilka tego typu ruchów. Pytanie, czy możemy z tych 5 jabłek, 5 śliwek i 5 gruszek dojść na końcu do 11 jabłek, 11 gruszek i 11 śliwek – tłumaczy dr Czerwiński.

Celem projektu jest m.in. stworzenie algorytmu, który dla danego systemu, określającego sytuację początkową i zestaw ruchów do dyspozycji, odpowiedziałby na pytanie o możliwość przejścia do konkretnej sytuacji końcowej. – Takie algorytmy już, oczywiście, istnieją, ale my staramy się stworzyć szybszy. Albo udowodnić, że nie da się szybszego zaprojektować. Mowa tu o konkretnym problemie osiągalności – mówi dr Czerwiński.

Kwestia ta była już przez naukowca poruszana w ramach jego wcześniejszych badań. Przedstawiono ją np. w artykule pt. „The Reachability Problem for Petri Nets is Not Elementary”, za który dr Wojciech Czerwiński wraz ze współautorami otrzymał Best Paper Award na zeszłorocznej konferencji ACM Symposium on Theory of Computing.

Pozostałe dwa problemy zaprezentowane w projekcie INFSYS dotyczą m.in. separacji w teorii automatów oraz automatów jednoznacznych.