3vLTL: A Tool to Generate Automata for Three-valued LTL

Francesco Belardinelli; Angelo Ferrando; Vadim Malvone

doi:10.4204/EPTCS.395.13

3vLTL: A Tool to Generate Automata for Three-valued LTL

Francesco Belardinelli
, Angelo Ferrando
, Vadim Malvone

Imperial College London
University of Genoa

Research output: Contribution to journal › Conference article › peer-review

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 multivalued specification languages. We present 3vLTL, a tool to generate Büchi 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 Büchi 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 Büchi 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.

Original language	English
Pages (from-to)	180-187
Number of pages	8
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	395
DOIs	https://doi.org/10.4204/EPTCS.395.13
Publication status	Published - 15 Nov 2023
Event	5th International Workshop on Formal Methods for Autonomous Systems, FMAS 2023 - Hybrid, Leiden, Netherlands Duration: 15 Nov 2023 → 16 Nov 2023

Access to Document

10.4204/EPTCS.395.13

Cite this

@article{45dae4378e0a42c4b2a91297722df64a,

title = "3vLTL: A Tool to Generate Automata for Three-valued LTL",

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 multivalued specification languages. We present 3vLTL, a tool to generate B{\"u}chi 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 B{\"u}chi 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 B{\"u}chi 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.",

author = "Francesco Belardinelli and Angelo Ferrando and Vadim Malvone",

note = "Publisher Copyright: {\textcopyright} 2023 Open Publishing Association. All rights reserved.; 5th International Workshop on Formal Methods for Autonomous Systems, FMAS 2023 ; Conference date: 15-11-2023 Through 16-11-2023",

year = "2023",

month = nov,

day = "15",

doi = "10.4204/EPTCS.395.13",

language = "English",

volume = "395",

pages = "180--187",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

}

TY - JOUR

T1 - 3vLTL

T2 - 5th International Workshop on Formal Methods for Autonomous Systems, FMAS 2023

AU - Belardinelli, Francesco

AU - Ferrando, Angelo

AU - Malvone, Vadim

PY - 2023/11/15

Y1 - 2023/11/15

N2 - 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 multivalued specification languages. We present 3vLTL, a tool to generate Büchi 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 Büchi 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 Büchi 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.

AB - 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 multivalued specification languages. We present 3vLTL, a tool to generate Büchi 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 Büchi 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 Büchi 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.

U2 - 10.4204/EPTCS.395.13

DO - 10.4204/EPTCS.395.13

M3 - Conference article

AN - SCOPUS:85179009208

SN - 2075-2180

VL - 395

SP - 180

EP - 187

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

Y2 - 15 November 2023 through 16 November 2023

ER -

3vLTL: A Tool to Generate Automata for Three-valued LTL

Abstract

Access to Document

Fingerprint

Cite this