Advertisement
Published in:
2015 | OriginalPaper | Chapter
Single-Pass Testing Automata for LTL Model Checking
Author : Ala Eddine Ben Salem
Published in: Language and Automata Theory and Applications
Publisher: Springer International Publishing
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
Testing Automaton
(TA) is a new kind of
$$\omega $$
-automaton introduced by Hansen et al. [
6
] as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen [
5
] shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach.
This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called
Single-pass Testing Automaton
(STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the BA and TA approaches. These experiments show that STA compete well on our examples.