Buchi automata in formal software verification

Question

As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in practice.

Let me recall the mathematical intuition behind model checking using these techniques. Buchi automata are the automata associated to $\omega$-regular languages. You can think of these languages as the infinite version of the regular languages (infinite in the sense that they operate on infinite words). As regular languages, they enjoy closure properties under composition and intersection. It is also well known that these Automata are "isomorphic" to proposition of a logic called S1S. This is the logic of Monadic Second Order Logic (i.e. you can have quantification of on the predicates of the logic, but the elements can ranges over a finite set). S1S has the nice property of being decidable, i.e. for each preposition we can tell if it is true or not. To find if a S1S formula is satisfiable, we can find if the associated atomata has an accepting state. In Buchi automata this is done by finding cycles between the starting state and any final state.

To find a "bug" in a software we proceed like this:

• we formalize our software as $\mathbb{S}$ using a S1S logic (a monaidic second order logic).
• we formalize the security properties of our software in the logic $\mathbb{P}$
• now we use closeness properties of $\omega$-languages, whose associated automata are equivalent to S1S logic: we build Buchi automata of $\overline{\mathbb{S}} \cap \mathbb{P}$

In this way, if the software does not comply to the security properties, the resulting automata will have at least an accepting state. In practice, the accepting state of a Buchi automata can be found by finding a cycle in the associated graph between the starting state and any final state.

I suspect in practice an algorithm for cycle detection cannot be used. This is due to the constraint that the cycle should pass from the only starting state and should pass through an accepting state, so the likelihood of finding the cycle you need might be very low. Anyway, the best algorithm for Cycle detection is solved by the Johnson Algorithm in time $O((n + e)(c + 1))$ and space bounded by $O(n + e)$).

In practice, S1S decidibility using Buchi automata might be best to be solved with s-t connectivity. For instance, NetworkX solves s-t connectivity with this algorithm by Abdol-Hossein Esfahanian.

Am I correct?

Which graph algorithm is used in practice to solve S1S satisfiability using Buchi automata?

I have found this, but it just shows a better reduction from S1S to Buchi, and it doesn't talk about graphs.

Answer 1

A Buchi automaton has a non-empty language if and only if there is an accepting lasso, i.e., a path from an initial state to some lasso starting state $s$, and a loop from $s$ to itself along which an accepting state is reached.

There is a very simple linear-time algorithm for this problem that model checkers such as spin implement. Javier Esparza has a nice slide set on this problem that can be found here. I've never heard of Johnson's Algorithm or s-t connectivity being used to find words accepted by Buchi automata - at the very least, they appear to be much more complicated than the standard solution. You will also find the algorithm in the book "Model Checking" by Clarke, Peled, and Grumberg, as well as the book "Principles of Model Checking" by Baier and Katoen.

Note that S1S is a logic that is quite useful in theory to characterize what can be expressed with Buchi automata. It is possible that by restricting your search to publications and book that mention S1S, you are missing out a lot of research. There is a lot of semi-applied research that does not use S1S, but rather uses logics such as linear temporal logic (LTL) to express properties of programs. The reason that translating from logics such as LTL has a much lower complexity (it is only exponential instead of non-elementary as in the S1S case). So it is much easier to build scaling tools for the translation. For this reason, all practically available mature tools for the translation that I am aware of use a logic other than S1S. While the non-elementariness of the translation does not rule out that there could be tools that are efficient in practice, S1S is also criticized for being quite hard to specify in.

There is another efficiency problem with your approach: You translate the program you want to check to S1S. Now since the translation from there to Buchi automata is non-elementary and programs are typically non-trivially large, you will not be able to use this approach without extremely good translation tools that make use of all kinds of heuristic optimizations. It's much easier to translate the program directly to a Buchi automaton that represents all of its executions and then make the language intersection with the specification on the automaton level. Now you mentioned security properties, and I'm not sure how exactly you would have to adapt this approach to cover meaningful security properties. But for classical reactive system properties (safety, liveness), this is the usual approach.

Answer 2

The fastest theoretical algorithm to solve Büchi Games in game graphs is presented in [1] and runs in $O(n^2)$: The algorithm uses a hierarchical decomposition approach. An easier folklore algorithm with $O(mn)$ running time using just the attractor concept is mentioned.

Büchi Games on graphs should be in linear time after computing the strongly connected components of the graph.

[1] Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition. J. ACM, (2014)