Paper detail

Synthesis for observability of logical control networks

Finite-state systems have applications in systems biology, formal verification and synthesis of infinite-state (hybrid) systems, etc. As deterministic finite-state systems, logical control networks (LCNs) consist of a finite number of nodes which can be in a finite number of states and update their states. In this paper, we investigate the synthesis problem for observability of LCNs based on state feedback with exogenous input by using the semitensor product proposed by Daizhan Cheng and the notion of observability graph (previously called weighted pair graph) proposed by us. We show that state feedback with exogenous input can either enforce or weaken observability of an LCN. We prove that for an LCN $Σ$ and another closed-loop LCN $Σ_{\mathcal{C}}$ obtained by feeding a state-feedback controller $\mathcal{C}$ with exogenous input into $Σ$, (1) if $Σ$ is observable, then $Σ_{\mathcal{C}}$ can be either observable or not; (2) if $Σ$ is not observable, $Σ_{\mathcal{C}}$ can also be observable or not. We also prove that if an unobservable LCN can be made observable by state feedback with exogenous input, then it can also be made observable by state feedback (without exogenous input, equivalent to state feedback with constant input). Furthermore, we give an upper bound on the number of state-feedback controllers that are needed to be tested in order to verify whether an unobservable LCN can be made observable by state feedback, and based on the procedure of obtaining the upper bound, we design an observability synthesis algorithm, by additionally combining the ideas of a greedy algorithm and dynamic programming. These results open the study of observability synthesis in LCNs.