要約
多値ロジックは、実行時検証を含むシステム検証に関する文献において長い伝統があります。
ただし、多値仕様言語用に開発されたモデル チェック ツールは比較的少数です。
3vLTL は、3 値のセマンティクスに基づいて解釈された線形時間時論理 (LTL) の数式から Buchi オートマトンを生成するツールです。
LTL 式、オートマトンのアルファベットとしての原子命題のセット、および真理値が与えられると、私たちの手順は、選択された真理値を LTL 式に割り当てるすべての単語を受け入れる Buchi オートマトンを生成します。
ツールの出力の特定の種類を考慮すると、サードパーティのライブラリによって自然な方法でシームレスに処理することもできます。
つまり、Buchi オートマトンを形式検証のコンテキストで使用して、特定のモデルで LTL 式が真、偽、または未定義であるかどうかを確認できます。
要約(オリジナル)
Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present 3vLTL, a tool to generate Buchi automata from formulas in Linear-time Temporal Logic (LTL) interpreted on a three-valued semantics. Given an LTL formula, a set of atomic propositions as the alphabet for the automaton, and a truth value, our procedure generates a Buchi automaton that accepts all the words that assign the chosen truth value to the LTL formula. Given the particular type of the output of the tool, it can also be seamlessly processed by third-party libraries in a natural way. That is, the Buchi automaton can then be used in the context of formal verification to check whether an LTL formula is true, false, or undefined on a given model.
arxiv情報
| 著者 | Francesco Belardinelli,Angelo Ferrando,Vadim Malvone |
| 発行日 | 2023-11-16 11:04:38+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google