LTL Model-checking in ASAP

I just finished integrating LTL model-checking into ASAP.  This is joint work with Sami Evangelista and Thomas Vestergaard.  Basically, I've made the translation from LTL to a Büchi automaton, Sami made the nested depth-first checker, and Thomas put it together, added a bunch of utility functions, and made the initial integration into ASAP.  After that I cleaned up the integration a bit and added a nifty user-interface for entering LTL formulae.

6 thoughts on “LTL Model-checking in ASAP

  1. Hi Michael,

    could you please tell me when and where your LTL-model checking plugin will be available (if…).

    Many thanks,

    1. Hi Davide,

      I have checked in the source in our repository (see more at here and here). You may or may not need a password to check out the code; I don’t remember.

      If you are interested, I can also look at building a new release of ASAP with the checker (as well as a bunch of optimizations I made subsequently) later this week. You can get releases here, but the latest release is quite old and contains no LTL checker code.


      1. Hi Michael,

        thanks for your answer! I’ve checked in your repository and I’ve been asked for a user/pwd input.
        I am surely interested in a new release (for your info, I’m a Mac user) with checker, it’s very kind of you.

        Best regards,

        1. Hi Michael,

          I hope everything it’s ok now!
          I’m writing to ask you if you’ve had time to prepare the ASAP release with the LTL checker.
          Thank in advance.
          Best regards,

  2. Thanks a lot, Michael!

    I knew what happened at your home…Surely you have had a lot of more important things to do than getting back to me about ASAP !!!

    Good luck and many thanks,

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.