Aktualności

Dr Krystian Jobczyk z Wydziału Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej otrzymał stypendium Senior Award programu Fulbright, które umożliwi mu prowadzenie badań w Stanach Zjednoczonych w roku akademickim 2020/2021.

Naukowiec wyjedzie do Centrum Badań im. Saula Kripkego (The Saul Kripke Center) na Uniwersytecie Miejskim w Nowym Yorku (CUNY), gdzie przez dziewięć miesięcy będzie realizować projekt dotyczący tzw. reaktywnej weryfikacji modelowej dla systemów logiki temporalnej w semantyce punktowej. Tytuł projektu brzmi „Reaktywne semantyki Kripkego i reaktywne automaty w użyciu, czyli w stronę reaktywnej weryfikacji modelowej dla systemów logiki temporalnej interpretowanej w semantyce punktowej”.

Każdy z nas ma do czynienia z różnorodnymi systemami rozumianymi ogólnie jako kolekcja obiektów o określonych relacjach przestrzennych z zadanym zbiorem akcji, które można nad tymi obiektami wykonać. Systemem może być hardware, software, interfejs użytkownika, automat do kawy lub biologiczny system regulacji genowej w komórkach.

Zazwyczaj zakłada się (zwłaszcza w odniesieniu do systemów sztucznych, np. znanych z praktyki informatyka) szereg warunków nakładanych na działanie i żywotność systemów, np. brak zakleszczeń akcji lub ich odpowiednia sekwencyjność. Ich spełnienie istotnie jest nie tylko dla poprawnego działania tych systemów, ale także dla ich bezpieczeństwa.

Aby zweryfikować czy zadane własności są spełnione, w badanych systemach w ramach tzw. weryfikacji modelowej same własności koduje się w różnych językach sformalizowanych, takich jak: język liniowej logiki temporalnej, logiki czasu rozgałęzionego, rachunku Hennesy-Milnera czy logiki Halperna-Shohama. Jednocześnie – zamiast samych systemów – rozważamy ich abstrakcyjne modele, takie jak: struktury Kripkego, automaty skończone czy tzw. systemy tranzycyjne.

Tymczasem rozważane systemy są zazwyczaj dynamiczne, wykazując tzw. reaktywność (reagują z otoczeniem, człowiekiem czy operującym agentem), a reprezentujące je modele – nie. Istnieje więc potrzeba wprowadzenie nowych reaktywnych modeli, bardziej adekwatnych dla weryfikacji oczekiwanych własności systemów.

Przedmiotem badań dr. Krystiana Jobczyka będzie właśnie konstrukcja takich modeli, dobrze „zgranych” z systemami logiki temporalnej (takich jak: reaktywne struktury Krikego czy reaktywne automaty) oraz opracowanie dla tych modeli zrębów reaktywnej weryfikacji modelowej. Dodatkowym celem projektu stanie się próba opracowania narzędzi dla automatycznej weryfikacji modelowej.

Dr Krystian Jobczyk w 2011 r. uzyskał tytuł doktora nauk humanistycznych w zakresie filozofii, a w 2017 r. tytuł doktora nauk technicznych w zakresie informatyki. Obszary jego badań obejmują logikę, informatykę teoretyczną na użytek AI, podstawy matematyki, epistemologię.

W latach 2011–2013 w Monachijskim Centrum Matematyki Filozoficznej (MCMP) na Uniwersytecie Ludwika Maksymiliana badacz zajmował się projektem z filozofii matematycznej, który dotyczył filozoficznej i formalnej korekty tzw. antyrealizmu semantycznego Putnama. W ramach drugiego doktoratu na Uniwersytecie w Caen we Francji oraz we współpracy z AGH prowadził badania na temat kwestii znajdowania nowych paradygmatów w modelowaniu problemów planowania temporalnego z ograniczeniami rozmytymi i preferencjami.

Z Akademią Górniczo-Hutniczą związany jest od 2017 r. W Katedrze Informatyki Stosowanej prowadzi zajęcia na studiach drugiego stopnia: SMADA – System Modeling and Data Analysis.

Program Fulbrighta to największy program wymiany naukowej i kulturowej Stanów Zjednoczonych. Od ponad 70 lat wspiera współpracę na rzecz rozwoju nauki, kultury oraz relacji międzyludzkich i międzyinstytucjonalnych pomiędzy Stanami Zjednoczonymi a ponad 160 krajami. Program Fulbrighta finansuje wyjazdy naukowe polskich studentów, badaczy i nauczycieli akademickich do USA i wspiera ich obiecujące projekty. Zgodnie z wizją inicjatora Programu, amerykańskiego senatora J. Williama Fulbrighta, jest to narzędzie w budowaniu dialogu i pokojowych relacji między narodami. Program Fulbrighta działa dwukierunkowo – również amerykańscy badacze i eksperci mają możliwość przyjazdu i pobytu naukowego w Polsce. Dzięki temu wiele polskich instytucji akademickich i edukacyjnych oraz organizacji pozarządowych ma możliwość zaproszenia do współpracy przy swoich projektach specjalistów i wykładowców z USA.