IJSEA Archive (Volume 7, Issue 4)
International Journal of Science and Engineering Applications (IJSEA) (Volume 7, Issue 4 April 2018)
EFFICIENT ALGORITHM TO TRANSFORM MINIMALIST SUBSET OF LTL FORMULA INTO FINITE STATE MODELS
Keywords: Linear Temporal Logic, Büchi automata, Model checking, Compositional modelling
The translation of LTL formula into equivalent Büchi automata plays an important role in many algorithms for LTL model checking, which consist in obtaining a Büchi 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üchi automata is empty if the model satisfies the property. Generating the Büchi automaton corresponding to an LTL formula may, in the worst case, be exponential in the size of the formula, making the model checking effort exponential in the size of the original formula. There is no polynomial solution for checking emptiness of the intersection. That comes from the translation step of LTL formula into finite state models. This makes verification methods hard or even impossible to be implemented in practice. In this paper, we propose a subset of LTL formula which can be converted to Büchi automata whose the size is polynomial.
C. Baier and J.P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008.
 E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Formal methods in system design, pages 415-427. Springer-Verlag, 1994.
 E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, April 1986.
 Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999.
 E.W. Dijkstra. An Algol 60 translator for the x1 and Making a translator for Algol 60. Technical Report 35, Mathematisch Centrum, Amsterdam, 1961.
 M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Property specification patterns for finite-state verification. In FMSP, pages 7- 15, 1998.
 M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Programming, pages 411 - 420, 1999.
 P. Gastin and D. Oddoux. Fast LTL to Buchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of LNCS, pages 53- 65, Paris, France, jully 2001. Springer.
 V. King, O. Kupferman, and M.Y. Vardi. On the Complexity of Parity Word Automata, pages 276 -286. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001.
 M. Mukund. Finite-state automata on infinite inputs, 1996.
 A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS '77, pages 46-57, Washington, DC, USA, 1977. IEEE Computer Society.
 J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proceedings of the 5th Colloquium on International Symposium on Programming, pages 337 - 351, London, UK, UK, 1982. Springer-Verlag.
 S. Safra. On the complexity of omega-automata. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 319- 327, 1988.
 S. Safra. Complexity of Automata on Infinite Objects. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, March 1989.
 A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733- 749, july 1985.
 A.P Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. In Automata, Languages and Programming, pages 465 - 474, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg.
 S. Taha, J. Julliand, F. Dadeau, K. Castillos, and B. Kanso. A compositional automata-based semantics and preserving transformation rules for testing property patterns. Formal Asp. Comput., 27(4):641 - 664, 2015.
 M. Y. Vardi and P.Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symp. on Logic in Computer Science, pages 332 - 344, Cambridge, June 1986.
 M.Y. Vardi. Branching vs. linear time: Final showdown. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, pages 1 - 22, London, UK, 2001. Springer-Verlag.
title = " EFFICIENT ALGORITHM TO TRANSFORM MINIMALIST SUBSET OF LTL FORMULA INTO FINITE STATE MODELS ",
journal = "International Journal of Science and Engineering Applications (IJSEA)",
volume = "7",
number = "4",
pages = "054 - 063 ",
year = "2018",
author = " Bilal Kanso, Ali Kansou ",