maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [Maude-help] Strategy language for Maude

From: Steven Eker <eker AT csl.sri.com>
To: maude-help AT cs.uiuc.edu
Cc: hamza merouani <merouanihamza AT yahoo.fr>, Maude-users AT cs.uiuc.edu
Subject: Re: [Maude-help] Strategy language for Maude
Date: Mon, 29 Mar 2010 10:20:05 -0700
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
List-id: <maude-help.cs.uiuc.edu>

On Saturday 27 March 2010, hamza merouani wrote:
> Hi;
> I work on the modelling of BPEL processes using Maude Strategy language,
> and I would like to use model-checking toverifysome properties. I was
> hoping to know if Maude Strategy language support LTL model-checker .
> Thinks.
>

The model checker does not support the strategy language. Model checking in
the presence of strategies is an interesting research problem but currently
the model checker using the standard double depth-first search algorithm for
finding cycles in the product automaton.

Steven

[Maude-help] Strategy language for Maude, hamza merouani, 03/27/2010
- Re: [Maude-help] Strategy language for Maude, Steven Eker, 03/29/2010