Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search
summary
Proposes a narrowing-based reachability method guided by a heuristic scoring function (G for path cost plus H for error likelihood) that targets counterexamples involving few objects, proves search completeness when all reachable patterns below any score are finite, and ships a prototype implementation. Applied to the one-third consensus threshold case, breadth-first narrowing explores ~25,000 symbolic states and takes ~4.8 hours, while the heuristic with prior knowledge finds a counterexample in about 20 minutes.
AI-written summary · about
chapters (9)
- 0:00Symbolic reachability analysis
- 3:40Modeling with Maude rules
- 6:38Narrowing technique
- 9:28Breadth-first search for verification
- 12:23Limitations of narrowing algorithms
- 15:51Heuristic search for infinite states
- 18:02One-third consensus algorithm
- 20:52Summary and future work
- 22:17Q&A
related talks
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
27mProbabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight ...
52mFine-Grained Complexity and Algorithm Design for Graph Reachability and Distance Problems
28mReasoning about Distributed Reconfigurable Systems
18mPsym: Efficient Symbolic Exploration of Distributed Systems
19mBeeping Shortest Paths via Hypergraph Bipartite Decomposition
46mHow Cheap Learning (not deep learning) Finds Faults in Distributed Systems
29mReachability in multi-agent transfer systems