New Results of Membership Problems for Trace Languages

In dynamic analysis of programs, one observes an execution (sequence of events) and checks whether the execution satisfies or violates some property. When the programs are concurrent, such a simple check is often not robust to nondeterministic thread scheduling. In this case, the more appropriate question is the predictive version: given an execution, is there a semantically equivalent execution that satisfies or violates the property of interest. In concurrency theory, when equivalence is characterised by Mazurkiewicz traces, the corresponding question is called membership problem for trace language (MPTL). In 1989, A. Bertoni, G. Mauri, and N. Sabadini showed that MPTL can be solved in time O(n^\alpha) when the property is described using a regular language; n is the size of the execution (or string) and \alpha describes the width of the concurrency relation. We show that, in fact, this problem cannot be solved in better time by showing matching (conditional) lower bound of \Omega(n^\alpha) under the Strong Exponential Time Hypothesis. This result applies to even star-free regular languages. Motivated by practical applicability of runtime monitoring in a predictive setting, we propose a class of languages, called pattern languages, for which MPTL can be solved in constant space and linear time, in other words, using a DFA. Pattern languages essentially encode the existence of a subsequence: for every Pattern language L, there is finite string u such that every member string w in L has u as a subsequence. Pattern languages is a subclass of star-free regular languages and is closed under union, intersection, concatenation, and Kleene star. Contributed talk given by Zhendong Ang

Authors

• Zhendong Ang

Keywords

No keywords are indexed for this paper.