Comparison of trace and bisimulation equivalences on time Petri nets with weak time policy

The security of many information and computer systems is critically important, since their failure can lead to large losses. Behavioral equivalences play an important role in the specification and verification both to compare distinct systems and to reduce the structure of a system without affecting its behavior. Various behavioral equivalences for concurrent and distributed systems have been promoted in the literature and the relationships between them have been fairly well-studied. Two dichotomies are usually considered when comparing the cquivalences. The first dichotomy is the “linear time - branching time” spectrum. Here, various possibilities of taking into account the choice points between the alternative actions of systems are discussed. Alternative choice points are completely ignored in the linear time semantics. As a result, the system behavior is described by the set of all sequences of system actions. Trace equivalence is a typical example of linear time equivalence. The standard example of branching time equivalence is bisimulation assuming that systems should behave in the same way, mutually simulating each other. Bisimulation carefully takes into account the branching structure of the systems behaviors. The second dichotomy is the so-called “interleaving - partial” order spectrum. Here, it determines how to take into account partial order representing causal dependences between system actions. The essence of the interleaving approach is to represent the concurrency relation as a nondctcrministic choice between the executions of linearly ordered actions, rather than directly. The advantage of the interleaving interpretation of concurrency is its simplicity, mathematical elegance, and allowing for the analysis of some safety and liveness properties of systems. However the difference between concurrency and nondeterminism is lost. A way to overcome the limitations of the interleaving approach is to model concurrency as a lack of causality dependence between system actions, which is presented, as a rule, by a partial order. In the step semantics located between the boundaries of the spectrum, concurrency is presented as a step - a set of concurrent actions. Petri nets (PN) is one of the generally accepted models for analysis of concurrent and distributed systems. The PN consists of two different sets of elements - places and transitions and a labeling function mapping each transition to an action. A state of the PN is called a marking - a subset of places that receive tokens when the net functions. A transition is enabled at a marking if the input places of the transition contain tokens. The firing of a transition enabled at a marking results in the new marking in which tokens are consumed from the input places and tokens are produced to the output places of the transition. In verification systems, there is an obvious need for considering time. Different timed extensions of Petri nets have been proposed. Time Petri Nets (TPNs) are now a well-established model to describe and study safety-critical systems that require verification of real time (quantitative) characteristics, in addition to functional (qualitative) properties. In the TPN, each transition is associated with a time interval. With that, each transition is assumed to have its own local clock. A state of the TPN contains a current marking and readings of the local clocks of enabled transitions. A transition can fire from a state only if the transition is enabled at the corresponding marking and its clock reaches a moment in time that is within the interval associated. So, the firing of an enabled transition can be suspended for a certain time. Along with that, the firing itself takes no time. State changes are divided in two types: either time elapses, i.e. the clocks of enabled transitions go forward, or a transition fires, i.e. a current marking is changed to a new one and the clocks of the transitions that become enabled at the new marking (newly enabled transitions) are reset to zero. There are two policies of time elapsing in TPNs, which define strong and weak semantics. In the former semantics, time elapsing cannot exceed the upper bounds of enabled transitions and, therefore, an enabled transition must fire no later than the upper bound of its time interval is reached. On the contrary, any time elapsing is allowed in the latter semantics and, therefore, enabled transitions are not forced to fire. It is known that the two semantics are incomparable w.r.t. timed weak bisimulation. Memory policies in TPNs determine when the local clocks of enabled transitions are reset. Intermediate and atomic memory policies are put forward in the literature. The former treats intermediary marking, i.e. the marking after consumption of tokens from the input places and before production of tokens to the output places of a transition t that fires.