Abstract: This paper presents a model for OWL-S process model based on labelled Petri net and gives the transformation rule from process model to LPN. It utilise LPN analysis methods to analyze reachability of the obtained model and check whether there are deadlocks. This method validates the correctness of corresponding process model description in OWL-S editor environment.

Key words: OWL-S process model, Labelled Petri net, Reachability, Deadlock, Petri net markup language

摘要： 提出了OWL-S过程模型的标签Petri网建模方法，给出了过程模型到LPN的转换规则，利用LPN分析方法对模型进行了可达性分析、死锁检测，能有效地检验过程模型描述的正确性。在OWL-S编辑器中嵌入该功能，完善了编辑器的功能。

关键词: OWL-S过程模型, 标签Petri网, 可达性, 死锁, Petri网标记语言