By April 5, 2010 6 Comments Read More →

LTL Model-checking in ASAP

This post has 140 words. Reading it will take less than one minute.

GD Star Rating
loading...

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.

With no further ado, check out the video below.  If it’s loading too slowly (or my flash-video thingy is still borked), try using the Youtube versions below (despite being unlovingly chopped over and in crappy quality).

Posted in: Uncategorized

6 Comments on "LTL Model-checking in ASAP"

Trackback | Comments RSS Feed

  1. Davide says:
    April 27, 2010 at 15:07
    GD Star Rating
    loading...

    Hi Michael,

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

    Many thanks,
    Davide

    Reply
    • Michael says:
      April 27, 2010 at 20:46
      GD Star Rating
      loading...

      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.

      Regards,
      Michael

      Reply
      • Davide says:
        April 27, 2010 at 22:16
        GD Star Rating
        loading...

        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,
        Davide

        Reply
        • Davide says:
          June 13, 2010 at 16:33
          GD Star Rating
          loading...

          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,
          Davide

          Reply
  2. Davide says:
    June 13, 2010 at 18:48
    GD Star Rating
    loading...

    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,
    Davide

    Reply

Post a Comment