Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Agent Path Finding
Counterexample guided abstraction refinement (CEGAR) represents a powerful symbolic technique for various tasks such as model checking and reachability analysis. Recently, CEGAR combined with Boolean satisfiability (SAT) has been applied for multi-agent path finding (MAPF), a problem where the task is to navigate agents from their start positions to given individual goal positions so that the agents do not collide with each other. The recent CEGAR approach used the initial abstraction of the MAPF problem where collisions between agents were omitted and were eliminated in subsequent abstraction refinements. We propose in this work a novel CEGAR-style solver for MAPF based on SAT in which some abstractions are deliberately left non-refined. This adds the necessity to post-process the answers obtained from the underlying SAT solver as these answers slightly differ from the correct MAPF solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous approach and speeds up the overall solving process making the SAT-based solver for MAPF competitive again in relevant benchmarks.
Code (0)
등록된 구현이 없습니다.
Tasks
Multi-Agent Path FindingNavigateSimilar Papers 제목 키워드 기반
Unassigned Agents in Compilation-based Multi-agent Path Finding
Compilation-based techniques represent an important stream of solvers for multi-agent path finding (MAPF) due to their modularity and adaptability for non-standard variants of the problem. While in the standard MAPF the …
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks
As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for ver…
TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI
Agentic AI systems act through tools and evolve their behavior over long, stochastic interaction traces. This setting complicates assurance, because behavior depends on nondeterministic environments and probabilistic mod…
Anomaly DetectionNeural Abstractions
We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximator…
Scalable Polyhedral Verification of Recurrent Neural Networks
We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and nonlinear recurrent update…