Maude-help mailing list

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

On Tuesday 30 August 2005 17:50, 
yfu002 AT cs.fiu.edu
 wrote:
> I'm using maude to verify the system model defined by Petri nets. I just
> notice that there is not past always ([-]) in the modelchecker.maude. So
> my question is how can i check past time LTL formula specified by past
> always ? Thanks in advance.
>
> --Yujian Fu
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help

Maude's model checker does not support past time operators - few model 
checkers do. While past time operators do not add expressive power, ptLTL is 
known to be exponentially more succinct than LTL [1] and I don't know of any 
easy translation.

Steven

[1] Laroussinie et al, Temporal Logic with a forgettable past, LICS 2002.