maude-help AT lists.siebelschool.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] LTL model-checking

From: rza AT Cs.Nott.AC.UK
To: maude-help AT cs.uiuc.edu
Subject: [Maude-help] LTL model-checking
Date: 29 Mar 2011 12:10:26 +0100
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
List-id: <maude-help.cs.uiuc.edu>
Source-info: From (or Sender) name not authenticated.

Hi,

can anyone please let me know whether Maude implements different algorithms to verify the following properties? I presume both of them would take same CPU time, but seems not in practice...

[] ( X -> <> Y )

[] ( X -> O Y )

Best,
--Abdur

[Maude-help] LTL model-checking, rza, 03/29/2011
- Re: [Maude-help] LTL model-checking, Steven Eker, 03/29/2011