Dissertation Thesis Report
Study programme: PHD — Informatics, Masaryk University, Brno
Field of study: Informatics
Name of the student: Nikola Benes
Thesis title: Disjunctive Modal Transition Systems
Reviewer: associate professor Andrzej Wqsowski, PhD
Institution: IT University of Copenhagen, Denmark
The results of the work. I summarize the results of the work in order of their presentation in the thesis, by individual chapters.
Chapter 1 (7 pages) presents an introduction, a list of contributions and an overview of the dissertation text. Chapter 2 (7 pages) introduces preliminary definitions. It defines transition systems, and disjunctive modal transition systems (DMTS) — the main object of study in this work. The DMTSs are introduced in a fully general manner, using a notion of setting which allows to include both automata-like versions, and Kripke structure like models, or a combination of the two. The notion of setting, and a few other subclasses of DMTSs are essential for later development of the dissertation, which carefully studies the problems considered for various settings and subclasses.
Chapter 3 (34 pages) is the main chapter of the thesis discussing properties of refinement relations for various subclasses of DMTSs. First, it introduces the distinction between the modal and thorough refinement. The modal refinement is a simulation like co-inductive refinement—a direct generalization of the refinement for Modal Transition Systems of Larsen and Thomsen. Thorough refinement is a model theoretic refinement: based on inclusions of model sets of specifications. A detailed study of the relations between the modal and thorough refinement is presented concluding that the two refinements only coincide in three specific subclasses of models. Since deterministic specifications is an important subclass in these, Benes studies a determinization construction (deterministic hull) and proves that this construction is optimal for syntactically consistent processes, in the sense that there is no stronger deterministic over-approximation.
Subsequently, the author proceeds to study complexity of deciding refinements. Checking modal refinement is obviously in PTIME, given a simple co-inductive algorithm, and P-complete due to the fact that bi-simulation is its special case. However Benes adds quite a few more interesting results for deterministic subclasses, identifying six such, for which modal refinement checking is significantly easier, namely NL-complete. At the same time checking of thorough refinement for DMTSs is shown to be EXPTIME-complete. The upperbound is shown in a constructive manner, while the lowerbound requires an involved reduction from acceptance for alternating linear bounded automata. This hardness result closes a complexity gap
1
for the problem of thorough refinement checking for modal transition systems, left open in our earlier work. The result is also positively surprising, as it shows that in general checking thorough refinement for Modal Transition Systems is just as hard as for DMTSs, which is a more expressive model (the difference in expressiveness is formally shown with a counterexample in the end of chapter 4).
Chapter 4(13 pages) is devoted to consistency of DMTSs, where a DMTS is consistent if it admits at least one model (implementation). Consistency checking for DMTSs is shown to be EXPTIME-complete, which is a strengthening of a result that I co-authored myself, that this problem is EXPTIME-complete for the subclass of mixed transition systems. Like for modal refinement, the fact that consistency checking does not become harder for DMTSs is positively surprising.
In the same diligent style as in the previous chapter, Beneš studies the problem for subclasses of input instances, establishing that it is P-complete for a bounded number of modal transition systems and for consistent deterministic DMTSs. The deterministic subclasses are further analyzed, to identify cases where the problem becomes NL-complete. It is particularly interesting to see that determinism separates modal transition systems from DMTSs for consistency. The problem turns out to be NL-complete for the former, and P-complete for the latter, which further supports expressiveness differences between the two models.
Chapter 5(15 pages) studies the generalized model checking problem for the LTL logics specification interpreted over DMTSs. The chapter recalls the definition of LTL and its semantics over Kripke transition systems. Then it lifts the semantics to DMTSs in existential and universal style. The objective is to study complexity of model checking problems for these new semantics. Beneš shows that universal model checking is PSPACE-complete for consistent DMTSs, while the existential model checking is 2-EXPTIME-complete for the same language. The universal problem is primarily useful for the safety properties, while the existential variant has a flavor of the controller synthesis problem, so establishment of the complexity gap between the two is quite interesting. In due dilligence, the thesis studies the variations of the problem for modal transition systems, and for finite and infinite words, finding that the difference from the above reported complexity classes only appears for the existential problem over infinite words for modal transition systems (PSPACE-complete).
Chapter 6 (3 pages) concludes the thesis, and sketches directions for future work.
Besides the main results summarized above, the thesis presents a very high number of individual small results for subclasses of problems, counterexamples, for various settings, and many derivable corollaries, due to inclusions between the studied model classes and settings.
The work of Beneš has been published in as many as 11 papers, accepted at
2
internationally venues, including two articles in high quality journals (Theoretical Computer Science and Science of Computer Programming), and papers in respectable international conferences, such as ICTAC and ATVA, with peer-reviewed and archived proceedings. This broad range of publications demonstrates not only the quality of the results presented in the thesis, but also wide interests of the author and contributions to research problems outside the scope of the dissertation. In my opinion, this high productivity characterizes a good independent researcher.
Structure of the Thesis. The text is logically organized, including both the split of the material into chapters, and the way each chapter goes into details into various subproblems. The organization of the study for each of the problems demonstrates high degree of diligence and high research standards.
Comments on the Text. The text does summarize related work, and contains a fare number of citations. Sometimes it would be beneficial to draw a more holistic picture of the relation between the new results and existing work on similar and related models of computation.
Language and Graphic Level. The thesis is very well written, using mature mathematical language. The text is supplemented with figures whenever necessary, to demonstrate constructions and counterexamples. The writing style is terse, but I was not able to point out any serious mistakes. I would like to commend the author for remarkably careful writing.
Questions for the Defense.   The following are my main questions:
1. The DMTS model has been introduced by Larsen and Xinxin not as a specification formali sm, but as a technical device to characterize solutions of equation systems in process algebra. Given the complexity results in this thesis, what is your opinion about the future of DMTSs as a specification formalism? Is there a subclass of the models for which a number of interesting questions are tractable, while it is still expressive enough for compositional design.
2. Even though you interpret DMTSs as a specification formalism, you seem to side step an essential operator: parallel composition. Do you see any challenges in defining parallel composition for DMTSs? Are there any specific decision problems related for parallel composition of DTMSs? Is there any hope of decomposition of one process into parallel processes being decidable?
3
3. I would like to understand how the results on expressiveness of mixed and modal transition systems (page 66) relate to the recent paper by Wei and coauthors from VMCAF09 (the paper cited as [WGC09] in the dissertation). In that paper a construction translating from Generalized Kripke Modal Transition Systems to mixed transition systems is presented (see section IV), which at first appears as if it contradicted your result.
4. Could you comment on complexity of generalized model checking of CTL over DMTSs? 1 expect that the counterpart of Theorem 5.3 is easy to achieve. Any conjectures about Theorem 5.4 for CTL? Why did you decide to study LTL and not CTL?
5. Do you expect any preservation results to be obtainable for modal refinement for DMTSs with respect to CTL and LTL properties?
Conclusion. The author in his distinguished dissertation thesis has demonstrated ability to work independently and creatively in the specified field. The thesis meets the standard requirements imposed on the dissertation thesis in the field. I clearly recommend this work to be accepted.
Copenhagen, April 15, 2012
Andrzej Wqsowski, PhD
Masarykova univerzita
Fakulta informatiky
Počat a druh nejist pffloti:
J.
MU107850
4
MU107850