An Ontology Alignment Approach Using Objective Weighting Methods for Enhanced Similarity Calculation in Formal Verification of Reconfigurable Discrete-Event Control Systems (RDECSs)

This paper addresses the formal verification of Reconfigurable Discrete Event Control Systems (RDECSs), modeled by Reconfigurable Timed Net Condition/Event Systems (R-TNCESs). Formal verification ensures system correctness, but faces challenges due to the complexity and redundant calculations introduced by reconfigurability. This complexity, exacerbated by internal similarities within system configurations, and external similarities between different systems, often leads to state explosion during model checking, complicating analysis. The novelty of the proposed ontology alignment approach lies in its ability to reduce verification complexity by identifying internal and external similarities, thus minimizing redundancy. A key contribution is the enhancement of ontology alignment approaches by introducing a new similarity function tailored for RDECSs, coupled with a multi-criteria decision analysis method for objectively weighting this function. Importantly, all similarity scores are computed deterministically in closed form from ontology content; the MCDA weighting step is applied once, non-iteratively, to the resulting decision matrix — this approach is therefore fundamentally different from iterative machine-learning-based methods. This approach significantly increases scalability and accuracy, overcoming limitations of existing solutions. The added value of this work is reflected in the substantial gains it offers in formal verification efficiency. Numerical validation on two benchmark production systems, FESTO MPS and THREADING HOLE SYSTEM, shows significant improvements. While precision remains at 1.0, recall improves by 13.33%, enabling the detection of more relevant similarities and reducing the state space size. This reduction leads to notable decreases in execution time, demonstrating the effectiveness of the proposed approach.