http://iet.metastore.ingenta.com
1887

LTL transformation modulo positive transitions

LTL transformation modulo positive transitions

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IET Computers & Digital Techniques — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

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)
      • A. Pnueli .
        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.
        . 18th Annual Symp. Foundations of Computer Science , 46 - 57
    2. 2)
      • E.A. Emerson , J.Y. Halpern .
        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.
        . J. Comput. Syst. Sci. , 1 , 1 - 24
    3. 3)
      • M.Y. Vardi .
        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.
        . 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 , 1 - 22
    4. 4)
      • A. Duret-Lutz , D. Poitrenaud .
        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.
        . 12th Int. Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004) , 76 - 83
    5. 5)
      • A. Duret-Lutz .
        5. Duret-Lutz, A.: ‘LTL translation improvements in spot 1.0’, Int. J. Critical Comput.-Based Syst., 2014, 5, (1/2), pp. 3154.
        . Int. J. Critical Comput.-Based Syst. , 31 - 54
    6. 6)
      • N. Pippenger . (1997)
        6. Pippenger, N.: ‘Theories of computability’ (Cambridge University Press, 1997).
        .
    7. 7)
      • P. Gastin , D. Oddoux .
        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.
        . 13th Int. Conf. Computer Aided Verification, CAV 2001 , 53 - 65
    8. 8)
      • G.J. Holzmann .
        8. Holzmann, G.J.: ‘The model checker SPIN’, IEEE Trans. Software Eng., 1997, 23, (5), pp. 279295.
        . IEEE Trans. Software Eng. , 5 , 279 - 295
    9. 9)
      • T. Babiak , M. Kretínský , V. Rehák .
        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.
        . 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 , 95 - 109
    10. 10)
      • T. Babiak , T. Badie , A. Duret-Lutz .
        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.
        . 20th Int. Symp. Model Checking Software, SPIN 2013 , 81 - 98
    11. 11)
      • M.Y. Vardi .
        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.
        . Proc. 8th Int. Conf. Verification, Model Checking, and Abstract Interpretation, VMCAI 2007 , 137 - 150
    12. 12)
      • M.Y. Vardi , T. Wilke .
        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.
        . Logic and Automata: History and Perspectives, Texts in Logic and Games , 629 - 736
    13. 13)
      • J.R. Büchi .
        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.
        . Proc. Int. Congress on Logic, Method, and Philosophy of Science , 1 - 12
    14. 14)
      • H. Tauriainen , K. Heljanko .
        14. Tauriainen, H., Heljanko, K.: ‘Testing LTL formula translation into Büchi automata’, Softw. Tools Technol Transfer, 2002, 4, (1), pp. 5770.
        . Softw. Tools Technol Transfer , 1 , 57 - 70
    15. 15)
      • K.Y. Rozier , M.Y. Vardi .
        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.
        . Proc. 14th Int. SPIN Workshop on Model Checking Software , 149 - 167
    16. 16)
      • J. Cichon , A. Czubak , A. Jasinski .
        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.
        . Fourth Int. Conf. on Dependability of Computer Systems, DepCos-RELCOMEX ‘09 , 17 - 24
    17. 17)
      • J. Couvreur .
        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.
        . FM'99 – Formal Methods, World Congress on Formal Methods in the Development of Computing Systems , 253 - 271
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