Symbolic Verification of GOLOG Programs with First-Order BDDs

Abstract

loop: while (∃x.OnRobot(x)) do πx:Dish unload (x) endWhile; G OLOG is an agent language that allows defining behaviours πy:Room { goto(y); in terms of programs over actions defined in a Situation Cal- while (∃xDirty(x, y)) do culus action theory. Often it is vital to verify such a program πx:Dish load (x, y) endWhile }; against a temporal specification before deployment. So far goto(kitchen) work on the verification of G OLOG has been mostly of theo- retical nature. Here we report on our efforts on implementing In each iteration of the infinite outer loop, the robot (ini- a verification algorithm for G OLOG based on fixpoint com- tially located in the kitchen) first unloads all dishes it car- putations, a graph representation of program executions, and ries, selects a room in the building, moves there, collects a symbolic representation of the state space. We describe the all dirty dishes there, and returns to the kitchen. Here, techniques used in our implementation, in particular a first- Dirty(x, y) reads as “dirty dish x is in room y” and order variant of OBDDs for compactly representing formulas. load (x, y) as “load dish x from room y”, and there are ex- We evaluate the approach by experimental analysis. ogenous newdish(x, y) actions causing a new dirty dish x to appear in room y. Unlike the previous example, the choice operators π (“picks”) here only range over finite domains