A Better Translation From LTL to Transition-Based Generalized Büchi Automata | Zendy

Weiwei Li | Zendy; Shuanglong Kan | Zendy; Zhiqiu Huang | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Better Translation From LTL to Transition-Based Generalized Büchi Automata

Author(s) -

Weiwei Li,

Shuanglong Kan,

Zhiqiu Huang

Publication year - 2017

Publication title -

ieee access

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.587

H-Index - 127

ISSN - 2169-3536

DOI - 10.1109/access.2017.2773123

Subject(s) - aerospace , bioengineering , communication, networking and broadcast technologies , components, circuits, devices and systems , computing and processing , engineered materials, dielectrics and plasmas , engineering profession , fields, waves and electromagnetics , general topics for engineers , geoscience , nuclear engineering , photonics and electrooptics , power, energy and industry applications , robotics and control systems , signal processing and analysis , transportation

Translating linear temporal logic (LTL) formulas into Büchi automata is one of the most important aspects of LTL model checking. Certain successful algorithms, such as LTL2BA and SPOT, first translate an LTL formula into a transition-based generalized Büchi automaton (TGBA) and then degeneralize it into a Büchi automaton. This paper focuses on achieving a better translation from LTL to TGBA and analyzing the performance of every step of the algorithm. We decompose the translation into three steps to give a step-wise description and improve all three steps. The first step is the basic translation without acceptance conditions and simplifications, which combines the advantages of both LTL2BA and SPOT. Second, we introduce a new definition of acceptance conditions. Our proofs and experiments have shown that our technique is more efficient and improves the degeneralization ability. Finally, we introduce the simplifications of our algorithm. We focus on not only producing better final Büchi automata but also minimizing intermediate automata, which can reduce the execution time.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research