7 papers
Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
Senthil Rajasekaran, Moshe Y. Vardi
Finite-horizon probabilistic multiagent concurrent game systems, also known as finite multiplayer stochastic games, are a well-studied model in computer science due to their abilit…
Modeling Concurrent Multi-Agent Systems
Senthil Rajasekaran, Moshe Y. Vardi
Recent work in the field of multi-agent systems has sought to use techniques and concepts from the field of formal methods to provide rigorous theoretical analysis and guarantees o…
TIDE: A Trace-Informed Depth-First Exploration for Planning with Temporally Extended Goals
Yuliia Suprun, Khen Elimelech, Lydia E. Kavraki +1
Task planning with temporally extended goals (TEGs) is a critical challenge in AI and robotics, enabling agents to achieve complex sequences of objectives over time rather than add…
Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams
Yi Lin, Moshe Y. Vardi
Motivated by functional synthesis in sequential circuit construction and quantified boolean formulas (QBF), boolean synthesis serves as one of the core problems in Formal Methods.…
Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models
Marcio Nicolau, Anderson R. Tavares, Zhiwei Zhang +4
Computational learning theory states that many classes of boolean formulas are learnable in polynomial time. This paper addresses the understudied subject of how, in practice, such…
Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
Zhiwei Zhang, Samy Wu Fung, Anastasios Kyrillidis +2
The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state…