Advertisement
Published in:
2013 | OriginalPaper | Chapter
Tulip: Model Checking Probabilistic Systems Using Expectation Maximisation Algorithm
Author : Rastislav Lenhardt
Published in: Quantitative Evaluation of Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We describe a novel tool for model checking
ω
-regular specifications on interval Markov chains, recursive interval Markov chains and interval stochastic context-free grammars. The core of the tool is an iterative expectation maximisation procedure to compute values for the unknown probabilities in a parametrised system, which maximises the probability of satisfying the specification. The tool supports specifications given as LTL formulas or unambiguous Büchi automata.