Advertisement
Published in:
2009 | OriginalPaper | Chapter
On-the-fly Emptiness Check of Transition-Based Streett Automata
Authors : Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur
Published in: Automated Technology for Verification and Analysis
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
In the automata theoretic approach to model checking, checking a state-space
S
against a linear-time property
ϕ
can be done in O(|
S
|×2
O(|
ϕ
|)
) time. When model checking under
n
strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes O(|
S
|×2
O(|
ϕ
| +
n
)
).
Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under
n
strong fairness hypotheses in O(|
S
|×2
O(|
ϕ
|)
×
n
). We focus on transition-based Streett automata, because it allows us to express strong fairness hypotheses by injecting Streett acceptance conditions into the state-space without any blowup.