Annex 6: Habilitation thesis reader's report
Masaryk University Faculty
Field of Habilitation
MU Faculty of Informatics Informatics
Applicant Affiliation Habilitation Thesis
RNDr. Jan Strejček, Ph.D.
Masaryk University, Faculty of Informatics
From Infinite-State Systems to Translation of LTL to Automata
Reader Affiliation
Professor Jaco van de Pol
University of Twente, The Nertherlands
Report Text (as large as the reader deems necessary)
I have read Dr. Jan Strejcek's habilitation thesis with pleasure. It is based on 4 journal and 7 international peer-reviewed conference papers, and accompanied with an introduction on the state-of-art in the field and a clear comprehensive summary of the contributions. The papers are without exception very skillful, and mainly present the author's progress from 2001-2006 in solving dedicability problems for reachability, linear-time model checking and equivalence checking for infinite state systems, presented as subsystems of Process Rewrite Systems (PRS). To study the fine structure of the decidable borderline, the author has introduced a number of new subsystems, extending them with finite control and finite constraints. Besides, the author also extended hierarchy of LTL-fragments to precisely pinpoint the decidability boundary of model checking.
These papers, co-authored with various strong members of the theoretical computer science community, are exceptionally well-written. They are self-containing both in introducing the necessary mathematical and formal background, in summarizing the related work, in explaining in detail all necessary constructions, and in explaining the relevance for the validation of computer-based embedded systems. In particular, the relationship between modern multi-core software and the theoretical infinite-state systems is carefully explained. A second (more recent) line of papers improves the translation of LTL formula's to Biichi automata. Some theoretical observations on weak and almost linear Biichi automata led to some very practical improvements in the translation. As a result, the author improved a longstanding widely-used tool LTL2BA in several ways, making it both more time- and memory-efficient and improving the quality of the resulting automata, making them smaller and more deterministic. This has direct consequences for the broad field of model checking, as it is currently routinely applied to many hardware and software systems.
Reader's questions to answer to defend the habilitation thesis (number of questions is upon reader's consideration)
1. Most of the results are concerned with decidability issues of model checking on infinite state systems. One of the motivations is that verification of finite models is infeasible, since they become very large. But, how practical are the model checking algorithms for infinite state systems in terms of their memory and time complexity?
[ it seems that besides the translation of LTL to Biichi automata, the paper doesn't address the practical or theoretical efficiency of model checking algorithms ]
2. Perhaps the most important open questions in this field are the decidability of strong equivalence for PA and weak equivalence for BPA and BPP. What is the perspective of solving these problems in the near future, and (how) does your study of the fine-structure of Process Rewrite Systems contribute to those main open questions?
Conclusion
Jan Strejcek's habilitation thesis of"From Infinite-State Systems to Translation of LTL to Automata " does   docs not meet the standard requirements for a habilitation thesis in the field of Informatics.
In Enschede on 31 august 2012
MU164206
MU164206