Benchmarks of Extended Basis Reachability Graphs
Yin Tong
TL;DR
This paper compares the efficiency of various graph-based methods for verifying K-step and infinite-step opacity in systems, focusing on Extended Basis Reachability Graphs, Basis Reachability Graphs, and Reachability Graphs.
Contribution
It provides a comparative analysis of the performance of different graph-based approaches for opacity verification.
Findings
EBRG offers efficient verification for opacity.
Comparison shows trade-offs among EBRG, BRG, and RG.
Results guide the choice of graph method for system security analysis.
Abstract
In this note, we want to provide a comparison among the efficiency of different approaches for the verification of K-step and infinite-step opacity based on three different graphs: the Extended Basis Reachability Graph (EBRG), the Basis Reachability Graph (BRG) when applicable, and the Reachability Graph (RG).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Petri Nets in System Modeling · semigroups and automata theory