Dla starożytnych nocne niebo było nieocenionym drogowskazem i narzędziem nawigacyjnym. POLARIS – projekt prof. Wojciecha Czerwińskiego, którego nazwa pochodzi od Gwiazdy Polarnej – poprowadzi badacza z Wydziału Matematyki, Informatyki i Mechaniki UW bliżej rozwiązania jednego z kluczowych dylematów w informatyce, jakim są granice osiągalności w systemach z nieskończoną liczbą stanów. Naukowiec został laureatem grantu Consolidator Europejskiej Rady ds. Badań Naukowych.
Swój pierwszy grant ERC Wojciech Czerwiński – jeszcze jako doktor – zdobył pięć lat temu. Teraz jest doktorem habilitowanym, profesorem uczelni i jednym z 10 reprezentantów Wydziału Matematyki, Informatyki i Mechaniki UW w gronie laureatów tego prestiżowego konkursu.
Nieustannie zadaje trudne pytania o osiągalność w systemach nieskończonych, czyli – jak wyjaśnia badacz – w takich modelach programów, które charakteryzuje nieskończona liczba możliwych stanów.
Inspiracją okazało się tym razem nocne niebo – jego obserwacja to prywatnie hobby profesora. POLARIS – akronim projektu – nawiązuje do Gwiazdy Polarnej. To niezwykłe ciało już w starożytności służyło za jedno z najlepszych narzędzi nawigacyjnych.
Każdy z nas nawiguje właściwie codziennie. Sprawdzamy na przykład, jak najprościej i najszybciej dostać się z punktu A do punktu B w zatłoczonym mieście. Podobne dylematy rozwiązuje też prof. Wojciech Czerwiński. Tyle że w programach komputerowych, badając wpływające na ich funkcjonowanie ruchy i procedury.
– Jestem skoncentrowany na poszukiwaniu technik pozwalających możliwie szybko i prosto rozwiązać problem osiągalności. A jego zrozumienie jest kluczowym czynnikiem wpływającym na lepsze poznanie działania programów – mówi prof. Czerwiński.
Naukowiec pracuje na modelach obliczeń zwanych systemami stanowymi – zwłaszcza nieskończenie stanowymi. Lwia część jego projektu dotyczy sprawdzenia, czy da się opracować szybszy niż dotychczasowe algorytm pozwalający przejść z sytuacji początkowej do końcowej danego programu.
Szybko, szybciej, najszybciej
O jakie systemy chodzi? – Mówiąc o systemie, mam na myśli model obliczeniowy zdolny do obrazowania wielu rodzajów zasobów. Wśród nich są np. sieć Petriego czy VAS, czyli Vector Addition Systems. Dla uproszczenia można sobie wyobrazić, że wspomnianymi zasobami są jabłka, gruszki i śliwki. W praktyce mogą to być substancje chemiczne albo, jeśli chodzi o informatykę, rozmaite programy komputerowe. Wracając jednak do uproszczenia, wyobraźmy sobie, że na początku mamy w systemie pięć jabłek, pięć śliwek i pięć gruszek. Możemy wykonywać różnego typu ruchy: dodać dwa jabłka czy zabrać jedno jabłko, jedną gruszkę i jedną śliwkę. Albo zamienić trzy jabłka na trzy śliwki. Mamy do dyspozycji kilka tego typu ruchów. Pytanie, czy możemy z tych pięciu jabłek, pięciu śliwek i pięciu gruszek przejść ostatecznie do 11 jabłek, 11 gruszek i 11 śliwek – tłumaczy dr Czerwiński.
Z pozoru problem osiągalności wydaje się prosty, jednak w rzeczywistości pozostaje trudny i nieoczywisty. Gdzie leży granica ich maksymalnej szybkości? Nad odpowiedzią w ciągu najbliższych pięciu lat będzie się zastanawiał zespół POLARIS prof. Wojciecha Czerwińskiego.
Projekt prof. Wojciecha Czerwińskiego pt. Reachability in Infinite Systems at High Resolution (POLARIS) uzyskał dofinansowanie w wysokości niemal 2 mln euro. Realizacja grantu Consolidator rozpocznie się w 2026 roku i potrwa pięć lat.
Dr hab. Wojciech Czerwiński, prof. ucz. pracuje w Instytucie Informatyki na Wydziale Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego. Zajmuje się teorią automatów, modelami współbieżności oraz logiką w informatyce. W latach 2017–2019 realizował projekt pt. Separability problem in automata theory, dofinansowany w konkursie SONATA Narodowego Centrum Nauki. W 2020 roku zdobył Starting Grant ERC na realizację projektu Challenging Problems in Infinite-State Systems (INFSYS).
W przygotowaniu aplikacji projektowych o granty ERC naukowców z UW wspiera Biuro Międzynarodowych Programów Badawczych, które organizuje spotkania informacyjne i szkoleniowe, panele próbne przed drugim (ustnym) etapem konkursu, prowadzi konsultacje indywidualne, a w razie przyznania środków na realizację projektu, przygotowuje umowę grantową.
BMPB UW współpracuje z ekspertem ds. prezentacji naukowych – prof. Piotrem Wasylczykiem z Wydziału Fizyki, panelistami ERC i laureatami grantów ERC (recenzje wewnętrzne, panele próbne) oraz z KPK PB UE (NCBR).