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.