Consistent timed semantics for nested petri nets with restricted urgency

Abstract

The nested Petri nets are a nets-within-nets formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. The formalism is supported by developed verification methods based on structural analysis and model checking techniques. Time constraints are crucial for many safety critical and everyday IoT systems. Recently, the non Turing-complete time semantics for Time Petri nets based on restricted urgency was suggested; and, it was shown that some behavioural analysis problems are decidable under the semantics. In the paper, the semantics is extended to the nested Petri nets formalism and it was demonstrated that some behavioural analysis problems are still decidable. The semantics is illustrated by an example of a health monitoring system.