# Synthesis for observability of logical control networks

## TL;DR

This paper investigates how to synthesize control strategies to ensure observability in logical control networks (LCNs), using semitensor products and observability graphs, with algorithms to verify and enforce observability.

## Contribution

It introduces a novel synthesis method for observability in LCNs using state feedback with exogenous input, including bounds and algorithms for practical verification.

## Key findings

- State feedback can both enforce and weaken observability.
- Unobservable LCNs can be made observable by feedback, with or without exogenous input.
- An observability synthesis algorithm based on bounds, greedy, and dynamic programming methods.

## Abstract

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 $\Sigma$ and another closed-loop LCN $\Sigma_{\mathcal{C}}$ obtained by feeding a state-feedback controller $\mathcal{C}$ with exogenous input into $\Sigma$, (1) if $\Sigma$ is observable, then $\Sigma_{\mathcal{C}}$ can be either observable or not; (2) if $\Sigma$ is not observable, $\Sigma_{\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.