Parallel Diagnosability Analysis with LTL-X Model Checking based on Petri Net Unfoldings
Laura Brandán-Briones, Agnes Madalinski, Hernán Ponce-de-León · HAL (Le Centre pour la Communication Scientifique Directe) · 2014
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.