Matching Trace Patterns with Regular Policies

We consider policies that, are described by regular expressions. finite automata. or formulae of linear temporal topic (LTL). Such policies are assumed to describe situations that, are problematic, and thus should be avoided. Given a trace pattern u, i.e., a sequence of action symbols and variables. were the variables stand for unknown (i.e., not observed) sequences of actions. we disk whether u potentially, violates a given policy L, i.e., whether die variables in u can be replaced by sequences of actions such that: the resulting, trace belongs to L. We also consider the dual case where the regular policy L is supposed to describe all the situations. Here, we want to know whether u always adheres to the given policy L, i.e.. whether all instances of u belong to L. We determine the complexity of the violation and the adherence problem, depending on whether trice patterns are linear or not. mid on whether the policy is assumed to be fixed or not.