Transformation from PLTL to automata via NFGs

Cong Tian (), Zhenhua Duan () and Mengfei Yang
Additional contact information
Cong Tian: Xidian University
Zhenhua Duan: Xidian University
Mengfei Yang: China Academy of Space Technology

Journal of Combinatorial Optimization, 2015, vol. 29, issue 2, No 5, 406-417

Abstract: Abstract A new linear transformation from PLTL formulas to alternating automata is proposed in this paper. To this end, C-F normal forms and normal form graphs (NFGs) are defined for PLTL formulas. Further, based on NFGs, generalized alternating Büchi automata (GABA) of PLTL formulas are built. Beside the conciseness in theoretical aspect, the new transformation is useful in improving the scalability of LTL model checking tools in practise. Also, based on the new transformation, an intuitive on-the-fly model checking approach can be implemented.

Keywords: LTL; Automata; Model checking; Satisfiability; Verification (search for similar items in EconPapers)
Date: 2015
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10878-013-9601-4 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jcomop:v:29:y:2015:i:2:d:10.1007_s10878-013-9601-4

Ordering information: This journal article can be ordered from
https://www.springer.com/journal/10878

DOI: 10.1007/s10878-013-9601-4

Access Statistics for this article

Journal of Combinatorial Optimization is currently edited by Thai, My T.

More articles in Journal of Combinatorial Optimization from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().