3vLTL: a tool to generate automata for three-valued LTL
File(s)2311.09787v1.pdf (643.25 KB)
Published version
Author(s)
Belardinelli, Francesco
Ferrando, Angelo
Malvone, Vadim
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.
Date Issued
2023-11-16
Date Acceptance
2023-11-15
Citation
Electronic Proceedings in Theoretical Computer Science, 2023, 395, pp.180-187
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.
This work is licensed under the
Creative Commons Attribution License.
License URL
Identifier
http://dx.doi.org/10.4204/eptcs.395.13
Source
Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023)
Publication Status
Published
Start Date
2023-11-15
Finish Date
2023-11-16
Coverage Spatial
Scheltema Leiden
Date Publish Online
2023-11-16