A fast transition of linear temporal logic formulae to transition-based Büchi automata
by Laixiang Shan; Zheng Qin
International Journal of Computer Applications in Technology (IJCAT), Vol. 53, No. 1, 2016

Abstract: This paper presents an algorithm based on revised tableau rules, which converts linear temporal logic formulae to transition-based Büchi automata more efficiently. The algorithm is geared towards being used in model checking in on-the-fly fashion. The algorithm circumvents the intermediate steps and the simplification process that follows, and therefore performs more efficiently. By attaching the satisfaction information of the infinite sequence on states and transitions, we can judge whether the runs of the automata are acceptable by using only one acceptance condition set, but not multiple ones. On-the-fly simplifications as well as binary decision diagram presentation are adopted in the algorithm to gain significant reduction both on the size of product automata and on the computational complexity. It can expand the state nodes while detecting the validity of these, removing the invalid nodes and combining equivalent states and transitions. By comparative testing with other conversion tools, the algorithm runs faster, with fewer states and transitions of the automaton.

Online publication date: Mon, 14-Dec-2015

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Applications in Technology (IJCAT):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com