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

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 at some time ("finally") a(x,y) holds and then starting from the neXt
state, b(x) does *not* hold until at some point in time b(x) holds but not
c(y).

The problem here is obviously that b(x) occurs both negated and "plain"
within the formula. A tracematch can only kind of negate by using symbols
with do not occur in the pattern.

My first try would be to define a new symbol b'(x), which is a copy of b(x)
but does not occur in the pattern. This would however lead to the
interesting fact that if say b(1) happens on a trace, this would be matched
by two symbols, b(x) and b'(x), meaning it would lead to a "b" and a "skip"
transition at the same time.

Assuming that this is however still behaving in the intended way, the second
complication is that c(y) should *not* hold when b(x) occurs. So how can we
express that? We *cannot* simply declare a symbol c(y) and not include it in
the pattern, because for instance the trace "a(1,2) c(2) b(1)" is legal,
meaning it *should* be matched. Hence, c(y) is generally allowed, but not
when the b(x) occurs.
Also one cannot declare a combined symbol "b(x) /\ !c(y)" because this
would bind y under negation which is not allowed.

Are you seeing any solution to this?

Thanks,
Eric

P.S. Are IRC conversations logged somewhere on server-side so that one can
look up previous discussions?

--
Eric Bodden
Chair I2 for Programming Languages and Program Analysis
RWTH Aachen University