NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Efficient Translation of LTL Formulae into Buchi AutomataModel checking is a fully automated technique for checking that a system satisfies a set of required properties. With explicit-state model checkers, properties are typically defined in linear-time temporal logic (LTL), and are translated into B chi automata in order to be checked. This report presents how we have combined and improved existing techniques to obtain an efficient LTL to B chi automata translator. In particular, we optimize the core of existing tableau-based approaches to generate significantly smaller automata. Our approach has been implemented and is being released as part of the Java PathFinder software (JPF), an explicit state model checker under development at the NASA Ames Research Center.
Document ID
20030064048
Document Type
Other
Authors
Giannakopoulou, Dimitra (Research Inst. for Advanced Computer Science Moffett Field, CA, United States)
Lerda, Flavio (Carnegie-Mellon Univ. Pittsburgh, PA, United States)
Date Acquired
August 21, 2013
Publication Date
June 1, 2001
Subject Category
Computer Programming and Software
Report/Patent Number
RIACS-TR-01.29
Funding Number(s)
CONTRACT_GRANT: NCC2-1006
Distribution Limits
Public
Copyright
Public Use Permitted.
Document Inquiry