Model Counting for Reactive Systems
Model counting is the problem of computing the number of solutions for a logical formula. In the last few years, it has been primarily studied for propositional logic and has been shown to be useful in many applications. In planning, for example, propositional model counting has been used to compute the robustness of a plan in an incomplete domain. In information-flow control, model counting has been applied to measure the amount of information leaked by a security-critical system.
In my thesis, I introduce the model counting problem for linear-time properties and show its applications in formal verification. In the same way propositional model counting generalizes the satisfiability problem for propositional logic, counting models for linear-time properties generalizes the emptiness problem for languages over infinite words to a problem that asks for the number of words in a language. The model counting problem, thus, provides a foundation for quantitative extensions of model checking, where not only the existence of computations that violate the specification is determined, but also the number of such violations.
I solve the model counting problem for the prominent class of omega-regular properties, present algorithms for solving the problem for different classes of properties, and show the advantages of these algorithms in comparison to indirect approaches based on encodings into propositional logic. I further show how model counting can be used for solving a variety of quantitative problems in formal verification, including probabilistic model checking, quantitative information-flow in security-critical systems, and the synthesis of approximate implementations for reactive systems.
Click here for the PDF
Counting Models of Omega-Regular Properties
I introduce four model counting problems for linear-time properties: The infinite trace counting problem, where we count the infinite traces defined by a given linear-time property, and the bounded model counting problems for bad-prefixes, good-prefixes, and lassos, where we compute the number of bad prefixes, good prefixes of bounded length and lassos of bounded size for a linear-time property.
For the prominent subclass of omega-regular properties, I introduce algorithms for solving the model counting problems for properties given as automata over infinite words, and as formulas in linear-time temporal logic (LTL). I introduce automata-based algorithms for each problem as well as symbolic encodings of these problems in propositional logic and give a thorough complexity analysis determining a lower and upper bound for each problem. The complexity analysis is done in terms of both the traditional decision complexity classes and the counting complexity classes.
Model Checking Quantitative Hyperproperties
Hyperproperties define sets of sets of computations and allow us to formalize properties such as information-flow policies and robustness properties of cyber-physical systems. Many interesting quantitative hyperproperties can be formalized as properties that express a bound on the number of traces in the system that may appear in a given relation. For example, in quantitative information-flow policies, we limit the amount of information about certain secret inputs that is leaked through the observable outputs of a system. Quantitative robustness definitions require that the difference in the observed output for similar inputs remains within certain distance.
Quantitative hyperproperties thus set a bound on the number of traces that have the same observable input but different observable output. Although standard algorithms for model checking hyperproperties can be used for model checking quantitative hyperproperties, I showed that using model counting, we only need logarithmic space bounds, which is an exponential or even doubly-exponential improvement (depending on the exact property) over the standard model checking algorithms.
Synthesis of Approximate Implementations
In reactive synthesis, an implementation of a reactive system is automatically constructed from a high-level specification (e.g. in temporal logics). While this idea holds great promise, in that the constructed implementation is inherently correct with respect to the given specification, one of the main hurdles of synthesis is that specifications tend to quickly get unrealizable, i.e., no implementation exists that satisfies the specification. This is due to the requirement that a system must satisfy its specification on all possible environment behaviors, which is in most cases not possible.
In my thesis, I presented algorithms for synthesizing approximate implementations for reactive systems. The approximation is based on fulfilling the specification for restricted environment behavior. The synthesis problem is thus transformed into an optimization problem, where we search for an implementation that fulfills the specification over a maximum number of environment inputs.
The algorithms I developed use an underlying model counting engine to compute the number of these inputs.
Dr.-Eduard-Martin Dissertation Award
For my thesis I received the Dr.-Eduard-Martin Doctoral Dissertation Award granted every year for the best doctoral thesis of each faculty at Saarland University.
My Thesis in 3 Minutes ...
Check out the following short video about the main contributions of my thesis: