Michał Knapik, PhD

The aim of the project was to develop some enhanced methods of automated verification of finite-state real-time systems performed by the analysis of their models, i.e., of the model checking. This task is of highly practical value, in particular, for the verification of safety critical systems. The essence of the developed approach consists in methods of the synthesis of the parameters values of complex systems under which the desired properties of these systems are secured.

The results obtained belong to two groups. The first one concerns systems where the time is not considered explicitly. Instead, only the temporal order of the events is taken into account. In such a case, the models are relatively simple and take form of, e.g., Kripke structures, the worlds of which correspond to the possible states. In practice, some compressed representations of such structures are used instead of the original graphs. In particular, Binary Decision Diagrams (BDD) provide such a very effective representation. The research in the project along these lines was carried out using three temporal logics, Action-Restricted Computation Tree Logic (ARCTL), Computation Tree Logic with Knowledge (CTLK) and Alternating-time Temporal Logic (ATL), which have been extended with parameters. For example, the standard ARCTL logic allows to express the properties of type: "All runs of the system in which only actions from the given set A are used end up in a safe state". Extending this logic with parameters allows for example to replace the given set A with a free variable X. The goal of the parameter synthesis is therefore to find all the sets of actions B such that the property holds when X is substituted with B. The algorithms for the synthesis for these logics extended with parameters primarily boil down to proposing appropriate fixed point methods that operate on sets of functions rather than on sets of states.

The second group of the results, concerning systems with explicit time modelling, may be further divided into methods dealing with, respectively, a discrete and continuous time representation. Again, the approaches have been proposed making it possible to introduce parameters, but this time not to the underlying logics but to the models under consideration. In case of the discrete time, a theory for the synthesis of parameters for the properties expressible in a version of the  Real-Time Computation Tree Logic (RTCTL) has been developed. In case of the continuous time modelling, some methods of the limited parametric model verification have been developed due to the known difficulty in proving even simple properties for the parametric temporal automata.

The methods developed in the framework of the project have been experimentally shown to be much more effective than the brute-force approach.

The results has been published in many papers (cf., here).

A number of software tools implementing proposed approaches to model checking has been implemented (cf., e.g., the SPATULA system and the pta2smt system).

You are here: Home Results Michał Knapik, PhD