Formal representation and verification of ontology using State Controlled Coloured Petri Nets

Ontologies are widely used in many areas. Different automatic or semiautomatic extraction techniques have been proposed for building domain ontology in recent years. The correctness of the extracted ontology, however, has often been ignored or not verified formally. With increasingly complex and sophisticated realworld domains, the issue of correctness and verification of ontology is becoming more important. This chapter proposes a formal technique for ontology representation and its verification, based on State Controlled Coloured Petri Net (SCCPN), which is a high level net combining Coloured Petri Net and State Controlled Petri Net. It provides the capability of detection and identification of potential anomalies in ontology. We first describe the formal representation of ontology by SCCPN. The definition of SCCPN for modeling ontologies and the mapping between them are presented in detail. Moreover, the ontology inference in SCCPN is also formulated with specified inference mechanisms. After modeling ontology by SCCPN, the formal verification of potential anomalies (including redundancy, circularity and contradiction) is discussed. It is based on the reachable markings generated by transition firings in the Petri nets.