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.

翻译：多值逻辑在系统验证（包括运行时验证）领域具有悠久的传统，然而针对多值规约语言的模型检测工具相对较少。本文介绍工具3vLTL，该工具能够基于三值语义解释的线性时态逻辑（LTL）公式生成Büchi自动机。给定一个LTL公式、一组作为自动机字母表的原子命题以及一个真值，本程序可生成一个Büchi自动机，该自动机接受所有将所选真值赋予该LTL公式的词。鉴于该工具输出的特定类型，其可无缝地以自然方式被第三方库处理。换言之，所生成的Büchi自动机能够用于形式化验证场景，以检验给定模型上LTL公式的真、假或未定义状态。