摘要：AbstractIn this article we introduce the problem of timed pattern diagnosis in timed system and propose a method to solve a sub-class of theses problems: the problem of timed pattern diagnosis of workflows. It consists in searching for all the possible evolutions of the workflow that are consistent with a timed sequence of observations and determining whether these evolutions match a pattern of timed events instead of a single fault event. The formal characterization of the diagnosis problem is based on the notion ofpattern matching. Defined as a reachability problem, the diagnosis problem is then solved bymodel checking.
关键词：KeywordsDiagnosisTime Petri NetTimed PatternModel checking
