Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Abdur,

No, the same general algorithm is used:

(1) The formula is negated
(2) It is then simplified and converted to standard form using Maude equations
(3) The standard form is converted to a very weakly alternating automaton
(4) The VWAA is optimized
(5) The VWAA is converted to a generalized Buchi automaton
(6) The GBA is optimized
(7) The GBA is converted into a regular Buchi automaton
(8) The BA is optimized
(9) The standard double depth first search method is used to compute and 
search 
the synchronous product of the optimized BA and the state transition graph of 
the specification being checked, on the fly;  with a reachable accepting 
cycle 
corresponding to a counter-example.

The reason for all of this rigmarole is that LTL model-checking is P-space 
hard and elaborate techniques are needed to avoid blowing up on quite trivial 
examples. One upshot is that there is no easily understood correspondence 
between the formula you start with and the Buchi automaton that ends up being 
used to compute the synchronous product. And thus a small change in the 
formula, say changing an "eventually" operator to a "next" operator can lead 
to a big change in the runtime. 

The techniques used in Maude were state of the art in 2001 when the model 
checker was implemented but I'm sure much theoretical progress has been made 
in the intervening decade and so there may be room for practical 
improvement... but I wouldn't hold your breath.

Steven

On Tuesday 29 March 2011 04:10:26 am 
rza AT cs.nott.ac.uk
 wrote:
> 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 mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>