Hierarchy of equivalences on time Petri nets with weak time policy

The security of many information systems is critically important, since their failure can lead to large economic losses and human casualties. Equivalences allow comparing systems and specifications in terms of different aspects of their behavior. In this wav, they are used to verify and reduce systems. Models of concurrent and distributed systems are compared in the dichotomies of “linear time - branching time" and “interleaving - partial order" in the literature. The first criterion of comparison is a degree of conflict accounting (a moment of choosing between several “branches” of computing). The semantics of linear time ignores the points of choice, and the behavior is described by the set of all executions (processes). Trace equivalence is a typical example of such cquivalence. On the contrary, branching time semantics takes into account the branching structure of the systcm”s behaviors. The second criterion of comparison is the degree of partial order accounting. Interleaving semantics ignores partial order. The concurrency is reduced to a nondctcrministic choice between executions of linearly ordered actions. On the other hand, “true concurrency” models preserve causality and concurrency between actions. Petri nets (PN) are one of the generally accepted tools for modeling and analyzing concurrent and distributed systems. The (PN) consists of two different sets of elements - transitions (system events) and places (conditions for events). This model is represented as an oriented bipartite graph. A state of the PN is a marking (a set of places with tokens'). All conditions for an event are met if there is a token in each input place of the corresponding transition. This transition is called enabled and can fire, i. e. change the marking. The new marking is obtained as a result of removing tokens from the input places and creating new tokens in the output transition places. It is often necessary to take into account time or quantitative characteristics when verifying systems. Various time extensions of Petri nets have been defined for these purposes. Time Petri Nets (TPNs) are model where each transition has its own clock and time interval. A state of the model is defined by the marking and the clock readings of enabled transitions. A transition can fire if it is enabled in the marking and its clock readings are in its interval. Firing the transition changes the marking, disables the clock for not enabled transitions, and initializes (resets) a clock for some enabled transitions. There is an intermediate, atomic and persistent atomic clock reset policy. Intermediate policy takes into account the marking before the creation of new tokens and after the removal of old tokens (intermediate marking). A transition clock will be disabled if the transition was not enabled in the intermediate marking. If a transition became enabled after the creation of new tokens, then its clock will take a zero value. The atomic policy does not consider intermediate states. Resetting clock will only happen if the transition is disabled in the new marking. The transition clock that is fired is always reset in the case of an intermediate and atomic policy (unlike persistent atomic). It is shown in [1] and [2] that the persistent atomic policy is strictly more expressive than the atomic one. The atomic policy is not less expressive than the intermediate one. In addition, the authors give examples of models of systems where the atomic policy is more preferable. Time elapsing increases the readings of the local clock of enabled transitions. Strong and weak time policies are presented in the literature. The strong policy restricts time elapsing. The value of a transition clock cannot go beyond the upper limit of the time interval. The transition must either fire or become disabled. In the weak policy, there are no restrictions on time elapsing. As it was shown in [3], strong and weak policies of time elapsing are incomparable in expressiveness. Definition and analysis of equivalence relations in the “linear time - branching time” and “interleaving - partial order” spectra is one of the important tasks for models of concurrency and distributed systems. In [4], a hierarchy of equivalences for time-free Petri nets is presented. In [5], the authors developed and investigated the simple bisimulation and forward-backward equivalences for the TPNs with the strong time policy and intermediate clock reset strategy. In [6], the semantic models in the “interleaving - partial order” spectrum were defined in terms of weak TPNs. In [7], trace and simple bisimulation equivalences were developed for the TPNs with an intermediate clock reset policy. As far as we know, there are no equivalences in the literature for TPNs with a weak time policy and with a persistent atomic method of resetting the clock.