Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • Communities & Collections
  • Research Outputs
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Computing
  4. Computing
  5. 3vLTL: a tool to generate automata for three-valued LTL
 
  • Details
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
URI
http://hdl.handle.net/10044/1/110305
URL
http://dx.doi.org/10.4204/eptcs.395.13
DOI
https://www.dx.doi.org/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.
License URL
https://creativecommons.org/licenses/by/4.0/
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
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback