Int. J. of Computer Applications in Technology   »   2016 Vol.53, No.1

 

 

You can view the full text of this article for Free access using the link below.

 

 

Title: A fast transition of linear temporal logic formulae to transition-based Büchi automata

 

Authors: Laixiang Shan; Zheng Qin

 

Addresses:
Department of Computer Science and Technology, Tsinghua University, Beijing, 100084, China
Department of Computer Science and Technology, Tsinghua University, Beijing, 100084, China

 

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.

 

Keywords: Büchi automata; linear temporal logic; satisfied information; binary decision diagram; model checking; Buechi automata.

 

DOI: 10.1504/IJCAT.2016.073603

 

Int. J. of Computer Applications in Technology, 2016 Vol.53, No.1, pp.62 - 70

 

Available online: 13 Dec 2015

 

 

Editors Full text accessFree access Free accessComment on this article