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

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

Received: 31 Dec 2013
Accepted: 07 May 2014
Published online: 14 Dec 2015 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article