On learning stochastic models: from theory to practice

Abstract

The field of model checking offers numerous tools for analysing stochastic models. This analysis provides a comprehensive understanding of the behaviours exhibited by the system represented in the model. Consequently, such analyses are of paramount importance for critical systems. Nonetheless, in certain application domains, the model is not readily accessible and needs to be acquired from partially-observable executions of the system under analysis. This thesis proposes to improve the learning of stochastic models, thereby facilitating the application of model checking to systems for which no model is currently available. This objective is realised via three discrete strategies: (i) formulating an active learning algorithm to learn Markov decision processes, (ii) devising a learning algorithm tailored for synchronised compositions of continuous-time Markov chains, and (iii) developing a library compatible with model checkers, streamlining the process of stochastic model acquisition and its seamless incorporation into the model checking procedure. The first two strategies focus on enhancing and extending the theoretical foundations of learning stochastic models, while the third one centers on facilitating the application of learning stochastic models and their integration into the model checking workflow.

Fagsviðið sem fjallar um könnun líkana býður upp á margs konar tól til að kanna líkindafræðileg líkön. Slíkar kannanir skapa gagnlegt innsæi í hegðun þess kerfis sem líkanið lýsir. Slíkar greiningar eru sérlega mikilvægar fyrir krítísk kerfi. Þrátt fyrir þetta er í mörgum tilfellum ekki auðvelt að fá aðgang að slíkum líkönum og því þörf á að geta skapað þau frá grunni með því að keyra kerfin og safna þeim upplýsingum sem eru aðgengilegar. Þessi ritgerð býður upp á leiðir til að læra líkindafræðileg líkön og á þann hátt gera það mögulegt að nota þessa aðferðafræði í tilfellum þar sem engin líkön hafa verið til fram að þessu. Þetta felur í sér eftirfarandi þrjár nálganir: (i) Að setja fram virkt reiknirit til að læra Markov ákvörðunarferli (ii) Að setja fram lærdómsreiknirit fyrir samstillta samsetningu á Markov-keðjum með samfelldan tíma, og (iii) að þróa hugbúnaðarkerfi sem er samhæft helstu kerfum sem sjá um könnun líkana og gera þannig allt ferlið meira straumlínulagað. Fyrstu tvær aðferðirnar miða fyrst og fremst að því að efla fræðilegan bakgrunn fyrir lærdómsreiknirit sem læra líkindafræðileg líkön en markmið hins þriðja gengur út á að bjóða upp á hugbúnað sem bætir almennt flæðið í lærdóms- og könnunarferlinu.