Altmetric
3vLTL: a tool to generate automata for three-valued LTL
File | Description | Size | Format | |
---|---|---|---|---|
2311.09787v1.pdf | Published version | 643.25 kB | Adobe PDF | View/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