Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon free LTL transformation modulo positive transitions

In this study, the author presents a new efficient algorithm for translating linear temporal logic (LTL) formulas to Büchi automata, which are used by LTL model checkers. The general idea of this algorithm is to generate Büchi automata from LTL formulas, using the principle of alternating automata and keeping only the positive transitions without generating the intermediate generalised automata. The LTL translation is the heart of any LTL model checker, which affects its performance. The translation performance is measured in addition to its speed and the size of the produced Büchi automaton (number of states and number of transitions), by correctness of produced Büchi automaton and its level of determinism. The author will show that this method is different from the others and it is very competitive with the most efficient translators to date.

References

    1. 1)
      • 10. Babiak, T., Badie, T., Duret-Lutz, A., et al: ‘Compositional approach to suspension and other improvements to LTL translation’. 20th Int. Symp. Model Checking Software, SPIN 2013, Stony Brook, NY, USA, 8–9 July 2013 (LNCS, 7976), pp. 8198.
    2. 2)
      • 13. Büchi, J.R.: ‘On a decision method in restricted second order arithmetic’. Proc. Int. Congress on Logic, Method, and Philosophy of Science, 1962, pp. 112.
    3. 3)
      • 17. Couvreur, J.: ‘On-the-fly verification of linear temporal logic’. FM'99 – Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, 20–24 September 1999 (LNCS, 1708), pp. 253271.
    4. 4)
      • 3. Vardi, M.Y.: ‘Branching vs. linear time: final showdown’. Proc. 7th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, Held as Part of the Joint European Conf. Theory and Practice of Software, ETAPS 2001, Genova, Italy, 2–6 April 2001 (LNCS, 2031), pp. 122.
    5. 5)
      • 7. Gastin, P., Oddoux, D.: ‘Fast LTL to Büchi automata translation’. 13th Int. Conf. Computer Aided Verification, CAV 2001, Paris, France, 18–22 July 2001 (LNCS, 2102), pp. 5365.
    6. 6)
      • 5. Duret-Lutz, A.: ‘LTL translation improvements in spot 1.0’, Int. J. Critical Comput.-Based Syst., 2014, 5, (1/2), pp. 3154.
    7. 7)
      • 9. Babiak, T., Kretínský, M., Rehák, V., et al: ‘LTL to Büchi automata translation: fast and more deterministic’. Proc. 18th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conf. Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24 March–1 April 2012 (LNCS, 7214), pp. 95109, pp. 18.
    8. 8)
      • 8. Holzmann, G.J.: ‘The model checker SPIN’, IEEE Trans. Software Eng., 1997, 23, (5), pp. 279295.
    9. 9)
      • 15. Rozier, K.Y., Vardi, M.Y.: ‘LTL satisfiability checking’. Proc. 14th Int. SPIN Workshop on Model Checking Software, Berlin, Germany, 1–3 July 2007 (LNCS, 4595), pp. 149167.
    10. 10)
      • 2. Emerson, E.A., Halpern, J.Y.: ‘Decision procedures and expressiveness in the temporal logic of branching time’, J. Comput. Syst. Sci., 1985, 30, (1), pp. 124.
    11. 11)
      • 4. Duret-Lutz, A., Poitrenaud, D.: ‘SPOT: an extensible model checking library using transition-based generalized Büchi automata’. 12th Int. Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), Vollendam, The Netherlands, 4–8 October 2004, pp. 7683.
    12. 12)
      • 14. Tauriainen, H., Heljanko, K.: ‘Testing LTL formula translation into Büchi automata’, Softw. Tools Technol Transfer, 2002, 4, (1), pp. 5770.
    13. 13)
      • 11. Vardi, M.Y.: ‘Automata-theoretic model checking revisited’. Proc. 8th Int. Conf. Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, Nice, France, 14–16 January 2007 (LNCS, 4349) pp. 137150.
    14. 14)
      • 12. Vardi, M.Y., Wilke, T.: ‘Automata: from logics to algorithms’. Logic and Automata: History and Perspectives, Texts in Logic and Games, 2008, vol. 2, pp. 629736.
    15. 15)
      • 6. Pippenger, N.: ‘Theories of computability’ (Cambridge University Press, 1997).
    16. 16)
      • 1. Pnueli, A.: ‘The temporal logic of programs’. 18th Annual Symp. Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, pp. 4657.
    17. 17)
      • 16. Cichon, J., Czubak, A., Jasinski, A.: ‘Minimal Büchi automata for certain classes of LTL formulas’. Fourth Int. Conf. on Dependability of Computer Systems, DepCos-RELCOMEX ‘09, Brunow, Poland, 30 June–2 July 2009, pp. 1724.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cdt.2017.0112
Loading

Related content

content/journals/10.1049/iet-cdt.2017.0112
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address