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.