Re: [abc] Tracematch-Question: Symbols both negated and unnegated

Eric Bodden wrote:

>>Hello.
>>
>>Yesterday I read through your TM paper again and tried to compare your Regex
>>implementation and our LTL implementation on a *formal* level (meaning on
>>the level of recognizable languages).
>>
>>I was wondering, how one could right a tracematch, which is equivalent to
>>the following LTL formula:
>>
>>Given symbols a(x), b(x) and c(x) (all exposing some object "x") assume the
>>formula:
>>F(a(x,y) /\ X( !b(x) U ( b(x) /\ !c(y) ) ) )
>>
>>
>
>
So does a() bind one or two objects?

Correct me if I'm wrong, but it seems to me that the regular pattern "a
c* b" would be equivalent to the above, provided that b() and c() are
disjoint. (If there are events matched by both b() and c(), define
symbols b'() := b() && !c() and c'() := c() && !b(), and use the pattern
"a c'* b'".)

>>(...)
>>P.S. Are IRC conversations logged somewhere on server-side so that one can
>>look up previous discussions?
>>
>>
>
>
Yes, check /home/alphabot/logs on musketeer for logs of conversations
that have been observed by Alphabot.

- P
Received on Sun Aug 28 01:40:31 2005