Automated Verification of Social Laws in Numeric Settings


  • Ronen Nir Technion - Israel Institute of Technology
  • Alexander Shleyfman Bar-Ilan University
  • Erez Karpas Technion - Israel Institute of Technology



PRS: Mixed Discrete/Continuous Planning, PRS: Deterministic Planning


It is possible for agents operating in a shared environment to interfere with one another. One mechanism of coordination is called Social Law. Enacting such a law in a multi-agent setting restricts agents' behaviors. Robustness, in this case, ensures that the agents do not harmfully interfere with each other and that each agent achieves its goals regardless of what other agents do. Previous work on social law verification examined only the case of boolean state variables. However, many real-world problems require reasoning with numeric variables. Moreover, numeric fluents allow a more compact representation of multiple planning problems. In this paper, we develop a method to verify whether a given social law is robust via compilation to numeric planning. A solution to this compilation constitutes a counterexample to the robustness of the problem, i.e., evidence of cross-agent conflict. Thus, the social law is robust if and only if the proposed compilation is unsolvable. We empirically verify robustness in multiple domains using state-of-the-art numeric planners. Additionally, this compilation raises a challenge by generating a set of non-trivial numeric domains where unsolvability should be either proved or disproved.




How to Cite

Nir, R., Shleyfman, A., & Karpas, E. (2023). Automated Verification of Social Laws in Numeric Settings. Proceedings of the AAAI Conference on Artificial Intelligence, 37(10), 12087-12094.



AAAI Technical Track on Planning, Routing, and Scheduling