'True Concurrency' Semantics for Time Petri Nets with Weak Time and Persistent Atomic Policies

Dense-Time Petri nets (TPNs), where time intervals for transition firings are assigned, are now a well-established model, which is used to describe and study safety-critical systems. Generally, the state space of the TPN is uncountably infinite, which increases the complexity of model analysis. 'True concurrency' semantics represents the behavior of the TPN as a set of actions, the causality relation between which is modeled by a partial order, and the absence of causality implies concurrency. This representation is more adequate for verifying properties of concurrent systems, e.g., deadlock-freedom, fairness, maximum parallelism, etc. This paper introduces and investigates step semantics (based on sets of concurrent actions) and partial order semantics (based on sets of causally ordered and concurrent actions) for TPNs the behavior of which is governed by the weak time policy (i.e., the passage of model time is not constrained by transition firing) and persistent atomic memory technique (i.e., transition firing is regarded as an atomic action when clocks are reset).