Simplifying LTL Model Checking Given Prior Knowledge
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908288091684864 |
|---|---|
| author | Duret-Lutz, Alexandre Poitrenaud, Denis Thierry-Mieg, Yann |
| author_facet | Duret-Lutz, Alexandre Poitrenaud, Denis Thierry-Mieg, Yann |
| contents | 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\otimes A_{\lnotφ}$ where $A_{\lnotφ}$ is an automaton for the negation of the property. We propose new operations that simplify an automaton $A_{\lnotφ}$ \emph{given} some knowledge automaton $A_K$, to produce an automaton $B$ that can be used instead of $A_{\lnotφ}$ 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_16891 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Simplifying LTL Model Checking Given Prior Knowledge Duret-Lutz, Alexandre Poitrenaud, Denis Thierry-Mieg, Yann Formal Languages and Automata Theory Logic in Computer Science 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\otimes A_{\lnotφ}$ where $A_{\lnotφ}$ is an automaton for the negation of the property. We propose new operations that simplify an automaton $A_{\lnotφ}$ \emph{given} some knowledge automaton $A_K$, to produce an automaton $B$ that can be used instead of $A_{\lnotφ}$ 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. |
| title | Simplifying LTL Model Checking Given Prior Knowledge |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2503.16891 |