Goal-Conflict Detection based on Temporal Satisfiability Checking

ASE 2016

Here we provide the tool, all case studies and a brief description to reproduce the experiments reported in the paper Goal-Conflict Detection based on Temporal Satisfiability Checking recently published in ASE 2016.

The Tool and Case Studies

Please find here (ase2016.zip) all the case studies and the tool to reproduce the experiments reported in the paper.
The source of the tool that automates our tableau based goal conflict detection approach can be obtained from github.

Reproduce the Experiments

We provide support for Mac OS and Linux, running the correspoding script: "run-mac.sh" and "run-linux.sh". The difference yields in the Satisfiability Checker for LTL that the tool integrates, depending on the OS selected. On Linux, we use Aalta, while on Mac OS we use pltl.

The tool takes two arguments:

  • (1) the path to the file containing the LTL specification of goals and domain properties, and
  • (2) the path where the computed conflicts will be stored.
For instance: ./run-mac.sh case-studies/tcp.ltl conflicts/tcp

If you have any issue with the tool, please e-mail me to rdegiovanni@dc.exa.unrc.edu.ar.

If you use any of the examples provided here, please cite the corresponding paper.