Skip to content
Vergo: A Verification System for GOLOG Programs
Prolog
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
agents
examples
lib
logic
projection
reasoners
temp
tools
transfinal
verification
LICENSE
README.md

README.md

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]

and was continued during the VERITAS project on Verification of Non-Terminating Action Programs within the research unit on Hybrid Reasoning for Intelligent Systems funded by the German Science Foundation (DFG).

While other GOLOG implementations such as Reiter's original prototype, IndiGolog or Readylog 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 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 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 known about the world state or what the next action should be. We thus 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.

Getting Started

Vergo requires a recent version of SWI-Prolog as well as at least one FOL theorem prover being installed (see dependencies below). The environment variable PATH_GOLOG should then point to the root directory of this software, e.g. via

$ export PATH_GOLOG=/home/user/vergo/

There currently is no elaborate documentation. Instead, we encourage the interested reader to study the sources and look at the provided examples. The underlying algorithms are discussed in the corresponding papers.

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 SWI-Prolog and consult the main file:

?- [main_fct].

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 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 SWI-Prolog and consult the main file:

?- [main_abstraction].

Next, start the construction of the abstract transition system via

?- compute_abstraction(main)

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

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.

  • lib:

    Various libraries (utilities, environment variables).

  • logic:

    Contains code for representing and manipulating formulas in different base logics (propositional logic, FOL, L).

  • projection:

    Code implementing regression and progression methods.

  • reasoners:

    Contains different implementations and interfaces for backend reasoners (FOL, FO^2, Description Logics).

  • temp:

    Temporary files are put here.

  • tools:

    Conversion tools such as PDDL parser.

  • transfinal:

    Contains various definitions for Golog program semantics.

  • verification:

    Contains implementations of different verification methods.

Dependencies

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

  1. Theorem Prover (required)

    In order to be able to use FOL theorem proving, we require that at least one theorem prover is available.

    1. E Prover

      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

      http://www.eprover.org

      and installed manually. For some distributions such as Fedora, there are also prepackaged versions. Installation on Fedora then for example is via

      $ sudo yum install E.x86_64
      
    2. Vampire

      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

      https://vprover.github.io/index.html

      Then call

      ?- fol:set_reasoner(vampire).
      
    3. FO²-Solver

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

      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/
      

      Then call

      ?- fol:set_reasoner(fo2solver).
      
  2. Model Checker

    To use verification based on abstraction and model checking, we require that the 'nusmv' executable is visible in PATH. The system has been developed and tested with the (currently) most recent version 2.5.4, which can be downloaded from

    http://nusmv.fbk.eu

    and installed manually according to the installation instructions given there.

    So far, NuSMV is the only model checker supported.

  3. Graphviz/dot

    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

    $ dot -Tpng prop_trans.dot -o prop_trans.png
    
  4. JPL (bidirectional Prolog/Java interface)

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

    $ sudo apt-get install swi-prolog-java
    

    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

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

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

  5. The Konclude Description Logic (OWL 2) Reasoner

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

    http://www.derivo.de/products/konclude.html

    as 64-bit binary for Windows, Linux and MacOS X, both in statically and dynamically linked form. Its source code is published under the LGPL.

References

  1. Jens Claßen:
    Symbolic Verification of Golog Programs with First-Order BDDs.
    In Proc. KR, 2018. [PDF]

  2. Benjamin Zarrieß and Jens Claßen:
    Verifying CTL* Properties of Golog Programs over Local-Effect Actions.
    In Proc. ECAI, 2014. [PDF]

  3. Jens Claßen, Martin Liebenberg, Gerhard Lakemeyer, and Benjamin Zarrieß:
    Exploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs.
    In Proc. AAAI, 2014. [PDF]

  4. Jens Claßen:
    Planning and Verification in the Action Language GOLOG.
    PhD Thesis, RWTH Aachen University, 2013. [Fulltext]

  5. Jens Claßen and Gerhard Lakemeyer:
    A Logic for Non-Terminating Golog Programs.
    In Proc. KR, 2008. [PDF]

  6. Jens Claßen and Gerhard Lakemeyer:
    Foundations for Knowledge-Based Programs using ES.
    In Proc. KR, 2006. [PDF]

You can’t perform that action at this time.