Příloha 6: Posudek oponenta habilitační práce
Masarykova univerzita Fakulta
Habilitační obor
Fakulta informatiky Informatika
Uchazeč Pracoviště Habilitační práce
RNDr. Jan Strejček, Ph.D. Fakulta informatiky
From Infinite-State Systems to Translation of LTL to Automata
Oponent Pracoviště
prof. RNDr. Petr Jančar, CSc. FEI VŠB-TU Ostrava
Text posudku (rozsah dle zvážení oponenta)
Předložená habilitační práce je souborem čtyř článků publikovaných v renomovaných mezinárodních časopisech v oblasti teoretické informatiky (Theoretical Computer Science, Acta Informatica, Information and Computation, Mathematical Structures in Computer Science) a sedmi příspěvků ve sbornících kvalitních mezinárodních konferencí a workshopů (jako FSTTCS, TACAS, Express, a také Concur, když počítáme i předběžné verze zmíněných časopiseckých publikací). V jednom případě je J. Strejček samostatným autorem, v dalších případech jsou jeho spoluautory zpravidla kolegové z FI MU, ve dvou případech se pak jedná výhradně o zahraniční spoluatory z renomovaných evropských pracovišť. Soubor prací je opatřen úvodním přehledem v rozsahu zhruba dvaceti stran.
Práce přispívají do oblasti teorie automatizované verifikace systémů, v jednom případě se jedná i o práci zahrnující experimentální vyhodnocení. Většina prací rozšiřuje poznatky o vyjadřovací síle a otázkách rozhodnutelnosti základních problémů automatizované verifikace (problém dosažitelnosti, ověřování modelu [model checking], behaviorální ekvivalence) v kontextu tzv. procesových přepisovacích systémů (Process Rewrite Systems, PRS).
Z oblasti problému dosažitelnosti mohu vyzdvihnout např. zpřesnění hranice rozhodnutelnosti mezi případem PRS, kde byla známa rozhodnutelnost, a případem se-PRS (state-extended PRS), kde je problém nerozhodnutelný, díky turingovské síle modelu rozšiřujícího PRS o konečnou stavovou jednotku. J. Strejček a jeho spoluautoři zavedli a prozkoumali model wPRS (weak PRS), který vznikne omezením stavové jednotky v se-PRS, a rozšířili důkaz rozhodnutelnosti dosažitelnosti na případ wPRS. S renomovanými zahraničními odborníky pak v oblasti problému dosažitelnosti J. Strejček přispěl k vylepšení algoritmu pro omezenou dosažitelnost v případě (turingovsky úplného) modelu ispirovaného vícevláknovým software s asynchronní komunikací.
V oblasti „model checkingu" vypadá zvlášť zajímavě případ lineární temporální logiky (LTL), kde byla dokázána rozhodnutelnost pro wPRS a některé fragmenty LTL; případ je zajímavý mj. vztahem k překladu na Buchiho automaty zmíněným níže.
V případě ověřování ekvivalencí se J. Strejček se spoluautory zřejmě snažili o zodpovězení otevřených otázek rozhodnutelnosti slabé bisimulační ekvivalence pro základní třídy sekvenčních (BPA) a paralelních (BPP) procesů. Tyto otázky zůstávají stále otevřené, ale podařilo se jim ukázat nerozhodnutelnost už pro velmi slabé rozšíření (normované fcBPA a
fcBPP).
Výše zmíněné zajímavé uplatnění předchozí práce na „model checkingu" LTL se objevilo na letošní významné konferenci TACAS (Tools and Algorithms for the Construction and Analysis of Systems). J. Strejček a spoluautoři navrhli úpravy známých algoritmů pro překlad formulí LTL na Buchiho automaty (což je jedna ze standardních procedur u automatizované verifikace) a také navrhli techniky redukce nedeterminismu (což je zřejmě v praxi užitečnější než minimalizace velikosti automatu). Zlepšený překlad implementovali a experimentálně úspěšně vyhodnotili.
Úvodní kapitola dávající čtenáři přehled o souboru prací je srozumitelná a stručná (přesto s několika překlepy, odkazem na obr. 3.2. místo 3.3, apod.). Podle mého názoru ale autor zvolil „minimalistický" přístup, počítá spíše se čtenářem specialistou, který nepotřebuje ani základní definice a osvětlující příklady, než se čtenářem pracujícím např. v jiném informatickém oboru. I jako čtenář specialista bych ovšem uvítal, kdyby autor věnoval více prostoru a úsilí přiblížení myšlenek výzkumných úspěchů, kterých si nejvíce cení.
Kromě prací zařazených do souboru je J. Strejček (spolu)autorem i dalších kvalitních prací. Citace dokládají, že jeho práce je známa a oceňována v mezinárodní vědecké komunitě činné v oblasti automatizované (formální) verifikace, tedy v oblasti živého celosvětového výzkumu, jejíž důležitost je v situaci naší všudypřítomné závislosti na fungování složitých softwarových a hardwarových systémů zřejmá.
V poslední době J. Strejček zřejmě také úspěšně spolupracuje jako konzultant s doktorskými studenty (letošní práce na TACAS je jedním z příkladů) a má za sebou solidní pedagogickou praxi. Znám jej také osobně a neváhám s pozitivním závěrem níže.
Dotazy oponenta k obhajobě habilitační práce (počet dotazů dle zvážení oponenta)
V souvislosti s mou poznámkou o „minimalistickém přístupu" zkuste vědecké radě naznačit výzkumné myšlenky, které považujete ve své práci za nejdůležitější a u nichž jste jedním z hlavních autorů.
Habilitační práce Jana Strejčka „From Infinite-State Systems to Translation of LTL to Automata" splňuje požadavky standardně kladené na habilitační práce v oboru Informatika.
Závěr
Ostrava, 23.9.2012
MU169309
MU169309