Reasoning about State Invariants and Constraints in Artificial Intelligence

Title: Reasoning about State Invariants and Constraints in Artificial Intelligence
Speaker: Yongmei Liu (Sun Yat-sen University)
Time: 14:00, Friday, 26 April, 2013.
Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
The concepts of state invariants and constraints in Artificial Intelligence are closely related to those of program invariants and safety properties in formal verification and software engineering. In dynamic systems, state invariants are formulas if true, will be true in all successor states, while state constraints are formulas which hold in  any reachable state. The key difference between the two is that the first  is a first-order property while the second is a second-order property.  In AI, it has been shown that state invariants and constraints can be  used to greatly reduce the planning search space. They are also useful  in debugging a domain axiomatization.

In this talk, I will present our recent work on a sound but incomplete first-order method for automatic verification and discovery of \forall^*\exists^* state constraints for a class of action theories that include many planning benchmarks. Our method is formulated in the situation calculus, theoretically based on Skolemization and Herbrand Theorem, and implemented with SAT solvers. Basically, we verify a state constraint by strengthening it in a novel way so that it becomes a state invariant. We experimented with the blocks world, logistics and satellite domains, and the results showed that, almost all known state constraints can be verified in a reasonable amount of time, and meanwhile succinct and intuitive related state constraints are discovered.

Biography:
Yongmei Liu is a Professor of Computer Science at Sun Yat-sen University. She received her PhD in Computer Science from University of Toronto in 2006. Her research interests lie in Artificial Intelligence, knowledge representation and reasoning, cognitive robotics, program verification and debugging. She has published over ten papers in top international AI conferences IJCAI and AAAI, and served on program committees of IJCAI and AAAI.