The Boolean constraint method for the observability problem of binary dynamical systems

Abstract

In this work, we propose a new approach based on the Boolean constraint method for investigating the observability of initial states in binary dynamical systems over a finite time interval. Within this framework, proving the satisfiability of the observability property reduces to verifying the truth of a quantified Boolean formula that integrates both the logical specification of the property and the system's dynamic equations. Several examples are presented to illustrate the application of the theoretical results obtained. A key advantage of the proposed technique is its scalability, ensuring its applicability to systems with high-dimensional state, control, and output vectors over extended discrete time intervals.