A high-level Petri nets-based approach to verifying task structures

As knowledge-based system technology gains wider acceptance, there is an increasing need to verify knowledge-based systems to improve their reliability and quality. Traditionally, attention has been given to verifying knowledge-based systems at the knowledge level, which only addresses structural errors such as redundancy, conflict and circularity in rule bases. No semantic errors (such as inconsistency at the requirements specification level) have been checked. In this paper, we propose the use of task structures for modeling user requirements and domain knowledge at the requirements specification level, and the use of high-level Petri nets for expressing and verifying the task structure-based specifications. Issues in mapping task structures onto high-level Petri nets are identified, e.g. the representation of task decomposition, constraints and the state model; the distinction between the "follow" and "immediately follow" operators; and the "composition" operator in task structures. The verification of task structures using high-level Petri nets is performed on model specifications of a task through constraint satisfaction and relaxation techniques, and on process specifications of the task based on the reachability property and the notion of specificity