• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

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

Journal of Parallel and Distributed Computing. 2021. Vol. 155. P. 14-23.
Mecheraoui K., Lomazova I. A., Belala N.

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.