In this paper, we propose an approach that allows to limit the verification of an LTL property of a modular system to the parts that it concerns. Given a modular Petri net and a property that concerns one module, the model checking is performed by exploring exclusively an abstract graph that models the behaviors of the module and is enriched with some global information. Thanks to a distributed state space version, named Reduced Distributed State Space (RDSS), of the considered modular system, there is no need to explore graphs of irrelevant modules to the property. We used the SPOT library to implement the suggested model checking in a C++ prototype, and we compared our primary results with those of the LTSmin model checker.
This page summarises published work. The authoritative version sits with the publisher.
DOI: 10.1109/codit62066.2024.10708172
Is something wrong with this record? Report it or request removal.
Discussion
Have you built on this work, tried to replicate it, or seen it applied in practice? Share what you know. Verified researchers and MARATTO™ domain experts can open a discussion, and any member can reply. Contributions are reviewed before they appear.
No discussion yet. Open the first thread.
New to MARATTO™? Create a free account.
