Approximate LTL Model Counting
Jennifer Niederländer
We consider the model counting problem of linear-time temporal logic (LTL). LTL is a well known specification logic and a standard input language for model checking and synthesis tools of reactive systems. The LTL model counting problem distinguishes two types of models: word and tree models. Word models are labeled sequences that satisfy the formula and are bounded in length. Counting word models can be used in verification to compute the number of errors in an implementation. Tree models are labeled trees that are bounded by depth where each path satisfies the formula. Counting tree models can be seen as a quantitative extension of synthesis in which we determine the number of implementations that satisfy the formula. Unfortunately, the best counting algorithms we know has double exponential complexity in the formula for word models and threefold exponential complexity in the formula for tree models. Although this algorithm improves the naive solution in terms of complexity in the bound, both solutions are impractical and are mostly limited to formulas of small length. In this thesis, we investigate approximative algorithms that efficiently solve the LTL counting problem. We present two main techniques, namely a technique based on the ideas of bounded model checking, where both the model and the LTL formula are transformed into a SAT formula, and another technique based on Monte Carlo methods, where we compute a set of possible solutions and determine proper lower and upper bounds.
Bachelor Thesis.