Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties
Henri Hansen, Wojciech Penczek, Antti Valmari · Electronic Notes in Theoretical Computer Science · 2002
The research examines liveness and progress properties of concurrent systems and their on-the-fly verification. An alternative formalism to Büchi automata, called testing automata, is developed. The basic idea of testing automata is to observe changes in the values of state propositions instead of the values. Therefore, the testing automata are able to accept only stuttering-insensitive languages. Testing automata can accept the same stuttering-insensitive languages as (state-labelled) Büchi automata, and they have at most the same number of states. They are also more often deterministic. Moreover, on-the-fly verification using testing automata can often (but not always) use an algorithm performing only one search in the state space, whereas on-the-fly verification with Büchi automata requires two searches. Experimental results illustrating the benefits of testing automata are presented.