PROBABILISTIC MODEL CHECKING WITH MARKOV MODELS SEMANTICS: NEW DEVELOPMENTS AND APPLICATIONS

Contemporary society is increasingly dependent on the use of autonomous computational systems. Being sure that these systems behave appropriately and do what they have been designed for is thus fundamental. Several techniques have been developed to this purpose. Among them, model checking includes a series of methods that make use of computa- tional logic and automatic procedures to check whether systems’ behaviour satisfies given desirable properties. In recent years, due to the increasing prevalence of stochastic models, conventional model checking techniques have proven inadequate. The consequence has been the devel- opment of probabilistic model checking, a new research program aimed at developing proper tools to check the behaviour of stochastic systems. Among others, the probabilistic model checking with Markov models semantics and its related languages (i.e., the Probabilistic Computation Tree Logic (PCTL) and its extensions) has been particularly successful and is nowadays applied throughout a variety of different systems and domains. Nevertheless, there remain numerous unexplored developments and applications in this field. In this doctoral dissertation, we specifically concentrate on three such aspects that hold signifi- cant relevance to contemporary AI research. To each of these aspect, we will dedicate a chapter. The dissertation is structured as follows. In the first chapter, we present the essential foundational information regarding prob- ability theory and Markov models. Initially, we introduce fundamental terminology and refresh the reader’s memory on the significant philosophical interpretations of probability, the Kolmogorov axiomatization, and the associated calculus. Subsequently, we delve into the application of probability in studying stochastic systems. Our primary emphasis is on Markov models, including discrete-time Markov chains, Markov reward models, and Markov decision processes. These models are indeed considered the reference formalism for representing stochastic systems in the domain of model checking. In the second chapter, we provide an overview of the state of the art of model check- ing, with a particular emphasis on both single-agent and multi-agents probabilistic model checking. In the opening section, we discuss the fundamental ideas of the program verifica- tion research field, of which model checking represents one of the contemporary evolutions. We focus in particular on the philosophical debate that emerged in the 1980s between 3 4 advocates and opponents of formal methods in computer science. This debate can be considered a pivotal milestone in the shift from traditional program verification methods to modern techniques such as model checking. In the subsequent sections, we then introduce various formalisms utilized in model checking for representing computational systems, specifying their attributes, and verifying their behaviors. For standard (non probabilistic) model checking, these formalisms include transition systems and their related logical languages (i.e., LTL and CTL), while for prob- abilistic model checking they include Markov models and the related language PCTL. We conclude the chapter by examining some recent extensions of probabilistic model checking suitable for the analysis of epistemic and probabilistic properties of stochastic multi-agent systems. Notably, the formalisms we consider include the logics CTLK [113], PCTLK [175], and COGWED [28], where the latter two formalisms will serve as the foundation for subsequent advancements and applications discussed in the remaining chapters of the dissertation. In the third chapter, we explore a potential connection between probabilistic model- checking and eXplainable AI (XAI), a recently-born field of research a