Prof. Jiri Zlatuska, Dean
Masaryk University
Faculty of Informatics
Department for Research and Development
Botanicka 68a, 602 00 Brno, Czech Republic
April 12, 2010
Dear Prof Zlatuska,
Thank you for inviting me to be part of Jana's PhD thesis committee. As I am very
interested in recent results from the ParaDiSe Lab, and in particular in Ivana's and Jiri's
work in quantitative formal verification, it is my pleasure to be part of the committee. I am
including below a short review of the PhD thesis proposal that you sent me some time
ago.
Central to the proposed work is a particular type of a transition system, called Transition
System with Degradation (TSD). Such models, which include the well known Markov
Decision Processes as a subclass, seem to be relevant to a number of applications
where the “strength” of a signal or a piece of information degrades along the trajectories
of the system. Given the particular semantics of such systems, new types of linear
temporal logics and corresponding Buchi automata are needed. The author proposes to
develop and implement the necessary computational frameworks. Both verification and
controller synthesis problems are proposed as part of this PhD thesis.
The proposed research is interesting, novel, and has the potential to significantly impact
the (well-established) formal verification and the (emerging) formal synthesis
communities. The review of related work is adequate. The research plan is well
structured. The author already has preliminary results, which gives me confidence that
she will be successful in achieving the proposed plan.
In the rest of this review, I will give some (minor) suggestions for improvement. Note that
some of these are mostly on the broader impact of the proposed research, and the
author might be expected to only include a short discussion in the thesis.
1) Some more motivation for the use of TSD is desirable. The author only gives a small
academic example from a communication network. Are these models appropriate for
biological networks? How about mobile robotics?
2) There is no discussion on the expected complexity of the proposed verification and
synthesis algorithms. What is the size of the models that she expects to be able to
handle? Is this size relevant to real-world applications?
3) Can TSD be seen as abstractions of any class of (infinite) continuous systems? There
is a large body of literature (mostly from the control theoretic community) on building
abstractions of infinite systems in the form of transition systems and MDP. Maybe (multirate)
timed automata (see works by Alur and Henzinger) with negative rates can be
abstracted to TSD?
4) The notion of what is degraded in a TSD is not very clear. The author mentions
“quality” at some point. Would it make sense that the degradation be defined for the
atomic propositions? Also, I am not sure I see the connection between the (only type of)
degradation in the TSD and the (several) degradation variables in the BADC.
5) It would be great if the author can make a comparison between TSD and other types
of models, i.e, in addition to transition systems and MDPs. How about Petri nets? Among
the several types of Petri nets, are there any that are semantically close to TSD?
6) How hard would it be to extend the proposed work to systems for which the state is
not known exactly? For example, when the state of an MDP is only known up to a
distribution, the MDP becomes a POMDP. Can the proposed synthesis approach be
extended to such systems?
In conclusion, I think this is a strong thesis plan with very encouraging preliminary
results. Please feel free to contact me. I would be happy to provide more information.
Best regards,
Calin Belta