Incremental Verification of Inference Observability in Decentralized Discrete-Event Control

Inference observability is one of the properties that must be satisfied to synthesize solutions to decentralized supervisory control problems. Current verification strategies require the construction of the complete system model. However, when a system model consists of multiple components, these monolithic approaches may be computationally infeasible due to the state-space explosion problem, a situation that arises when the system's state space increases exponentially with the number of its components. Incremental verification algorithms have been proposed to navigate this issue, where verification occurs component-wise. Our proposed solution to this issue involves updating an algorithm for the incremental verification of co-observability and extending it to inference observability.