On Matching Concurrent Traces?

Abstract. Concurrent traces are sequences of computational steps where independent steps can be permuted and executed in any order. We study the problem of matching on concurrent traces. We outline a sound and complete algorithm for matching traces with one variable standing for an unknown subtrace. 1 State-Transition Concurrency Computation in a concurrent system results from the interactions of computing units such as threads or agents. One popular approach to modeling concurrent computation views each such agent as being able to perform local transforma-tions on a global state, possibly in parallel. This is the approach embraced by Petri nets [5]. This is also the approach underlying propositional multiset rewrit-ing, which we will now describe in further detail. A multiset rewriting system is determined by a set of rules of the form ã → b̃, where a ̃ and b ̃ are multisets over some support set S. We write “· ” for the empty multiset and “ã, b̃ ” for the union of multisets a ̃ and b̃. Multiset union is associativ