README.md 11.9 KB
Newer Older
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: <br/>
> **Planning and Verification in the Action Language GOLOG.** <br/>
> 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
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
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
47
known about the world state or what the next action should be. We thus
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
70

71
    $ export PATH_GOLOG=/home/user/vergo/
72

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
76
corresponding [papers](#references).
77

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's avatar
Jens Claßen committed
84
SWI-Prolog and consult the file:
85

Jens Claßen's avatar
Jens Claßen committed
86
    ?- [coffee_bat_fct].
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's avatar
Jens Claßen committed
104
SWI-Prolog, and consult the file containing the action theory:
105

106
    ?- [dish_robot_bat].
107
108

Next, start the construction of the abstract transition system via
109

Jens Claßen's avatar
Jens Claßen committed
110
    ?- compute_abstraction(main).
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
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.

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's avatar
Jens Claßen committed
139
- lib:
140

Jens Claßen's avatar
Jens Claßen committed
141
  Various libraries (utilities, environment variables).
142

143
- logic:
144

145
  Various modules for representing and manipulating logical formulas,
Jens Claßen's avatar
Jens Claßen committed
146
  e.g. (first-order) BDD representation, and the closed-world and
147
  unique names assumptions.
Jens Claßen's avatar
Jens Claßen committed
148

149
150
151
152
- planning:

  Planning related code such as PDDL parser.

Jens Claßen's avatar
Jens Claßen committed
153
154
155
- projection:

  Code implementing regression and progression methods.
156
157
158
  
- reasoners:

159
  Contains different implementations and interfaces for backend
160
  reasoners (FOL, FO^2, Description Logics, System Z).
161
162
163
164
165
166
167
168
169

- temp:

  Temporary files are put here.

- verification:

  Contains implementations of different verification methods.

170
## Dependencies
171

172
Vergo uses SWI-Prolog (currently version 8.3.8). Furthermore, there
173
are the following dependencies to external tools and systems:
174

175
1. **Theorem Prover** (required)
176

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's avatar
Jens Claßen committed
180
   1. E Prover
181

Jens Claßen's avatar
Jens Claßen committed
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
186

Jens Claßen's avatar
Jens Claßen committed
187
      http://www.eprover.org 
188

Jens Claßen's avatar
Jens Claßen committed
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
192

Jens Claßen's avatar
Jens Claßen committed
193
          $ sudo yum install E.x86_64
194

Jens Claßen's avatar
Jens Claßen committed
195
   2. Vampire
196

Jens Claßen's avatar
Jens Claßen committed
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
201

Jens Claßen's avatar
Jens Claßen committed
202
      https://vprover.github.io/index.html    
203

Jens Claßen's avatar
Jens Claßen committed
204
      Then call
205

Jens Claßen's avatar
Jens Claßen committed
206
          ?- fol:set_reasoner(vampire).
207
208
209
210

   3. FO²-Solver

      Verification based on abstraction and model checking relies on
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
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/

233
234
235
236
      Then call

          ?- fol:set_reasoner(fo2solver).

237
2. **Model Checker**
238
239

   To use verification based on abstraction and model checking, we
240
   require that the 'nusmv' executable is visible in PATH. The system
241
   has been developed and tested with the (currently) most recent
242
   version 2.6.0, which can be downloaded from
243
244
245
246
247
248

   http://nusmv.fbk.eu

   and installed manually according to the installation instructions
   given there.

249
250
   So far, NuSMV is the only model checker supported.

251
3. **Graphviz/dot**
252

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

258
       $ dot -Tpng prop_trans.dot -o prop_trans.png
259

260
4. **JPL (bidirectional Prolog/Java interface)**
261

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
266
267
268
   distribution; under some Linuxes such as Ubuntu, it can be
   installed through the package manager via

269
       $ sudo apt-get install swi-prolog-java
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

276
       $ export LD_LIBRARY_PATH=/usr/lib/jvm/java-7-openjdk-amd64/jre/lib/amd64/server/
277

278
279
   (where the specific path and Java version may differ for your
   system).
280

281
5. **The Konclude Description Logic (OWL 2) Reasoner**
282
283

   To use description logic reasoning, we require that the 'Konclude'
284
   executable is visible in PATH. The system has been developed and
285
   tested with the (currently) most recent version
286
   v0.6.2. Konclude can be obtained at
287

288
   http://www.derivo.de/products/konclude.html
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's avatar
Jens Claßen committed
292
   LGPL.
293

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.

307
308
309
310
311
312
313
314
## References

1. Jens Claßen: <br/>
   **Symbolic Verification of Golog Programs with First-Order BDDs.** <br/>
   In *Proc. KR*, 2018.
   [[PDF]](http://jens-classen.net/pub/Classen2018.pdf)

2. Benjamin Zarrieß and Jens Claßen: <br/>
315
   **Verifying CTL\* Properties of Golog Programs over Local-Effect
316
317
318
319
320
321
322
323
   Actions.** <br/>
   In *Proc. ECAI*, 2014.
   [[PDF]](http://www.jens-classen.net/pub/ZarriessClassen2014b.pdf)

3. Jens Claßen, Martin Liebenberg, Gerhard Lakemeyer, and Benjamin
   Zarrieß: <br/>
   **Exploring the Boundaries of Decidable Verification of
   Non-Terminating Golog Programs.** <br/>
Jens Claßen's avatar
Jens Claßen committed
324
   In *Proc. AAAI*, 2014.
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: <br/>
   **Planning and Verification in the Action Language GOLOG.** <br/>
   PhD Thesis, RWTH Aachen University, 2013.
   [[Fulltext](http://publications.rwth-aachen.de/record/229059/)]
   
5. Jens Claßen and Gerhard Lakemeyer: <br/>
   **A Logic for Non-Terminating Golog Programs.** <br/>
   In *Proc. KR*, 2008.
   [[PDF]](http://jens-classen.net/pub/ClassenLakemeyer2008.pdf)

6. Jens Claßen and Gerhard Lakemeyer: <br/>
   **Foundations for Knowledge-Based Programs using ES.** <br/>
   In *Proc. KR*, 2006.
   [[PDF]](http://jens-classen.net/pub/ClassenLakemeyer2006a.pdf)