AD-query - A Tool for Answering Queries on Action Descriptions

Overview

AD-query is a Perl script that converts the action description written in a fragment of an action language C into a DLP program, runs the DLP solver DLV and parses its output to give answers to certain questions about the action description.

The questions that can be answered range from whether are certain queries violated, if the queries are contradictory themselves to getting exact answer to which states and transitions violate certain queries and how can this be amended.

A formal description of the tests performed can be found in the paper "Eiter et al. - Resolving conflicts in action descriptions." (ECAI-06). The implementation and examples are available as .tar.gz package for download in the files directory. You can also download singular files from the respective subdirectories within.

Recently a methodology for error classification in action descriptions using AD-query tests has been proposed in "Eiter et al. - Error Classification in Action Descriptions: A Heuristic Approach." (AAAI-08, in press). The data (domain descriptions and queries) used for its experimental evaluation is also available for download as a .tar.gz package: experiments.tar.gz.

This work is part of the project "Answer Set Programming for Reactive Planning and Execution Monitoring"

Publications

T. Eiter, E. Erdem, M. Fink, and J. Senko "Resolving conflicts in action descriptions.", In G. Brewka and S. Coradeschi and A. Perini and P. Tra Proceedings of the 17th Eureopean Conference on Artificial Intelligence (ECAI'2006), pages 367-371, 2006. (... .pdf)
T. Eiter, M. Fink, and J. Senko "A Tool for Answering Queries on Action Descriptions.", In M. Fisher et al., editors, Proceedings 8th European Conference on Logics in Artificial Intelligence (JELIA 2006), pages 473-476, 2006. (... .pdf)

Usage

AD-query can be invoked in the following way:

ad-query -TEST FILE1 FILE2 ... FILEn

TEST

This switch specifies the test to perform. To run test T3, use switch -T3. Currently we support tests D1..D4 and T1..T4:

`-T1`	Given a single possibility query, which states violate it?
`-T2`	Given a single necessity query, which transitions violate it?
`-T3`	Given a literal L, is it under-specified relative to some transition candidate for each possible initial state? This literal has to be specified by background knowledge `checkliteral(N,F,FP,FPP)` where N is negation, F literal name and FP and FPP its parameters (or 'dummy' if none)
`-T4`	Given a single possibility query, which transition candidates are under-specified?
`-D1`	Given multiple queries, are they contradictory?
`-D2`	Given a single necessity query, which causal laws violate it?
`-D3`	Given multiple queries, can they be satisfied without modifying existing rules? Please note that only laws in D_0 need to be present in the input.
`-D4`	Given multiple queries, do we need to modify existing rules to resolve conflict? Please note that only laws in D_0 need to be present in the input.

FILEx File which contains the description of rules, fluents, queries, actions or constraints. Any number of files can be used, and they are treated as one big file.

The answer to the test is printed on the standard output in a human readable form. To specify the constraints on initial or successor states (formulas $\psi$ and $\phi$ ) you can use the respective keywords in the input file.

Syntax of the input files

To describe actions and rules, we use a slightly modified C language. Each line has to start with a keyword, otherwise it is considered to be background knowledge and inserted directly to the DLV. The keywords used in the description are the following:

`action` `literal [requires condition].`	Every action literal has to be properly declared before its use. We can declare one literal on one line. The condition enables us to add type information, for example: `action move(X) requires box(X)`.
`fluent` `literal [requires condition].`	Similarily every fluent has to be defined.
`caused` `[-]literal [if ifpart] [after afterpart] [requires condition].`	This is used to describe a static or dynamic causal law. Static laws have empty afterparts. Condition enables us again to use variables in rules, e.g.: `caused -light(B) after break(B),light(B) requires bulb(B).`
`inertial` `[-]literal.`	This is a shortcut for an inertial rule of a single literal.
`possibly` `[-]literal[ after afterpart] [if ifpart].`	This is used to describe a possibility query.
`neccessarily` `[-]literal[ after afterpart] [if ifpart].`	And similarily for a neccessity query.
`initial` `[-]literal, ..., [-]literal.`	This is used to describe a formula $\phi$ used as a constraint on the state s in some of the tests. This formula is a conjunction of literals, which must be true in this state.
`successor` `[-]literal, ..., [-]literal.`	And the equivalent for $\psi$ and the state s'.

literal is an unique name of an atom or an action symbol.
ifpart, afterpart, condition are conjunctions of literals with possible parameters, separated with commas

In the current implementation, the literals can have at most 2 parameters (variables) and rules can have at most 3. For example we can use:

fluent on(B,L) requires block(B), location(L) or
caused on(B,L) after move(B,L), on(B,L2), L<>L2 requires block(B), location(L), location(L2).

Example Domains

'Bulb' example

Here we consider the lightbulb example, mentioned in our papers, and consisting of two fluents and single action. The transition diagram of the domain description is as follows:

To describe the lightbulb example for our tool, we have to specify input file as following:
To declare fluents and actions:

fluent light.
fluent broken.
action toggle.

Then to describe causal laws (1) and (2):

caused light after toggle, -light.
caused -light if broken.

And to describe inertial rule (3):

inertial light.
inertial -light.
inertial broken.
inertial -broken.

Then to specify the query we're running we have to add respective line: possibly -light after toggle if broken. necessarily -light after toggle if light. As some of the tests require that only one query is present in the input file, we will divide this description into three files bulb.in, bulb.pos and bulb.nec, where the .in file will contain all rules except last two, and the .pos and .nec files will contain the respective queries. You can find these three files in the examples archive along with the another example.

'Game' example

In this example we're describing a 'shell' game played with 3 shells or cups, where one of these shells hide a small ball. The dealer exchanges the positions of these shells, and the player tries to guess the position of the ball. In reality the dealer often cheats and this game is banned in many places.

We're going to model the action of cheating, where the position of ball after cheat can be anywhere. We will define position(X) for numbers 1,2,3, describing the valid positions of the ball, and a single fluent at(X) which describes where the ball is. A single action used is cheat. The rules used are following:

inertial at(X), -at(X). caused at(X) if at(X) after cheat. caused -at(X) if at(Y) after cheat, X!=Y.

Please note, that in this description, the ball cannot disappear from the table.

Each state can lead into a three different states: {at(1)},{at(2)},{at(3)}, except for a state {} which can lead to itself.

This example is described in file game.in also with a single possibility query which says that state {} is possible after executing action cheat.

'Blocksworld' example

In this example we will consider a typical blocksworld domain -- world consists of blocks and a table. It consists of a single fluent on(B,L) which describes that block B lies on location L (which can be either a block or the table), and a single action move(B,L) which describes moving a block B to location L.

For sake of a consistency check, we have added 2 new fluents to the domain -- legal which indicates that the current situation if consistent, and above(B,L) which is a transitive closure of on(B,L). Furthermore we added a nop action that does nothing.

Consistency checking is a bit problematic in C language, as we have to consider any initial state for the transitions. This means, that even our auxiliary fluents used for consistency checking can be guessed to be either true or false. In our implementation we're checking for consistency in these steps:

We check that every block is at exactly one location, and that location is not the block itself.
We check that no two blocks lie on the same block.
(At this point, the on relation describes either 'lines' of blocks rooted to the table or 'circles' of blocks not rooted to the table.)
We define the above relation as transitive closure of on relation. That means that if block is truly above another, then above holds, but not vice versa, due to the random guessing.
We detect the circles of block by checking for above(B,B) and eliminating such states as incosistent.
Now to make sure that above is exactly transitive closure of on relation we check for above(B1,B2) such that B1 and B2 are in different 'lines' of blocks.

Example Sessions

'Bulb' example

This session will show how the designer of an action description can use our tool for identifying and possible repair of inconsistencies in it. The example consists of 2 queries: a possibility query possibly -light after toggle if broken and a necessity query necessarily -light after toggle if light.
First, the designer wants to check whether a query is violated at all, so she runs test T1 to check the possibility query: home> ./ad-query -T1 bulb.in bulb.pos Test T1. Which states of T(D) violate q? INITIAL STATE: broken. -light. This acknowledges that this query is violated at a certain state. Then she checks the necessity query by test T2: home> ./ad-query -T2 bulb.in bulb.nec Test T2. Which transitions of T(D) violate q? INITIAL STATE: -broken. light. SUCCESSOR STATE: -broken. light. Also necessity query is broken by certain transition. She wonders whether the queries are contradictory (and no action description would satisfy both), and checks this by test D1: home> ./ad-query -D1 bulb.in bulb.nec bulb.pos Test D1. Is the set of queries Q contradictory relative to D? The set of queries is not contradictory. That's good, the description can be repaired somehow. An important question is whether just adding new rules is needed - for this she can use the test D4: home> ./ad-query -D4 bulb.in bulb.nec bulb.pos Test D4. Do we have to modify a set of dynamic causal laws D to resolve a conflict between D and Q? The conflict cannot be resolved without modifying D, due to these queries: Possibility query q2 is contradictory with the rest at state: broken. -light. So she needs to remove some of the existing rules. She wants to check whether the inertia rules can be kept intact - by using test D3 with modified domain description containing only inertia rules. This domain description will be stored in file bulb-rules.in: home> ./ad-query -D3 bulb-rules.in bulb.nec bulb.pos Test D3. Can we resolve a conflict between D and Q, without modifying a set of causal laws D? The conflict between D and Q can be resolved without modifying D. That's a good sign. Now she knows she needs to modify the causal law for sure, and does not have to modify inertia. To get some ideas for repair, she might check if the possibility query is violated due to underspecification by test T4: home> ./ad-query -T4 bulb.in bulb.pos Test T4. Which underspecified transitions are there for states that violate query q? INITIAL STATE: broken. -light. SUCCESSOR STATE: -broken. -light. UNDERSPECIFIED ATOMS: -broken. This information means she can add rule `caused -broken if -broken,-light after broken,-light' and the query wouldn't be violated anymore. Then she might check which causal rules are in conflict with necessity query using test D2: home> ./ad-query -D2 bulb.in bulb.nec Test D2. If D does not satisfy a particular necessity query q in Q, which dynamic causal laws in D violate q? LAWS: i1. i4. This information means that by removing inertia rules #1 and #4, the query would be satisfied. However this is not a solution the designer is looking for, therefore she has to think about a different solutions.

By using all tests, the designer found out which states and transitions are violating queries, got some information about what needs to be modified and also received some suggestions for these repairs. How to actually repair the description, is up to her.

Created and maintained by Jan Senko