Altmetric

3vLTL: a tool to generate automata for three-valued LTL

File Description SizeFormat 
2311.09787v1.pdfPublished version643.25 kBAdobe PDFView/Open
Title: 3vLTL: a tool to generate automata for three-valued LTL
Authors: Belardinelli, F
Ferrando, A
Malvone, V
Item Type: Conference Paper
Abstract: 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.
Issue Date: 16-Nov-2023
Date of Acceptance: 15-Nov-2023
URI: http://hdl.handle.net/10044/1/110305
DOI: 10.4204/eptcs.395.13
ISSN: 2075-2180
Publisher: Open Publishing Association
Start Page: 180
End Page: 187
Journal / Book Title: Electronic Proceedings in Theoretical Computer Science
Volume: 395
Copyright Statement: © F. Belardinelli, A. Ferrando & V. Malvone This work is licensed under the Creative Commons Attribution License.
Conference Name: Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023)
Publication Status: Published
Start Date: 2023-11-15
Finish Date: 2023-11-16
Conference Place: Scheltema Leiden
Online Publication Date: 2023-11-16
Appears in Collections:Computing



This item is licensed under a Creative Commons License Creative Commons