Home // ICSEA 2019, The Fourteenth International Conference on Software Engineering Advances // View article

From a Subset of LTL Formula to Büchi Automata

Authors:
Bilal Kanso
Ali Kansou

Keywords: Linear Temporal Logic; Buchi automata; Model checking; Compositional modeling.

Abstract:
We present a fragment of Linear Temporal Logic (LTL) together with an polynomial translation of formula from this LTL fragment into equivalent B¨uchi automata. The translation is completely implemented based on Java Pluging Framework in GOAL Tool as a plugin. The implementation is mainly based on pre-proven theorems such that the transformation works very efficiently. In particular, it runs in polynomial space in terms of the length of the given formula. The main application of this transformation could be in model checking area which consists in obtaining a B¨uchi automaton that is equivalent to the software system specification and another one that is equivalent to the negation of the property. The intersection of the two B¨uchi automata is empty if the model satisfies the property. Furthermore, the experiments are performed with three sets of LTL formula, which is commonly used in the literature and the result shows that our proposed LTL fragment covers most of them.

Pages: 61 to 67

Copyright: Copyright (c) IARIA, 2019

Publication date: November 24, 2019

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-752-8

Location: Valencia, Spain

Dates: from November 24, 2019 to November 28, 2019