In the reasoning about actions community, one of the most basic reasoning problems is the projection problem: the question whether a certain assertion holds after executing a sequence of actions. While undecidable for general action theories based on the situation calculus, the projection problem was shown to be decidable in two different restrictions of the situation calculus to theories formulated using description logics. In this paper, we compare our implementations of projection procedures for these two approaches on random testing data for several realistic application domains. Important contributions of this work are not only the obtained experimental results, but also the approach for generating test cases. By using patterns extracted from the respective application domains, we ensure that the randomly generated input data make sense and are not inconsistent.
The situation calculus (SC) [
For the DL-based action formalism introduced in [
For the SC-based action formalism introduced in [
Both approaches for solving the projection problem have been implemented. In this paper, we compare these implementations on random testing data for several realistic application domains. In addition to describing the obtained experimental results, this paper also sketches our approach for generating the test cases. By using typical patterns extracted from the respective application domains, we ensure that the randomly generated input data make sense and are not inconsistent.
The rest of the paper is organised as follows. After a short presentation of the two action formalisms and their respective approaches for solving the projection problem, the test case set-up is explained and the experimental results are presented. The paper concludes with a discussion of the results obtained and possible future work. 2
In this section, we explain the two approaches for deciding the projection problem
on an intuitive level. More details on the directly DL-based action formalism can
be found in [
We assume the reader to be familiar with basic notions of Description Logics
(DLs), which can e.g. be found in [
Formulated for DL-based action formalisms, the projection problem deals
with the following question: Given an initial ABox describing the initial state, a
TBox describing the domain constraints, and a sequence of actions, does a query,
i.e., an assertion, hold after executing the action sequence from the initial state?
In the following, we call the approach for solving the projection problem
introduced in [
In this paper, we will use examples from the logistics domain [
The action formalism [
{loaded(Box42, OurBoeing777)}/at(Box42, Singapore)}).
The pre-condition at(OurBoeing777, AirportJFK) ensures that this action is only applicable if OurBoeing777 is indeed at AirportJFK. The effect of this action, described by two conditional post-conditions, is that the box Box42 is no longer at NYC but at Singapore if it was loaded to OurBoeing777. This action is a simplified version of an action used in our experiments.
According to the semantics of DL actions defined in [
In [
Note that the reduction in [
This approach is based on Basic Action Theories (BATs) in the Situation
Calculus (SC) [
In the context of BATs in SC, regression is the act of converting the query
formula (which should hold after executing the action sequence) to a formula
that should hold in the initial situation by making use of the SSAs and the
domain constraints. In the regression approach used in this paper, solving the
projection problem in certain BATs based on a restricted first-order language,
called L, is reduced to solving the satisfiability problem in the Description Logic
ALCOU . This is done by imposing precise syntactic constraints on Reiter’s SSAs
to guarantee that after doing the logically equivalent transformations required by
regression, the resulting regressed formula remains in L, if the projection query
formula is in L. Instead of defining this approach in detail, which is not possible
due to space constraints, we illustrate it on an example. Detailed definitions can
be found in [
There is a PA axiom for each action that describes the pre-conditions for executing the action. For instance, the PA of the action fly looks as follows: Poss(fly(z1, z2, z3), S) = airplane(z1) ∧ airport(z2) ∧ airport(z3) ∧
at(z1, z2, S) ∧ (z2 6= z3) Similarly, there is one SSA per fluent that describes the conditions under which actions make the fluent true or false. This is the SSA of the fluent loaded: loaded(x, y, do(a, S)) = ∃z1.a = load(x, y, z1) ∧ ready(x, S) ∨
loaded(x, y, S) ∧ ¬(∃z1.a = unload(x, y, z1)) The domain constraints are basically acyclic TBox axioms, but written in the language L. An example would be the following:
object(x) ≡ box(x) ∨ luggage(x) The initial theory and the query are L sentences that are restricted such that they can be transformed into ALCOU -assertions. The following is an example of an initial theory DS0 and a query W .
DS0 = truck(T1) ∧ box(B1) ∧ location(L1) ∧ ∀x.(box(x) ⊃ loaded(x, T1))
W = loaded(B1, T1, do([load(B1, T1, L1), unload(B1, T2, L1)], S0)) Note that the action sequence is here viewed to be part of the query, whereas for the reduction approach it is given separately. 2.3
Both approaches solve the projection problem for an action formalism that is based on the DL ALCOU . The action sequence is in both cases a list of ground actions, i.e., they do not contain free variables. However, the actions considered in the regression approach are more general than the ones in the reduction approach. In fact, the actions of the latter approach are so-called local-effect actions, which can only effect changes for named individual (i.e., ones that are explicitly named by a constant symbol), whereas global-effect actions, which are allowed in the former approach, can also effect changes for unnamed individuals. For example, the action fly in the regression approach moves all objects loaded to the airplane from one city to the other, independent of whether these objects have a name or not. Its approximation in the reduction approach moves only objects that are explicitly mentioned by their name in the description of the action. Though this approximation may in principle lead to different answers for the projection problem, this never happened in our experiments.
Another difference are the languages in which the queries are formulated. In the reduction approach, only instance queries are considered, whereas the other approach formulates queries in a restricted first-order language, with explicit variables and (unguarded) quantification. However, for the queries considered in our experiments, we were able to use the universal role to bridge this gap.
Regarding the complexity of the projection problem, regression may take up to double exponential time and space, whereas the reduction approach takes polynomial space. However, this is the worst-case complexity of the approaches. The more expressive regression approach is assumed to hit this bound only in non-practical cases.
In the next section, we show how these approaches behave in practice by evaluating them on randomly generated input data that are modelled on patterns occurring in applications. 3
In order to evaluate the two approaches for solving the projection problem, we generated testing data inspired by several application domains. Of course, the representation of the input data is different for the two approaches. Basically, we generated the data for the regression approach, and then translated them into the format required by the reduction approach. As already mentioned, globaleffect actions are approximated by local effect actions that make changes to all the named individuals. Otherwise, the translation preserves the semantics of the action theory. To increase readability for DL-literate readers, we describe the translated input data rather than the SC-based ones. Also, we use the size of the translated input data as size of the input.
In general, a test case is divided into a fixed part and a varying part. The fixed part consists of descriptions of all available actions and an acyclic TBox describing the domain. The varying part consisting of the initial ABox, the query to be asked, and the action sequence.
Subsequently, we sketch one domain, the logistics domain, to give an impression about what kind of projection problems can be expressed and solved by the formalisms.5 The examples used above already gave an impression of how the domain looks like. It represents a simplified version of logistics planning. Various objects, e.g. boxes and luggage, can be transported by vehicles, such as airplanes and trucks, from one location to another.
More precisely, the fixed part is as follows. The acyclic TBox describes general facts about the domain. It contains the following axioms:
5 See http://www.cse.yorku.ca/~w2yehia/dl2012_results.html for further domains.
The initial ABox contains incomplete knowledge about the initial state. It states static facts like Airplane(OurBoeing777), Airport(AirportJFK), Box(Box42), Truck(OurTruck), City(NYC), inCity(OurGarage, NYC), etc. In addition, the initial ABox contains dynamical knowledge like at(OurTruck, AirportJFK), Ready(Box42), loaded(Box127, OurBoeing777), which means that OurTruck is at AirportJFK, Box42 is ready to be loaded, and Box127 is loaded into OurBoeing777.
The action sequences are built using the atomic actions load, unload, fly, and driveTruck, instantiated with appropriate individuals. The action load loads an object into a vehicle at a location, e.g. load(Box42, OurBoeing777, AirportJFK) is an instance of this action. It is executable if both Box42 and OurBoeing777 are at AirportJFK, i.e., at(Box42, AirportJFK) and at(OurBoeing777, AirportJFK) hold, and Box42 is ready to be loaded, i.e., we have Ready(Box42). The action unload is defined analogously for unloading an object from a vehicle at a location. Executing the action fly means that an airplane flies from one airport to another one, e.g. fly(OurBoeing777, AirportJFK, AirportSIN). This action is executable if we have at(OurBoeing777, AirportJFK), and the two airports are not the same, which is the case in the example. The action driveTruck is similar. It is used to drive a truck from one location to another one. An example for such an action would be driveTruck(OurTruck, OurGarage, AirportJFK). Executing the action is only possible if OurGarage and AirportJFK are at the same city.
On the DL side, queries are instance queries, i.e., concept assertions of the form C(a) where C is a ALCOU -concept description built using the concept names and role names introduced above and a is an individual name such as Box42, AirportJFK, OurBoeing777, etc.
To properly test our implementations, we obviously need some sort of
automated generation of input data, but due to the non-trivial expressivity of the
language at hand, it is hard to generate useful test cases. We could not find
any precedence for such an attempt, i.e., generating random projection
problem test cases, in the literature. For planning domains [
We describe now more precisely how we generate the testing data. The TBox contains the axioms above plus some auxiliary axioms described below. The initial ABox contains both static knowledge and dynamical knowledge. For the static knowledge, it makes no sense to add incompleteness, because usually we know, for instance, that Box42 is a box. We omit, however, axioms stating facts like Box42 is not an airplane, i.e., ¬Airplane(Box42). The real incompleteness concerns the dynamical knowledge. We found it useful to generate more or less complete knowledge by generating a number of boxes, trucks, airplanes, airports, and cities together with static knowledge like in which city airports are located. We generate also assertions for the role names at, loaded and Ready for all individuals of the respective type. We add more incompleteness by removing assertions from the ABox and adding new assertions using the following transformation rules: a t-rule, and an ∃-rule. Applying the t-rule means to take two assertions A(a), B(a) and replacing them with the assertion (A t B)(a). For reasons of simplicity and interchangeability of the formats read by our implementations, we introduce a new concept name Aux, and add the concept definition Aux ≡ A t B to the TBox, and the assertion Aux(a) to the ABox.6 Applying the ∃-rule means to take a role assertion r(a, b) and to replace it with (∃r.>)(a). For example, at(Box127, AirportSIN) could be replaced with (∃at.>)(Box127). Instead of knowing that Box127 is at AirportSIN, we now just know that Box127 is somewhere, i.e., at a location. Again, we introduce a new concept name for ∃at.>, and add its definition to the TBox. Of course, it makes no sense to apply the rules too often since then the resulting ABox would be too incomplete. For this reason, we use them rather sparingly: roughly there are ten-times more individuals than the number of times these rules are applied.
The query and the action sequence are generated using (domain-specific) patterns. Building formulas from hand-made patterns occurring in real applications is one step towards generating realistic test cases, but it suffers from the fact that the generated formulas might be too similar, and thus the test cases do not provide the extensive coverage that random formula generation does. Thus, we mixed patterns with a bit of randomness. We developed ten patterns for the logistics domain. Some of these patterns can take input, and generate a random input if none is given. For example, a pattern might describe whether there are any boxes on a truck in some location. The input could be any combination of box, truck or location constants. If necessary, a missing constant can be randomly generated, or it could remain as a variable otherwise. The following formula Φ was generated from such a pattern, where the input was boxi and locationj . The generated formula is translated to the ALCOU -assertion α with aux being a dummy individual.
Φ = ∃y.(loaded(boxi, y) ∧ truck(y) ∧ at(y, locationj )) α = (∃U.({boxi} u ∃loaded.(Truck u ∃at.{locationj })))(aux) We use those simple but versatile patterns to generate formulas that replace the propositions in a randomly generated satisfiable formula of propositional logic in disjunctive normal form in order to obtain the query. Using this approach, it is ensured that we have more randomness at the propositional level and less randomness at the FOL level.
Finally, to generate random but executable action sequences, we used patterns again. But now a pattern is a generic description of a sequence of actions necessary to satisfy a goal. For instance, one action sequence in the logistics domain describes the process of gathering all known boxes in a particular city and transporting them to another city. The choice of the cities is random, and 6 Thus, the TBox contains also abbreviations for concepts, where the abbreviation occurs only once in the ABox. picking the transportation vehicle is random as well. On top of that, we compute this action sequence based on a random initial ABox. Of course, we could have tried to pick purely random actions, but then most of the generated action sequences would not have been executable (i.e., not all pre-conditions would be satisfied). Testing randomly generated action sequences for executability takes time and would result in having to throw away most of the generated sequences.
We now present the testing results we obtained for the logistics domain. The results were obtained on an Intel R CoreTM 2 Duo E8400 CPU with a clock frequency of 3.00 GHz, and 4 GB of RAM. We used JVM version 1.7.0. Both implementations use HermiT 1.3.6 as underlying DL reasoner.
To make the results better comparable, we generated a couple of initial theories, and then manually removed individuals from them to create new smaller initial theories. Then, we generated a set of queries and action sequences for each initial theory. This way, we can measure the running time for solving the projection problem as the ABox varies in size, while the query and action sequence stay the same. Some of the testing results for about 700 test cases that we obtained can be found in Tab. 1. These results give an impression of the performance of the two approaches. We sketched how the action sequences and the queries look like. Empty cells in Tab. 1 mean that the program could not finish within two minutes, which was our cut-off time. To be useful in practice, an answer within two minutes is preferred. For the regression approach, we also measured the time for computing the regressed formula only, which is usually quite small (about 0.01 s). Thus, the main time for the regression approach is used for checking the consistency of the generated knowledge base using HermiT. One can observe that the running times very much depend on the action sequence and the query that is asked. For action sequences of length 5 or more, both approaches seem to be struggling due to overhead taken by HermiT. Thus, improving DL-systems will improve the running time of our approaches significantly. Note that the last test case in Tab. 1 describes a rather simple scenario, which is still too complex for both approaches. One can observe also that the size of the initial ABox affects the running time. Note that the length of the regressed formula is not affected by these variations. Also, in most cases, a query involving a value restriction on U causes a longer running time for the reduction approach.
All in all, the testing done in this paper should be considered as a first step. More testing and a careful inspection of the structure of the input is needed to give an answer to the question which approach performs better on which inputs. 4
We have compared the implementations of two approaches for solving the projection problem for DL-based action formalisms. The main result of this comparison is twofold. First, it is clear that both approaches seem to be struggling when dealing with action sequences longer than five. It turned out that computing the regression formula can be done very quickly, and most of the time for the regression approach is consumed by the DL-reasoner. For the reduction approach, it is unload, load, unload (∃U.(Box u ∃loaded.Truck))(aux) unload, load, fly (∃U.({b} u ∃loaded.Truck))(aux) load, load, load, fly (∀U.(¬(∃at.{`} u Box) t
(∃loaded.{a})))(aux) unload, load, load, unload, unload (∀U.(¬(∃at.{`}) u Box) t Ready)(aux) unload, load, load, load, fly, unload,
unload, unload (∃U.({b} u ∃loaded.Truck))(aux) also clear that long action sequences cannot be handled efficiently since, in the worst case, the initial ABox is copied for each point in time. Also, we observed that the length of the action sequence is not the only metric that affects the running time. The size of the initial ABox as well as the form of the query are also important. We expect that more testing will give a more accurate description on what what are the weak points of the approaches. Maybe also the actions, i.e., the size and structure of the pre-conditions and the post-conditions, need to be considered in more detail. For the reduction approach, the pre-conditions affect the runtime in our experiments, while for regression they do not. As a result of these investigations, we hope to locate the parts of the implementations that need to be optimised.
The second main result is that we gained some experience in automatically generating testing data for the projection problem. It is clear that generating good test cases is not a trivial task (comparable to generating good test cases in programming languages). Randomly generating test cases on a purely syntactic level without taking the semantics of action formalisms into account is problematic since the resulting initial ABoxes can easily be inconsistent, the action sequences not executable, etc. In these cases, projection does not make sense. To take the semantics into account, we followed a domain specific approach, and used patterns found in applications to generate data that make sense from a semantic point of view. Nevertheless, these are only first step towards semantically well-founded test case generation. More versatile approaches need to be developed as future work.