Learning Markov Decision Processes for Model Checking

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

Abstrakt

Constructing an accurate system model for formal model verification can be both resource demanding
and time-consuming. To alleviate this shortcoming, algorithms have been proposed for automatically
learning system models based on observed system behaviors. In this paper we extend the algorithm
on learning probabilistic automata to reactive systems, where the observed system behavior is in
the form of alternating sequences of inputs and outputs. We propose an algorithm for automatically
learning a deterministic labeled Markov decision process model from the observed behavior of a
reactive system. The proposed learning algorithm is adapted from algorithms for learning deterministic
probabilistic finite automata, and extended to include both probabilistic and nondeterministic transitions.
The algorithm is empirically analyzed and evaluated by learning system models of slot machines. The
evaluation is performed by analyzing the probabilistic linear temporal logic properties of the system
as well as by analyzing the schedulers, in particular the optimal schedulers, induced by the learned
models.
OriginalsprogEngelsk
TidsskriftElectronic Proceedings in Theoretical Computer Science
Vol/bind103
Sider (fra-til)49-63
ISSN2075-2180
DOI
StatusUdgivet - 2012
BegivenhedQuantities in formal methods - Paris, Frankrig
Varighed: 28 aug. 201228 aug. 2012
Konferencens nummer: 1

Workshop

WorkshopQuantities in formal methods
Nummer1
LandFrankrig
ByParis
Periode28/08/201228/08/2012

Fingeraftryk Dyk ned i forskningsemnerne om 'Learning Markov Decision Processes for Model Checking'. Sammen danner de et unikt fingeraftryk.

Citationsformater