2018
Symbolic Verification of GOLOG Programs with First-Order BDDs
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...