2025/03/21 by Alexandre Duret-Lutz, Duret-Lutz, Alexandre, Denis Poitrenaud +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.2503.16891
openalex publication_date 2025/03/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the problem of the verification of an LTL specification φ on a system S given some prior knowledge K, an LTL formula that S is known to satisfy. The automata-theoretic approach to LTL model checking is implemented as an emptiness check of the product S⊗ A¬φ where A¬φ is an automaton for the negation of the property. We propose new operations that simplify an automaton A¬φ given some knowledge automaton AK, to produce an automaton B that can be used instead of A¬φ for more efficient model checking. Our evaluation of these operations on a large benchmark derived from the MCC'22 competition shows that even with simple knowledge, half of the problems can be definitely answered without running an LTL model checker, and the remaining problems can be simplified significantly.