Skip to Main content Skip to Navigation
Poster communications

Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings

Abstract : We present a framework that shows how components in parallel can infer the diagnosability property of the complete system (distributed and with multiple faults) from the diagnosability verification of each component synchronizing with a fault free versions of the other ones. Furthermore, we use existing efficient methods and tools, in particular parallel model checking based on Petri net unfoldings, to verifier diagnosability of such components.
Document type :
Poster communications
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00915478
Contributor : Hernan Ponce de Leon <>
Submitted on : Monday, December 15, 2014 - 2:23:42 PM
Last modification on : Monday, February 15, 2021 - 10:49:08 AM
Long-term archiving on: : Saturday, April 15, 2017 - 4:32:18 AM

File

dx-2014.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00915478, version 2

Citation

Laura Brandan-Briones, Agnes Madalinski, Hernán Ponce de León. Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings. Workshop on Principles of Diagnosis, Sep 2014, Graz, Austria. 2013. ⟨hal-00915478v2⟩

Share

Metrics

Record views

328

Files downloads

447