Model Checking for the Analysis and Control of Complex and Non-deterministic Systems

In the last two decades, the use of intelligent planning algorithms, complex controllers,and automated verification processes is growing apace, having a great impact in many industrial fields, as robotics, manufacturing processes, and embedded systems, which now are present in an increasing number of everyday products and appliances. Moreover, many processes take place in an environment having variable and unpredictable influences on the system dynamics, making the problem of dealing with these non-deterministic behaviours a very significant concern. As a result, a growing synergy between Control and AI Planning communities has been established, with the aim to develop algorithms and tools able to cope with such systems. In particular, it is interesting to evaluate robustness, verify the correctness and compute plans to execute activities. To this aim, formal methods (and in particular model checking) are well-suited to deal with these issues. For several years, both control and planning problems have been addressed only through symbolic model checking, which has been successfully applied to a wide class of systems. Nevertheless, there are still some open issues in dealing with Discrete Time Hybrid Systems (DTHS), whose state description involves both continuous and discrete variables, as well as systems with a complex nonlinear dynamics, for which symbolic approaches are hard to apply. To this regard, we focus on the use of explicit model checking, which is based on the explicit enumeration of the system states, to deal with control and planning problems in both deterministic and non-deterministic domains. Nevertheless, the explicit approach is strongly affected by the so called state explosion problem. In order to mitigate this problem, a first contribution is the developing of a disk-based algorithm for the UPMurphi tool: a universal planner for continuous domains built on top of the Murphi model checker. We exploit the use of disk-based approach to analyse and control systems having a huge state space, showing a number of benchmarks and real world planning and control case studies. Moreover, we extend the use model checking to database data quality problems, using formal methods for the verification of data consistency defined over a set of data items, and evaluating the results on a real application of a Public Administration database provided by the C.R.I.S.P. research centre. Finally, we tackle with non-deterministic systems in which an action may have different outcomes, unpredictable at planning time, addressing the problem to synthesise a plan able to reach a goal in spite of the non-determinism, i.e., strong plan. Many approaches have been applied in literature, mainly based on symbolic model checking. As a novel contribution, we present an algorithm able to synthesise strong plans (if any) with minimum cost with respect to a given cost function (that is minimising the non-deterministic worst-case execution), analysing its complexity, correctness and completeness. Finally, we describe the implementation of the algorithm into UPMurphi and we test it on two continuous non-deterministic case studies.