TY - GEN

T1 - Rule base verification using Petri nets

AU - Yang, Stephen J.H.

AU - Lee, Alex S.

AU - Chu, William C.

AU - Yang, Hongji

N1 - Publisher Copyright:
© 1998 IEEE.

PY - 1998

Y1 - 1998

N2 - We propose a Petri net formalism for the verification of rule based systems. Typical structural errors in a rule based system are redundancy, inconsistency, incompleteness, and circularity. Since our verification is based on Petri nets and their incidence matrix, we need to transform rules into a Petri net first, then derive an incidence matrix from the net. In order to allow a rule based system to be immune from the above described structural errors, we have observed that for all columns in the matrix, all positive entries must be above all negative entries; and for all rows in the matrix, all positive entries must be to the right of all negative entries. If this is not the case, the rule based system may commit errors. Based on this concept, we have developed a tool consisting of the following four phases: rule normalization, rule ordering, rule-to-Petri-net transformation, and rule verification. In phase one, we normalize the rules into Horn clauses. We rearrange the ordering of these normalized rules in phase two, then transform the reordered rules into a Petri net and its corresponding incidence matrix in phase three. In phase four, we perform the rule verification based on the incidence matrix.

AB - We propose a Petri net formalism for the verification of rule based systems. Typical structural errors in a rule based system are redundancy, inconsistency, incompleteness, and circularity. Since our verification is based on Petri nets and their incidence matrix, we need to transform rules into a Petri net first, then derive an incidence matrix from the net. In order to allow a rule based system to be immune from the above described structural errors, we have observed that for all columns in the matrix, all positive entries must be above all negative entries; and for all rows in the matrix, all positive entries must be to the right of all negative entries. If this is not the case, the rule based system may commit errors. Based on this concept, we have developed a tool consisting of the following four phases: rule normalization, rule ordering, rule-to-Petri-net transformation, and rule verification. In phase one, we normalize the rules into Horn clauses. We rearrange the ordering of these normalized rules in phase two, then transform the reordered rules into a Petri net and its corresponding incidence matrix in phase three. In phase four, we perform the rule verification based on the incidence matrix.

UR - http://www.scopus.com/inward/record.url?scp=79953113886&partnerID=8YFLogxK

U2 - 10.1109/CMPSAC.1998.716699

DO - 10.1109/CMPSAC.1998.716699

M3 - 會議論文篇章

AN - SCOPUS:79953113886

T3 - Proceedings - International Computer Software and Applications Conference

SP - 476

EP - 481

BT - Proceedings - 22nd Annual International Computer Software and Applications Conference, Compsac 1998

PB - IEEE Computer Society

Y2 - 19 August 1998 through 21 August 1998

ER -