A Petri net extension for systems of concurrent communicating agents with durable actions

This paper provides a true-concurrency approach for the specification and verification of systems of concurrent communicating agents with durable actions. We present high-level Petri nets with durable actions (DaHL) to cope with various details in such complex systems. We define a DaHL module as an open variant of time-dependent colored Petri nets. A DaHL system is a fused set of modules for systems consisting of concurrent agents which can interact with each other. We also introduce hybrid-based reachability graph that covers the entire state space of DaHL systems with a true-concurrency semantics. We show that such reachability graph allows us to check important properties such as deadlock-freeness, liveness, home space, and reversibility, and also to predict timing properties prior to real implementation. A case study is used to model and analyze a simple scenario where autonomous vehicles are able to transport containers freely in an enterprise environment. (C) 2021 Elsevier Inc. All rights reserved.

Automated summary

This paper introduces a true-concurrency approach for specifying and verifying systems of concurrent communicating agents with durable actions. It presents high-level Petri nets with durable actions (DaHL) to handle details in complex systems, and defines a DaHL module as an open variant of time-dependent colored Petri nets. The paper also introduces a hybrid-based reachability graph to cover the entire state space of DaHL systems and allows checking of important properties before real implementation.