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.
