Jens Claßen committed May 02, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 ``````# Vergo: A Verification System for GOLOG Programs Vergo is (yet) an(other) implementation of the high-level agent control language **GOLOG**, specifically devised as a testbed for various algorithms for the temporal verification of programs. This repository is a collection of code whose development was started during the preparation of the doctoral thesis > Jens Claßen:
> **Planning and Verification in the Action Language GOLOG.**
> PhD Thesis, Department of Computer Science, RWTH Aachen University, 2013. > [[Fulltext](http://publications.rwth-aachen.de/record/229059/)] and was continued during the [VERITAS][1] project on Verification of Non-Terminating Action Programs within the research unit on [Hybrid Reasoning for Intelligent Systems][2] funded by the [German Science Foundation][3] (DFG). While other GOLOG implementations such as [Reiter's original prototype][4], [IndiGolog][5] or [Readylog][6] make use of Prolog's evaluation mechanism for reasoning, Vergo supports full first-order logic (FOL) by relying on an embedded theorem prover. That is to say Prolog is used only for the *manipulation* of formulas (for syntactic transformations such as regression), which are represented as terms `````` Jens Claßen committed May 24, 2019 26 27 28 29 30 31 32 33 34 ``````with a special syntax. For example. `all(X,some(Y,p(X) + q(Y) * -r(X,Y)))` expresses that for every `X` there is some `Y` such that `p(X)` or `q(Y)` and not `r(X,Y)` holds (with the usual syntactical preference among Boolean connectives). *Inference* tasks, such as deciding whether an initial theory entails a query formula, are then delegated to the theorem prover. The reason for this is that for the purpose of formal verification, it is necessary to adhere strictly to the formal definition of the underlying logic, and avoid intermingling Prolog evaluation with GOLOG reasoning. It also means that the full `````` Jens Claßen committed May 02, 2019 35 36 37 38 39 40 41 42 43 44 45 46 ``````expressivity of FOL can be utilized to devise agent programs, which, as always, comes at the price of computational efficiency. As opposed to many other GOLOG systems, Vergo is not a fully-fledged agent framework that includes interfaces to an agent's sensors and actuators and takes care of the full sense-plan-act cycle. Should one actually decide to use it for controlling an agent, it should rather be thought of as a *module* to be integrated into a larger agent/robot framework. The interpreter runs in a single instance of Prolog and provides an interface for (a) telling the system updates about world state changes in terms of actions that have been executed and sensing results that were obtained, and (b) asking it queries about what is `````` Jens Claßen committed May 24, 2019 47 ``````known about the world state or what the next action should be. We thus `````` Jens Claßen committed May 02, 2019 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 ``````follow Levesque's functional view on a knowledge-based system. The code provided in this repository is in a constant state of 'work in progress' and comes without any warranty (see also the attached license). The algorithms implemented herein merely serve as proofs of concept and are open-sourced for the sake of academic exchange and reproducibility. [1]: https://www.hybrid-reasoning.org/en/projects/a1-verification-of-non-terminating-action-programs/ [2]: https://www.hybrid-reasoning.org [3]: http://www.dfg.de [4]: http://www.cs.toronto.edu/cogrobo/kia [5]: https://bitbucket.org/ssardina-research/indigolog/src [6]: http://robocup.rwth-aachen.de/readylog ## Getting Started Vergo requires a recent version of [SWI-Prolog](http://www.swi-prolog.org) as well as at least one FOL theorem prover being installed (see [dependencies](#dependencies) below). The environment variable PATH_GOLOG should then point to the root directory of this software, e.g. via `````` Jens Claßen committed Apr 30, 2019 70 `````` `````` Jens Claßen committed May 02, 2019 71 `````` \$ export PATH_GOLOG=/home/user/vergo/ `````` Jens Claßen committed Mar 06, 2015 72 `````` `````` Jens Claßen committed May 02, 2019 73 74 75 ``````There currently is no elaborate documentation. Instead, we encourage the interested reader to study the [sources](#directories) and look at the provided examples. The underlying algorithms are discussed in the `````` Jens Claßen committed May 03, 2019 76 ``````corresponding [papers](#references). `````` Jens Claßen committed Mar 06, 2015 77 `````` `````` Jens Claßen committed May 02, 2019 78 79 80 81 82 83 ``````### Verification by Fixpoint Computation To get started with verification by fixpoint computation, consider the `coffee_robot` domain in the `examples` directory. Look at the file `coffee_bat_fct.pl` and how actions, fluents, programs and temporal properties are defined in it. From within the directory, call `````` Jens Claßen committed Jul 31, 2020 84 ``````SWI-Prolog and consult the file: `````` Jens Claßen committed May 02, 2019 85 `````` `````` Jens Claßen committed Jul 31, 2020 86 `````` ?- [coffee_bat_fct]. `````` Jens Claßen committed May 02, 2019 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 `````` Next, construct the characteristic graph via ?- construct_characteristic_graph(main). and observe the output. The actual verification for one of the properties is initiated e.g. through ?- verify(main,prop4). ### Verification by Abstraction This verification method additionally requires a model checker (see [dependencies](#dependencies) below). For the local-effect case, consider the `dish_robot` domain in the `examples` directory. Look at the file `dish_robot_bat.pl` and how actions, fluents, programs and temporal properties are defined in it. From within the directory, call `````` Jens Claßen committed Aug 17, 2020 104 ``````SWI-Prolog, and consult the file containing the action theory: `````` Jens Claßen committed May 02, 2019 105 `````` `````` Jens Claßen committed Aug 17, 2020 106 `````` ?- [dish_robot_bat]. `````` Jens Claßen committed May 02, 2019 107 108 `````` Next, start the construction of the abstract transition system via `````` Jens Claßen committed Mar 06, 2015 109 `````` `````` Jens Claßen committed Aug 17, 2020 110 `````` ?- compute_abstraction(main). `````` Jens Claßen committed May 02, 2019 111 112 113 114 115 116 117 `````` and observe the output (this may take some time). To actually verify a property by the model checker, call then e.g. ?- verify(prop5). ## Directories `````` Jens Claßen committed Mar 06, 2015 118 119 120 121 122 123 124 125 126 127 128 129 `````` The code is divided into the following subdirectories: - agents: Contains agents interfaces. These are required for the actual execution of and interaction with an agent program. - examples: Example domain definitions for agents. `````` Jens Claßen committed Aug 17, 2020 130 131 132 133 134 135 136 137 138 ``````- golog: Contains code related to Golog programs, e.g. transition semantics. - kbs: Modules implementing a knowledge base given a certain base logic, most importantly L (FOL with standard names). `````` Jens Claßen committed Nov 20, 2019 139 ``````- lib: `````` Jens Claßen committed Mar 06, 2015 140 `````` `````` Jens Claßen committed Nov 20, 2019 141 `````` Various libraries (utilities, environment variables). `````` Jens Claßen committed Mar 06, 2015 142 `````` `````` Jens Claßen committed Nov 14, 2019 143 ``````- logic: `````` Jens Claßen committed Mar 06, 2015 144 `````` `````` Jens Claßen committed Aug 17, 2020 145 `````` Various modules for representing and manipulating logical formulas, `````` Jens Claßen committed Aug 17, 2020 146 `````` e.g. (first-order) BDD representation, and the closed-world and `````` Jens Claßen committed Aug 17, 2020 147 `````` unique names assumptions. `````` Jens Claßen committed Nov 20, 2019 148 `````` `````` Jens Claßen committed Jul 26, 2020 149 150 151 152 ``````- planning: Planning related code such as PDDL parser. `````` Jens Claßen committed Nov 20, 2019 153 154 155 ``````- projection: Code implementing regression and progression methods. `````` Jens Claßen committed Nov 14, 2019 156 157 158 `````` - reasoners: `````` Jens Claßen committed Mar 06, 2015 159 `````` Contains different implementations and interfaces for backend `````` Jens Claßen committed Aug 17, 2020 160 `````` reasoners (FOL, FO^2, Description Logics, System Z). `````` Jens Claßen committed Mar 06, 2015 161 162 163 164 165 166 167 168 169 `````` - temp: Temporary files are put here. - verification: Contains implementations of different verification methods. `````` Jens Claßen committed May 02, 2019 170 ``````## Dependencies `````` Jens Claßen committed Mar 06, 2015 171 `````` `````` Jens Claßen committed Oct 05, 2020 172 ``````Vergo uses SWI-Prolog (currently version 8.3.8). Furthermore, there `````` Jens Claßen committed Sep 07, 2015 173 ``````are the following dependencies to external tools and systems: `````` Jens Claßen committed Mar 06, 2015 174 `````` `````` Jens Claßen committed May 02, 2019 175 ``````1. **Theorem Prover** (required) `````` Jens Claßen committed Mar 06, 2015 176 `````` `````` Jens Claßen committed May 02, 2019 177 178 179 `````` In order to be able to use FOL theorem proving, we require that at least one theorem prover is available. `````` Jens Claßen committed Jul 31, 2019 180 `````` 1. E Prover `````` Jens Claßen committed May 02, 2019 181 `````` `````` Jens Claßen committed Jul 31, 2019 182 183 184 185 `````` By default, the system expects the 'eprover' executable is visible in PATH. The system has been developed and tested with the (currently) most recent version "2.0 Turzum". E can be downloaded from `````` Jens Claßen committed May 02, 2019 186 `````` `````` Jens Claßen committed Jul 31, 2019 187 `````` http://www.eprover.org `````` Jens Claßen committed May 02, 2019 188 `````` `````` Jens Claßen committed Jul 31, 2019 189 190 191 `````` and installed manually. For some distributions such as Fedora, there are also prepackaged versions. Installation on Fedora then for example is via `````` Jens Claßen committed May 02, 2019 192 `````` `````` Jens Claßen committed Jul 31, 2019 193 `````` \$ sudo yum install E.x86_64 `````` Jens Claßen committed May 02, 2019 194 `````` `````` Jens Claßen committed Jul 31, 2019 195 `````` 2. Vampire `````` Jens Claßen committed May 02, 2019 196 `````` `````` Jens Claßen committed Jul 31, 2019 197 198 199 200 `````` Alternatively, Vampire can be used instead of E. This similarly requires that the 'vampire' executable binary (last tested stable version: 4.2.2) is visible in PATH. Vampire is available under `````` Jens Claßen committed Mar 06, 2015 201 `````` `````` Jens Claßen committed Jul 31, 2019 202 `````` https://vprover.github.io/index.html `````` Jens Claßen committed Mar 06, 2015 203 `````` `````` Jens Claßen committed Jul 31, 2019 204 `````` Then call `````` Jens Claßen committed Mar 06, 2015 205 `````` `````` Jens Claßen committed Jul 31, 2019 206 `````` ?- fol:set_reasoner(vampire). `````` Jens Claßen committed May 02, 2019 207 208 209 210 `````` 3. FO²-Solver Verification based on abstraction and model checking relies on `````` Jens Claßen committed May 24, 2019 211 212 213 214 `````` deciding consistency of sets of formulas from the two-variable fragment of FOL. An FOL theorem prover is generally not a decision procedure for this problem. As alternative, we can use Tomer Kotek's FO²-Solver `````` Jens Claßen committed May 02, 2019 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 `````` http://forsyte.at/people/kotek/fo2-solver/ (version 0.3d), which in turn requires a propositional SAT solver such as Glucose http://www.labri.fr/perso/lsimon/glucose/ or Lingeling http://fmv.jku.at/lingeling/ as well as a Java runtime environment. The environment variable PATH_FO2SOLVER has to point to the location of the installation of FO²-Solver, e.g. using \$ export PATH_FO2SOLVER=~/local/FO2-Solver/ `````` Jens Claßen committed Jul 31, 2019 233 234 235 236 `````` Then call ?- fol:set_reasoner(fo2solver). `````` Jens Claßen committed May 02, 2019 237 ``````2. **Model Checker** `````` Jens Claßen committed Mar 06, 2015 238 239 `````` To use verification based on abstraction and model checking, we `````` Jens Claßen committed Feb 16, 2018 240 `````` require that the 'nusmv' executable is visible in PATH. The system `````` Jens Claßen committed Mar 06, 2015 241 `````` has been developed and tested with the (currently) most recent `````` Jens Claßen committed Oct 05, 2020 242 `````` version 2.6.0, which can be downloaded from `````` Jens Claßen committed Mar 06, 2015 243 244 245 246 247 248 `````` http://nusmv.fbk.eu and installed manually according to the installation instructions given there. `````` Jens Claßen committed May 02, 2019 249 250 `````` So far, NuSMV is the only model checker supported. `````` Jens Claßen committed Apr 30, 2019 251 ``````3. **Graphviz/dot** `````` Jens Claßen committed Mar 06, 2015 252 `````` `````` Jens Claßen committed Nov 02, 2015 253 254 255 256 257 `````` To visualize some of the graph structures created during verification, there are predicates to generate corresponding .dot files in the temp directory. An image file can then be generated for example using `````` Jens Claßen committed Apr 30, 2019 258 `````` \$ dot -Tpng prop_trans.dot -o prop_trans.png `````` Jens Claßen committed Sep 07, 2015 259 `````` `````` Jens Claßen committed Apr 30, 2019 260 ``````4. **JPL (bidirectional Prolog/Java interface)** `````` Jens Claßen committed Sep 07, 2015 261 `````` `````` Jens Claßen committed May 02, 2019 262 263 264 265 `````` For some purposes such as the visualization applet for the Wumpus world, the Prolog->Java interface provided by the JPL library is needed. Typically, JPL does not have to be installed manually: Under Windows, it is already contained in the SWI-Prolog `````` Jens Claßen committed Sep 07, 2015 266 267 268 `````` distribution; under some Linuxes such as Ubuntu, it can be installed through the package manager via `````` Jens Claßen committed Apr 30, 2019 269 `````` \$ sudo apt-get install swi-prolog-java `````` Jens Claßen committed Sep 07, 2015 270 271 272 273 274 275 `````` For JPL to function properly, the LD_LIBRARY_PATH environment variable should be modified so that it contains directories that contain libjava.so, libjni.so, libjsig.so, and maybe some other Java libraries. For example, this can be achieved via `````` Jens Claßen committed Apr 30, 2019 276 `````` \$ export LD_LIBRARY_PATH=/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/amd64/server/ `````` Jens Claßen committed Sep 07, 2015 277 `````` `````` Jens Claßen committed Aug 04, 2017 278 279 `````` (where the specific path and Java version may differ for your system). `````` Jens Claßen committed Sep 07, 2015 280 `````` `````` Jens Claßen committed Apr 30, 2019 281 ``````5. **The Konclude Description Logic (OWL 2) Reasoner** `````` Jens Claßen committed Sep 07, 2015 282 283 `````` To use description logic reasoning, we require that the 'Konclude' `````` Jens Claßen committed Feb 16, 2018 284 `````` executable is visible in PATH. The system has been developed and `````` Jens Claßen committed Sep 07, 2015 285 `````` tested with the (currently) most recent version `````` Jens Claßen committed Oct 05, 2020 286 `````` v0.6.2. Konclude can be obtained at `````` Jens Claßen committed Sep 07, 2015 287 `````` `````` Jens Claßen committed Apr 30, 2019 288 `````` http://www.derivo.de/products/konclude.html `````` Jens Claßen committed Sep 07, 2015 289 290 291 `````` as 64-bit binary for Windows, Linux and MacOS X, both in statically and dynamically linked form. Its source code is published under the `````` Jens Claßen committed Sep 07, 2015 292 `````` LGPL. `````` Jens Claßen committed Feb 16, 2018 293 `````` `````` Jens Claßen committed Jul 26, 2020 294 295 296 297 298 299 300 301 302 303 304 305 306 ``````6. **The Fast Downward PDDL Planner** To use PDDL planning, we require that 'fast-downward.py' is visible in PATH and executable (meaning Python and all dependencies are installed). Instructions for obtaining and running Fast Downward are available at http://www.fast-downward.org/ Fast Downward will be run using the default configuration using `--alias lama-first`. So far, Fast Downward is the only PDDL planner supported. `````` Jens Claßen committed May 02, 2019 307 308 309 310 311 312 313 314 ``````## References 1. Jens Claßen:
**Symbolic Verification of Golog Programs with First-Order BDDs.**
In *Proc. KR*, 2018. [[PDF]](http://jens-classen.net/pub/Classen2018.pdf) 2. Benjamin Zarrieß and Jens Claßen:
`````` Jens Claßen committed May 03, 2019 315 `````` **Verifying CTL\* Properties of Golog Programs over Local-Effect `````` Jens Claßen committed May 02, 2019 316 317 318 319 320 321 322 323 `````` Actions.**
In *Proc. ECAI*, 2014. [[PDF]](http://www.jens-classen.net/pub/ZarriessClassen2014b.pdf) 3. Jens Claßen, Martin Liebenberg, Gerhard Lakemeyer, and Benjamin Zarrieß:
**Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs.**
`````` Jens Claßen committed May 03, 2019 324 `````` In *Proc. AAAI*, 2014. `````` Jens Claßen committed May 02, 2019 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 `````` [[PDF]](http://www.jens-classen.net/pub/ClassenEtAl2014.pdf) 4. Jens Claßen:
**Planning and Verification in the Action Language GOLOG.**
PhD Thesis, RWTH Aachen University, 2013. [[Fulltext](http://publications.rwth-aachen.de/record/229059/)] 5. Jens Claßen and Gerhard Lakemeyer:
**A Logic for Non-Terminating Golog Programs.**
In *Proc. KR*, 2008. [[PDF]](http://jens-classen.net/pub/ClassenLakemeyer2008.pdf) 6. Jens Claßen and Gerhard Lakemeyer:
**Foundations for Knowledge-Based Programs using ES.**
In *Proc. KR*, 2006. [[PDF]](http://jens-classen.net/pub/ClassenLakemeyer2006a.pdf)``````