On Compositionality of 1L-Liveness and Local Path-Based Properties for Nested Petri nets
Nested Petri nets (NP-nets) are a ‘nets-within-nets’ formalism convenient for modelling systems that consist of distributed mobile agents with individual behaviour. An NP-net consists of a highlevel system net and individual net tokens. Each net token is defined as a Petri net, and net tokens are coordinated by the system net. Many behavioural problems such as liveness, boundedness, reversibility are undecidable for two-level NP-nets; others, e.g. termination and coverability, have high complexity. Compositionality allows us to infer NP-net behaviour properties from
the properties of its constituents — net components. The compositionality of boundedness and system-level liveness has been studied in . In the paper, we suggest sufficient conditions for compositionality of liveness of net tokens and system net. For NP-nets with one synchronization label, we suggest necessary and sufficient conditions for compositionality of net tokens and system net liveness. We also demonstrate that under additional restrictions,
linear-time action-based properties of a net token can be checked locally.