Opacity is an essential feature in the control and supervision of cyberphysical systems, in particular w.r.t. cybersecurity. It prevents intruders from knowing whether the system accessed specific secret states. In particular, a quantified variant of the opacity property, called K-step opacity, ensures that the intruder cannot determine the passage of the system through a secret state within K steps following such a passage. This paper introduces an algebraic method to verify K-step opacity in discrete event systems modeled by partially observed labeled Petri nets. Namely, we develop an algebraic formulation that establishes a necessary and sufficient condition for K-step opacity, and sets the basis for investigating this feature by means of optimization techniques. The underlying idea is to eliminate the need to build the state space of the net or any derived graph, thus tackling the potentially related combinatorial explosion problem.

The aim of the paper is the estimation of sequences in Timed Petri nets. We propose a general strategy composed of two phases: The first phase considers the logical aspect only and suggests candidate count vectors where the second one checks the existence of a relevant time sequence for a Timed Petri net and generate a subspace of time sequences for a given candidate vector.