The Complexity of Diagnosability and Opacity Verification for Petri Nets

Autor: Béatrice Bérard, Stefan Haar, Sylvain Schmitz, Stefan Schwoon
Přispěvatelé: Modélisation et Vérification (MoVe), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Verification in databases (DAHU), Wil van der Aalst, Eike Best, LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2017
Předmět:
Opacity
0209 industrial biotechnology
Theoretical computer science
Computer science
Reachability problem
Distributed computing
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages/F.4.3.3: Decision problems
Petri nets
02 engineering and technology
Fault (power engineering)
Diagnosability
Theoretical Computer Science
020901 industrial engineering & automation
Reachability
ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methods
0202 electrical engineering
electronic engineering
information engineering
Mathematics
Algebra and Number Theory
Verification
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Complexity
Petri net
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs
020202 computer hardware & architecture
Undecidable problem
Computational Theory and Mathematics
020201 artificial intelligence & image processing
Finite state systems
Information Systems
Zdroj: Petri nets 2017-38th International Conference on Applications and Theory of Petri Nets and Concurrency
Petri nets 2017-38th International Conference on Applications and Theory of Petri Nets and Concurrency, Jun 2017, Zaragoza, Spain. pp.200--220, ⟨10.1007/978-3-319-57861-3_13⟩
Fundamenta Informaticae
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2018, 161 (4), pp.317--349. ⟨10.3233/FI-2018-1706⟩
Fundamenta Informaticae, 2018, 161 (4), pp.317--349. ⟨10.3233/FI-2018-1706⟩
Application and Theory of Petri Nets and Concurrency ISBN: 9783319578606
Petri Nets
ISSN: 0169-2968
DOI: 10.1007/978-3-319-57861-3_13⟩
Popis: International audience; Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
Databáze: OpenAIRE
Externí odkaz: