Verification of initial-and-final-state opacity for unambiguous weighted automata.

Initial-and-final-state opacity (IFO) is a type of opacity that characterizes a system's ability to prevent the disclosure of information about whether its evolution starts at an initial state and ends at a final state. In this paper, we extend the notion of IFO from the logical automata to the framework of unambiguous weighted automata (UWAs) that do not contain any cycle composed solely of unobservable events. For the verification of IFO, we first construct a labeled observer and a trellis-based initial state estimator for a given UWA. Even though the labeled observer has much smaller state space compared to the trellis-based initial state estimator, it cannot be used when the set of secret state pairs or the set of non-secret state pairs is not in the Cartesian product form. Based on the labeled observer, we present a more efficient method to verify IFO in the case when the set of non-secret state pairs is expressed as a Cartesian product, regardless of whether the set of secret state pairs is in the Cartesian product form. Furthermore, we use the labeled observer to verify initial-state opacity for a UWA.