TECHNISCHE
HOCHSCHULE
AACHEN
RHEINISCH-
WESTFÄLISCHE
L E H R S T U H L INFORMATIK 2
PROF. DR. IR. J.-P. KATOEN
SOFTWAREMODELLIERUNG UND VERIFIKATION
Lehrstuhl Informatik 2 - RWTH Aachen - D-52056 Aachen Ahornstraße 55, D-52074 Aachen/Germany
Review of the dissertation, entitled
'Modal Transition Systems: Extensions and Analysisit
by Jan Kretínský
Masaryk University, Brno
June 20, 2014
Introduction and background
This dissertation is concerned with modal transition systems (MTSs), a specification formalism
for labeled transition systems originated by Larsen and Thomsen in 1988. MTSs aim to provide
an operational specification formalism that can be used in a step-wise development process of
reactive systems. They extend labeled transition systems by replacing the ordinary transition
relation between states into must and may transitions. Must transitions are required, i.e., each
implementation must realize them. May transitions are optional and may be present in an
implementation, but this is not mandatory. The theory of MTSs is equipped with a natural notion
of refinement - when is a model a correct refinement of another one? - and quotienting - what is
the most general process X such that X in parallel with an exisiting component T satisfies the
MTS S? MTSs have been used in interface theories, product line theories, program analysis
using abstraction, and MTS-based software engineering.
The subject of the dissertation is on the one hand to study several extensions of MTSs with more
expressive notions for specifying which transitions need to be present, with time durations of
actions, prices of actions, infinite-state MTSs, etc., and on the other hand to develop new analysis
algorithms (with accompanying tool support) for MTSs, e.g., for checking refinement between
MTSs and computing the cheapest implementation of a given MTS. For the analysis algorithms
also the theoretical complexity is determined.
Main contributions and structure of the dissertation
The dissertation focuses on two main aspects: extensions of modal transition systems (MTSs) and
the analysis of MTSs.
Extensions of MTSs. Kfetinsky proposes two extensions for describing which transitions in an
implementation of an MTS should be present: Boolean MTS (BMTS) and parametric MTS
(PMTS). BMTSs extend MTSs by the possibility to specify an exclusive choice between the
existence of transitions, whereas PMTSs allow top make certain choices persistent. BMTSs are
in fact defined as parametric-free PMTSs. It is shown that any PMTS can be de-parameterised
into (a possibly exponentially larger) BMTS, and that any BMTS can be transformed into an
equivalent disjunctive MTS, again at the cost of an exponential blow-up. Disjunctive MTS is a
variant of MTS (by Larsen and Xinxin, 1990) that specifiy a disjunction over transitions. DMTSs
with more initial states are strictly more expressive that classical DTMSs with a single initial
state. Altogether, this yields the result that any finite set of labeled transition systems can be
either represented by a finite PMTS, a finite BMTS, or a finite set of finite DMTSs. In addition,
it is proven that a DMTS (with several initial states) is equivalent to a formula in HennessyMilner
logic (without greatest fixed points). These results are summarized in Chapter 3. In
addition, a timed extension of BMTSs is presented in which the duration of transitions is modeled
as controllable (i.e., chosen by the implementation) or uncontrollable intervals (i.e., chosen by the
environment), and process rewrite systems, a formalism to decsribe infinite-state labeled
transition systems, is extended so as to accommodate the specification of infinite-state MTSs.
These extensions are described in Chapter 4.
Analysis of MTSs. As stated above, PMTSs can be exponentially more succinct than BMTSs and
in turn BMTSs can be exponentially more succinct than DTMS (with several initial states).
Kfetinsky studies the theoretical complexity of refinement checking between different types of
MTSs, both with and without parameters. Since all complexities are in PSPACE, Kfetinsky
resorts to reduce refinement to problems solvable by QBF solvers. Practical experiments show
that the presence of non-determinism in MTSs is the most influential factor in run times. It is
shown that modal refinement coincides with thorough refinement (entailing an inclusion of the
set of implementations) except for PMTSs; in addition, a classification of modal process rewrite
systems is given for which refinement with respect to a finite or infinite specification is decidable.
Kfetinsky also shows the closure of PMTSs (and BMTSs and DMTSs with several initial states)
under operations such as conjunction, disjunction, parallel composition and quotienting. MTSs
are shown not to be closed under conjunction. Finally, the model checking of MTSs against LTL
is considered. The complexity of LTL model checking for different settings is considered (all
implemengtations, some implementations, deadlock-free etc.). An interesting result is the new
translation of LTL into generalised deterministic Rabin automata. A nice (and practical) result is
that parallel composition preserves and reflects all LTL properties. As a final result, the timed
MTSs are equipped with two prices (running costs per action per time unit, and resource
requirements per action), yielding the natural question on obtaining the "cheapest"
implementation. Here, the running cost is considered to be the worst-case long-run average cost.
The general problem is shown to be NP-complete, whereas a restricted version (e.g. finitely many
resources) is shown in NP and coNP by a reduction to mean pay-off games. These results are
described in Chapter 5 of the dissertation.
Text comments
I only have some minr textual comments:
p. 13 (disjunction) it seems that "and" on the right-hand side should be "or"
p. 23 it is unclear whether it is assumed in the SOS-rules for the process algebra of OTS that
processes are considered modulo a structural congruence. The fact that the SOS-rules for
conjunction and disjunction are the same is somewhat puzzling.
p. 48, line 9: there is a reference missing
Language and graphic level
The writing and graphical illustrations of the dissertation are excellent.
Defense questions
1. The motivation behing the introdcution of PMTSs (p. 18) are three undesirable
implementations of a sample MTS specification. What evidence do you have that PMTS
do not suffer from similar deficiencies, i.e., can we not come upo with PMTSs that have
J
"undesirable" implementations as well?
2. Can you explain the SOS-rules of the process algebra for OTS (p. 23), in particular
whether you implicitly assume a structural congruence, and about the rules for
conjunction and disjunction?
3. Can DMTSs be captured by a fragment of H M L (without least fixed points)?, and how
would such fragment look like? Similar questions apply to MTSs.
4. To what extent does the complexity result (Theorem 5.35) depend on the cost measure
considered; that is, what would happen if one considers accumulated costs rather than
long-run average costs, or would use discounting?
5. What is the complexity of checking the absence of Zeno cycles in MTSDs (p. 28)? Is this
indeed just a graph analyis?
6. Any thoughts on model checking timed MTSs against Koymans' metric temporal logic?
Evaluation
To my opinion, Jan Kfetinsky delivered an excellent dissertation with various very strong results
on modal transition systems. The dissertation clearly shows the ability of the candidate to
provide new non-trivial theoretical results.
The dissertation is a pleasure to read and is illustrated with carefully selected examples. The
results of this dissertation have been published at top conferences in the field such as CAV,
A T V A (three times), and CONCUR. The work on deterministic MTSs has been published in the
journal Theoretical Computer Science, whereas the EXPT1ME completeness result appeared in
Information and Computation. This publication record as such is very good. I am impressed by
the fact that besides these publications, Jan Kfetinsky published more than ten other papers
(again mostly at top venues) that are not covered by this dissertation. This is a truly exceptional
output for a PhD student, both in quantitative but also in qualitative terms. Given that these
publications go (far) beyond modal transition systems, it also shows the breadth of Kfetinsky's
research interests.
Jan Kfetinsky also delivered a PhD dissertation at the TU Munich (Germany) on "Verification of
Discrete- and Continuous-Time Non-Deterministic Markovian Systems". As external examiner
of that dissertation, I can confirm that there is no overlap between the two dissertations. That
dissertation completely focused on stochastic systems, whereas the current dissertation is not
covering stochastic aspects at all. It again illustrates the exceptional broad interest of Kfetinsky.
Recommendation
This dissertation is a very strong and valuable piece of work with various excellent scientific
contributions. The author has demonstrated the ability to work independently and creatively in
the specified field. The thesis meets the standard requirements imposed on a dissertation thesis in
the specified field.
Without any reservation, I therefore wholeheartedly recommend to accept this manuscript as a
Ph.D dissertation. Given the exceptional quality of the dissertation, I grade the dissertaion with
grade A, and I adviseto accept the dissertation with distinction.
June 20, 2014
Softwaremodeliierung und Verirtte?
LEHRSTUHL INFORMATIK J?
RWTH Aachen
Ahornstraße 55
Fakulta informatiky
Datum: 2 B ~06-
Č.jVE.č.:
Počet listú dokumentu:....
Počet pffloh s listú/SV,:....
Počet a druh neüsL příloh
J.
J.