3vLTL: A Tool to Generate Automata for Three-valued LTL
This tool addresses a gap in formal verification for multi-valued logics, but it is incremental as it extends existing LTL methods to a three-valued semantics.
The authors tackled the lack of model-checking tools for multi-valued specification languages by developing 3vLTL, a tool that generates Buchi automata from three-valued LTL formulas, enabling formal verification to check if formulas are true, false, or undefined on models.
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.