Preliminaries
Definition 1.
A transition system is defined as where

is the set of states.

is the set of possible initial states.

is the set of possible actions.

is the transition function, returns the set of possible successor states after applying a possible action in the current state.
For any states , we say that there is a trajectory between and , denoted by for some action sequence where , if there exist such that and for all .
We will refer to this transition system as the original transition system. The constituents and are assumed to be finite in the rest of the paper. Note that, this transition system represents fully observable settings. Large environments cause high number of possibilities for states, which cause the transition systems to be large. Especially, if the environment is nondeterministic, the resulting transition system contains high amount of transitions between states, since one needs to consider all possible outcomes of executing an action.
Action Languages
Action languages describe a particular type of transition systems that are based on action signatures. An action signature consists of a set V of value names, a set F of fluent names and a set A of action names. Any fluent has a value in any state of the world.
A transition system of an action signature is similar to Defn. 1, where and corresponds to the relation . In addition, we have a value function , where shows the value of in state . A transition system can be thought as a labeled directed graph, where a state is represented by a vertex labeled with the function , that gives the value of the fluents. Every triple is represented by an edge leading from a state to a state and labeled by .
An action is executable at a state , if there is at least one state such that and is deterministic if there is at most one such state. Concurrent execution of actions can be defined by considering transitions in the form with a set of actions, where each action is executable at .
An action signature is propositional if its value names are truth values: . In this work, we confine to propositional action signatures.
The transition system allows one to answer queries about the program. For example, one can find a plan to reach a goal state from an initial state, by searching for a path between the vertices that represent these states in the transition system. One can express properties about the paths of the transition system by using an action query language.
Running Example: Search Scenarios
Consider a memoryless agent that can sense horizontally and vertically, in an unknown grid cell environment with obstacles, where a missing person needs to be found. Suppose we are given the action description of the agent with a policy of “always going to the farthest reachable point in visible distance (until a person is found)”. Following this reactive policy, the agent chooses its course of actions to reach the farthest reachable point, referred as target, from its current location with respect to its current knowledge about the environment. After executing the plan and reaching a state that satisfies the target, the decision process is reiterated and a new target, hence a new course of actions, is determined.
Given such a policy, one would want to check whether or not the agent can always find the person, in all instances of the environment. Note that we assume that the obstacles are placed in a way that the person is always reachable.
Figure 1 shows some possible instances for , where the square in a cell represents the agent and the dot represents the missing person. The course of actions determined by the policy in all the instances is to move to (3,1), which is the farthest reachable point, i.e. target. It can be seen that (a) is an instance where the person can be found with the given policy, while in (b) the agent goes in a loop and can’t find the person, since after reaching (3,1) it will decide to move to (1,1) again. In (c), after reaching (3,1) following its policy, the agent has two possible directions to choose, since there are two farthest points. It can either move to (3,3), which would result in seeing the person, or it can move back to (1,3), which would mean that there is a possibility for the agent to go in a loop.
Notice that our aim is different from finding a policy (i.e. global plan) that satisfies certain properties (i.e. goals) in an unknown environment. On the contrary, we assume that we are given a representation of a system with a certain policy, and we want to check what it is capable (or incapable) of.
Modeling Policies in Transition Systems
A reactive policy is described to reach some main goal, by guiding the agent through its interaction with the environment. This guidance can be done by determining the course of actions to bring about targets from the current situation, via externally computed plans. A transition system that models such policies should represent the flow of executing the policy, which is the agent’s actual trajectory in the environment following the policy. This would allow for verifying whether execution of a policy results in reaching the desired main goal, i.e. the policy works.
We define such a transition system by clustering the states into groups depending on a profile. A profile is determined by evaluating a set of formulas over a state that informally yield attribute (respectively feature) values; states with the same attribute values are clustered into one. The choice of formulas for determining profiles depends on the given policy or the environment one is considering. Then, the transitions between these clusters are defined according to the policy. The newly defined transitions are able to show the evaluation of the policy by a higher level action from one state to the next state. This next state satisfies the target determined by a target component, and the higher level action corresponds to the execution of an externally computed plan.
Having such a classification on states and defining higher level transitions between the states can help in reducing the state space or the number of transitions when compared to the original transition system. Furthermore, it aids in abstraction and allows one to emulate a modular hierarchic approach, in which a higher level (macro) action, expressed by a target, is realized in terms of a sequence of (micro) actions that is compiled by the external planner, which may use different ways (planning on the fly, resorting to scripts etc.)
State profiles according to the policy
We now describe a classification of states, which helps to omit parts of the state that are irrelevant with respect to the environment or the policy. This classification is done by determining profiles, and clustering the states accordingly.
Example 1.
Remember the possible instances from Figure 1 in the running example. Due to partial observability, the agent is unable to distinguish the states that it is in, and the unobservable parts are irrelevant to the policy. Now assume that there are fluents that hold the information of the agent’s location, the locations of the obstacles and the reachable points. One can determine a profile of the form “the agent is at (1,1), sees an obstacle at (1,3), and is able to reach to points at (1,2), (2,1), (3,1)” by not considering the remaining part of the environment that the agent can not observe. The states that have this profile can be clustered in one group as in Figure 2, where the cells with question marks demonstrate that they are not observable by the agent.
For partially observable environments, the notion of indistinguishable states can be used in the classification of states. The states that provide the same observations for the agent are considered as having the same profile. However, in fully observable environments, observability won’t help in reducing the state space. One needs to find other notions to determine profiles.
We consider a classification function, , where is the set of possible state clusters. This is a general notion applicable to fully and partially observable cases.
Definition 2.
An equalized state relative to the classification function is a state . The term equalized comes from the fact that the states in the same classification are considered as the same, i.e. equal.
To talk about a state that is clustered into an equalized state , we use the notation , where we identify with its preimage (i.e. the set of states that are mapped to according to ).
Different from the work by Son and Baral baral01 where they consider a “combinedstate” which consists of the real state of the world and the states that the agent thinks it may be in, we consider a version where we combine the real states into one state if they provide the same classification (or observation, in case of partial observability) for the agent. The equalization of states allows for omitting the details that are irrelevant to the behavior of the agent.
Transition systems according to the policy
We now define the notion of a transition system that is able to represent the evaluation of the policy on the state clusters.
Definition 3.
An equalized (higher level) transition system , with respect to the classification function , is defined as , where

is the finite set of equalized states;

is the finite set of initial equalized states, where if there is some such that holds;

is the finite set of possible targets relative to the behavior, where a target can be satisfied by more than one equalized state;

, is the target function that returns the possible targets to achieve from the current equalized state, according to the policy;

is the transition function according to the policy, referred to as the policy execution function, returns the possible resulting equalized states after applying the policy in the current equalized state.
The target function gets the equalized state as input and produces the possible targets to achieve. These targets may be expressed as formulas over the states (in particular, of states that are represented by fluents or state variables), or in some other representation. A target can be considered as a subgoal condition to hold at the followup state, depending on the current equalized state. The aim would be to intend to reach a state that satisfies the conditions of the target, without paying attention to the steps taken in between. That’s where the policy execution function comes into the picture.
The formal description of the policy execution function is as follows:
where is an outsourced function that returns a plan needed to reach a state that meets the conditions from the current equalized state :
where and gives the resulting states of executing a sequence of actions at a state :
where the state is an artifact state that does not satisfy any of the targets, and
Figure 3 demonstrates a transition in the equalized transition system. The equalized states may contain more than one state that has the same profile. Depending on the current state, , the policy chooses the next target, , that should be satisfied. There may be more than one equalized state satisfying the same target. The policy execution function finds a transition into one of these equalized states, , that is reachable from the current equalized state. The transition is considered as a big jump between states, where the actions taken and the states passed in between are omitted.
Notice that we assume that the outsourced function is able to return conformant plans that guarantee to reach a state that satisfies the determined targets. In particular, may also contain only one action. For practical reasons, we consider to be able to return a subset of all conformant plans. The maximal possible , where we have equality, is denoted with .
Consider the case of uncertainty, where the agent requires to do some action, e.g. , in order to get further information about its state. One can define the target function to return as target a dummy fluent to ensure that the action is made, e.g. , and given this target, the function can return the desired action as the plan. The nondeterminism or partial observability of the environment is modeled through the set of possible successor states returned by .
The generic definition of the equalized transition system allows for the possibility of representing wellknown concepts like purely reactive systems or universal planning [Cimatti, Riveri, and Traverso1998a]. To represent reactive systems, one can describe a policy of “pick some action”. This way one can model reactive systems that do not do reasoning, but immediately react to the environment with an action. As for the exactly opposite case, which is finding a plan that guarantees reaching the goal, one can choose the target as the main goal. Then, the would have the difficult task of finding a universal plan or a conformant plan that reaches the main goal. If however, one is aware of such a plan, then it is possible to mimic the plan by modifying the targets and the target function in a way that at each point in time the next action in the plan is returned by , and the corresponding transition is made. For that, one needs to record information in the states and keep track of the targets.
As the function is outsourced, we rely on an implementation that returns conformant plans for achieving transitions in the equalized transition systems. This naturally raises the issue of whether a given such implementation is suitable, and leads to the question of soundness (only correct plans are output) and completeness (some plan will be output, if one exists). We next assess how expensive it is to test this, under some assumptions about the representation and computational properties of (equalized) transition systems, which will then also be used for assessing the cost of policy checking.
Assumptions
We have certain assumptions on the representation of the system. We assume that given a state which is implicitly given using a binary encoding, the cost of evaluating the classification , the (original) transition for some action , and recognizing the initial state, say with , is polynomial. The cost could also be in NP, if projective (i.e. existentially quantified) variables are allowed. Furthermore, we assume that the size of the representation of a “target” in is polynomial in size of the state, so that given a string, one can check in polynomial time if it is a correct target description . This test can also be relaxed to be in NP by allowing projective variables.
Given these assumptions, we have the following two results. These results show the cost of checking whether an implementation of that we have at hand is sound (delivers correct plans) and in case does not skip plans (is complete); we assume here that testing whether is feasible in (this is the cost of verifying conformant plans, and we may assume that is no worse than a naive guess and check algorithm).
Theorem 1 (soundness of ).
Let be a transition system with respect to a classification function . The problem of checking whether every transition found by the policy execution function induced by a given implementation is correct is in .
Proof (Sketch).
According to the definition of the policy execution function, every transition from a state to some state corresponds to some plan returned by . Therefore, first one needs to check whether each plan returned by given some and is correct. For that we need to check two conditions on the corresponding trajectories of the plan:

for all partial trajectories it holds that for the upcoming action from the plan , (i.e. the action is applicable)

for all trajectories , .
Checking whether these conditions hold is in .
Thus, to decide whether for some state and target the function does not work correctly, we can guess (resp. ), and a plan and verify that and that is not correct. As the verification is doable with an oracle for in polynomial time, a counterexample for correctness can be found in ; thus the problem is in . ∎
The complexity is lower, if output checking of has lower complexity (in particular, it drops to if output checking is in coNP).
The result for soundness of is complemented with another result for completeness with respect to short (polynomial size) conformant plans that are returned by .
Theorem 2 (completeness of ).
Let be a transition system with respect to a classification function . Deciding whether for a given implementation , fulfills whenever a short conformant plan from to exists in , is in .
Proof (Sketch).
For a counterexample, we can guess some and (resp. , ) and some short plan and verify that (i) is a valid conformant plan in to reach from , and (ii) that a target exists such that produces some output. We can verify (i) using a oracle to check that is a conformant plan, and we can verify (ii) using a oracle (for all guesses of targets and short plans , either is not a target for or is not produced by ). This establishes membership in . ∎
As in the case of soundness, the complexity drops if checking the output of is lower (in particular, to if the output checking is in coNP).
We also restrict the plans that are returned by to have polynomial size. This constraint would not allow for exponentially long conformant plans (even if they exist). Thus, the agent is forced under this restriction to develop targets that it can reach in polynomially many steps, and then to go on from these targets. Informally, this does not limit the capability of the agent in general. The “long” conformant plans can be split into short plans with a modified policy and by encoding specific targets into the states.
We denote the main goal that the reactive policy is aiming for by . Our aim is to have the capability to check whether following the policy always results in reaching some state that satisfies the main goal. That is, for each run, i.e. sequence such that and , for all , there is some such that . (The behavior could be easily modified to stop or to loop in any state that satisfies the goal.) This way we can say whether the policy works or not. Under the assumptions from above, we obtain the following
Theorem 3.
The problem of determining that the policy works is in PSPACE.
Proof (Sketch).
One needs to look at all runs from every initial state in the equalized transition system and check whether each such run has some state that satisfies the main goal . Given that states have a representation in terms of fluent or state variables, there are at most exponentially many different states. Thus to find a counterexample, a run of at most exponential length in which is not satisfied is sufficient. Such a run can be nondeterministically built in polynomial space; as NPSPACE PSPACE, the result follows. ∎
Note that in this formulation, we have tacitly assumed that the main goal can be established in the original system, thus at least some trajectory from some initial state to a state fulfilling the goal exists (this can be checked in PSPACE as well). In a more refined version, we could define the working of a policy relative to the fact that some abstract plan would exist that makes true; naturally, thus may impact the complexity of the policy checking.
Above, we have been considering arbitrary states, targets and transitions in the equalized transition system. In fact, for the particular behavior, only the states that can be encountered in runs really matter; these are the reachable states defined as follows.
Definition 4.
A state is reachable from an initial state in the equalized transition system if and only if for some where is defined as follows.
Under the assumptions that apply to the previous results, we can state the following.
Theorem 4.
The problem of determining whether a state in an equalized transition system is reachable is in PSPACE.
The notions of soundness and completeness of an outsourced planning function could be restricted to reachable states; however, this, would not change the cost of testing these properties in general (assuming that is decidable with sufficiently low complexity).
Constraining equalization
The definition of allows for certain transitions between equalized states that don’t have corresponding concrete transitions in the original transition system. However, the aim of defining such an equalized transition system is not to introduce new features, but to keep the structure of the original transition system and discard the unnecessary parts with respect to the policy. Therefore, one needs to give further restrictions on the transitions of the equalized transition system, in order to obtain the main objective.
Let us consider the following condition
(1) 
This condition ensures that a transition between two states in the equalized transition system represents that any state in has a transition from some state in . An equalization is called proper if condition (1) is satisfied.
Theorem 5.
Let be a transition system with respect to a classification function . Let be the transition function that the policy execution function is based on. The problem of checking whether is proper is in .
Proof (sketch).
As a counterexample, one needs to guess and such that no has . ∎
The results in Theorems 15 are all complemented by lower bounds for realistic realizations of the parameters (notably, for typical action languages such as fragments of ).
The following proposition is based on the assumption that the transition function satisfies condition (1).
Proposition 1 (soundness).
Let be a transition system with respect to a classification function . Let be equalized states that are reachable from some initial states, and . Then for any concrete state there is a concrete state such that for some action sequence , in the original transition system.
Proof.
For equalized states , having means that satisfies a goal condition that is determined at , and is reachable via executing some plan . With the assumption that (1) holds, we can apply backwards tracking from any state following the transitions corresponding to the actions in the plan backwards. In the end, we can find a concrete state from which one can reach the state by applying the plan in the original transition system. ∎
Thus, we can conclude the following corollary, with the requirement of only having initial states clustered into the equalized initial states (i.e. no “noninitial” state is mapped to an initial equalized state). Technically, it should hold that .
Corollary 1.
If there is a trajectory in the equalized transition system with initial state clustering from an equalized initial state to , then it is possible to find a trajectory in the original transition system from some concrete initial state to .
We want to be able to study the reactive policy through the equalized transition system. In case the policy does not work as expected, there should be trajectories that shows the reason of the failure. Knowing that any such trajectory found in the equalized transition system exists in the original transition system is enough to conclude that the policy indeed does not work.
Current assumptions can not avoid the case where a plan returned by on the equalized transition system does not have a corresponding trajectory in the original transition system. Therefore, we consider an additional condition as
(2) 
that strengthens the properness condition (1). Under this condition, every plan returned by can be successfully executed in the original transition system and will establish the target . However, still we may lose trajectories of the original system as by clustering states they might not turn into conformant plans. Then one would need to modify the description of determining targets, i.e. the set of targets and the function .
Example 2.
Remember the environment and the policy described in the running example, and consider the scenario shown in Figure 4(a). It shows a part of the equalized transition system constructed according to the policy. The states that are not distinguishable due to the partial observability are clustered into the same state.
The policy is applied according to current observations, and the successor states show the possible resulting states. The aim of the policy is to have the agent move to the farthest reachable point, which for is . As expected, there can be several states that satisfy the target . The successor states of is determined by computing the possible resulting states after executing the plan returned by . Considering that the agent will gain knowledge about the environment while moving, there are several possibilities for the resulting state.
Notice that this notion of a transition system can help in reducing the number of states, due to the fact that it is able to disregard states with information on fluents that does not have any effect on the system’s behavior. For example, Figure 4(b) shows a case where the unknown parts behind the obstacles are not relevant to the agent’s behavior, i.e. the person can be found nonetheless.
Relation with Action Languages
In this section, we describe how our definition of a higherlevel transition system that models the behavior can fit into the action languages. Given a program defined by an action language and its respective (original) transition system, we now describe how to model this program following a reactive policy and how to construct the corresponding equalized transition system according to the policy.
Classifying the state space
The approach to classify the (original) state space relies on defining a function that classifies the states. There are at least two kinds of such classification; one can classify the states depending on whether they give the same values for certain fluents and omit the knowledge of the values of the remaining fluents, or one can introduce a new set of fluents and classify the states depending on whether they give the same values for the new fluents:

Type 1: Extend the set of truth values by , where denotes the value to be unknown. Extend the value function by . Then, consider a new set of groups of states, , where a group state contains all the states that give the same values for all , i.e. . The value function for the new group of states is .

Type 2: Consider a new set of (auxiliary) fluent names , where each fluent is related with some fluents of F. The relation can be shown with a mapping . Then, consider a new set of groups of states, , where a group state contains all the states that give the same values for all , i.e. . The value function for the new group of states is .
We can consider the states in the same classification to have the same profile, and the classification function as a membership function that assigns the states into groups.
Remarks:
(1) In Type 1, introducing the value unknown for the fluents allows for describing sensing actions and knowing the true value of a fluent at a later state. Also, one needs to give constraints for a fluent to have the unknown value. e.g. it can’t be the case that a fluent related to a grid cell is unknown while the robot is able to observe it.
(2) In Type 2, one needs to modify the action descriptions according to the newly defined fluents and define abstract actions. However, in Type 1, the modification of the action definitions is not necessary, assuming that the actions are defined in a way that the fluents that are used when determining an action always have known values.
Once a set of equalized states is constructed according to the classification function, one needs to define the reactive policy to determine the transitions. Next, we describe how a policy can be defined from an abstract point of view, through a target language which figures out the targets and helps in determining the course of actions, and show how the transitions are constructed.
Defining a target language
Let denote the set of fluents that the equalized transition system is built upon. Let denote the set of formulas in an abstract language that can be constructed over .
We consider a declarative way of finding targets. Let be the set of formulas that describe target determination. Let denote the set of possible targets that can be determined via the evaluation of the formulas over the related fluents in the equalized states.
Notice that separation of the target determining formulas and the targets is to allow for outsourced planners that are able to understand simple target formulas. These planners do not need to know about the target language in order to find plans. However, if one is able to use planners that are powerful enough, then the target language can be given as input to the planner, so that the planner determines the target and finds the corresponding plan.
To define a relation between and , we introduce some placeholder fluents. Let be the set of target formulas. Consider a new set of fluents where each of the formulas in is represented by some fluent. The value of a fluent depends on whether its respective formula is satisfied or not, i.e. for a state , . Now consider a mapping where
means that if there is a state such that , and for the remaining formulas , then in the successor state of , for some , should hold. We consider the output of to be a set of targets in order to represent the possibility of nondeterminism in choosing a target.
Transition between states
The transition for the equalized transition system can be denoted with , where corresponds to the policy execution function that uses (a) the target language to determine targets, (b) an outsourced planner (corresponding to the function ) to find conformant plans and (c) the computation of executing the plans (corresponding to the function ). The outsourced planner finds a sequence of actions from an equalized state to one of its determined targets . Then the successor equalized states are computed by executing the plan from . Transition shows the resulting states after applying the policy.
Example 3.
Let us consider a simple blocksworld example where a policy (of two phases) is defined as follows:

if at phase 1 and not all the blocks are on the table, move one free block on a stack with highest number of blocks to the table.

if all the blocks are on the table, move to phase 2.

if at phase 2 and not all the blocks are on top of each other, move one of the free blocks on the table on top of the stack with more than one block (if exists any, otherwise move the block on top of some block).
Since the policy does not take blocks’ labels into consideration, a classification can be of the following form for number of blocks: We introduce an tuple to denote equalized states such that for , would represent the number of stacks that have blocks. For example, for blocks, a state where would represent all the states in the original transition system with the profile “contains a stack of 1 block and a stack of 3 blocks”. Notice that in the original transition system for 4 labeled blocks, there are 24 possible states that have this profile and if the blocks need to be in order, then there are 4 possible states.
Figure 5 demonstrates the corresponding equalized transition system for the case of blocks. The equalized transition system for this example is in the following form:

is the set of equalized states according to the abstraction as described above.

is the initial equalized states (all elements of except ).

, since the policy is related with all the blocks, it can determine targets as the whole states.

is the target function.

is the policy execution function, returning the resulting successor state after applying one action desired by the behavior, shown as in Figure 5.
Application on Action Language
In this section, we describe how one can construct an equalized transition system for a reactive system that is represented using the action language [Giunchiglia and Lifschitz1998]. First, we give some background information about the language , then move on to the application of our definitions.
Syntax
A formula is a propositional combination of fluents.
Given a propositional action signature , whose set E of elementary action names is disjoint from F, an action description is a set of expressions of the following forms:

static laws:
(3) where and are formulas that do not contain elementary actions;

dynamic laws:
(4) where and are as above, and is a formula.
Semantics
The transition system described by an action description is defined as follows:

is the set of all interpretations of F such that, for every static law (3) satisfies if satisfies ,

i.e. identify with
We focus on a fragment of the language where the heads of the static and dynamic laws only consist of literals. This restriction on the laws reduces the cost of evaluating the transitions to polynomial time. Thus, we match the conditions on complexity from above. Furthermore, by wellknown results on the complexity of action language [Turner2002, Eiter et al.2004] all the results in Theorems 15 can be turned into completeness results already for this fragment.
Defining a policy
Let be the set of fluents that are relevant to the policy. The target language is defined explicitly via static laws using the fluents in , denoted , where a target is determined by the evaluation of these formulas in a state.
Example 4.
An example of a target language for the running example uses causal laws from :
where consists of all atoms and for .
The target of a state according to the policy is computed through joint evaluation of these causal laws over the state with the known fluents about the agent’s location and the reachable points. Then, the outsourced planner may take as input the agent’s current location and the target location, to find a plan to reach the target.
Equalized transition system
The equalized transition system that describes the policy is defined as follows:

is the set of all interpretations of such that, for every static law (3) satisfies if satisfies ,

, where ,

is the set of all such that

for every there is a trajectory from some of the form in the original transition system;

for static laws for which satisfies the body, it holds that for some

Notice that in the definition of the transition relation in (iii) there is no description of (a) how a trajectory is computed or (b) how a target is determined. This gives flexibility on the implementation of these components.
Other languages can be similarly used to describe the equalized transition system, as long as they are powerful enough to express the concepts from the previous section.
Related Work
There are works being conducted on the verification of GOLOG programs [Levesque et al.1997], a family of highlevel action programming languages defined on top of action theories expressed in the situation calculus. The method of verifying properties of nonterminal processes are sound, but do not have the guarantee of termination due to the verification problem being undecidable [De Giacomo, Ternovskaia, and Reiter1997, Claßen and Lakemeyer2008]. By resorting to action formalisms based on description logic, decidability can be achieved [Baader and Zarrieß2013].
Verifying temporal properties of dynamic systems in the context of data management is studied by [Calvanese et al.2013] in the presence of description logic knowledge bases. However, target establishment and planning components are not considered in these works, and they do not address real life environment settings.
The logical framework for agent theory developed by Rao and Georgeff bdi91 is based on beliefs, desires and intentions, in which agents are viewed as being rational and acting in accordance with their beliefs and goals. There are many different agent programming languages and platforms based on the BDI approach. Some works carried out on verifying properties of agents represented in these languages, such as [Bordini et al.2006, Dennis et al.2012]. These approaches consider very complex architectures that even contain a plan library where plans are matched with the intentions or the agent’s state and manipulate the intentions.
Synthesizing and Verifying Plans
There have been various works on synthesizing plans via symbolic model checking techniques by Cimatti et al. cimattistrong98,cimattiobdd98, Bertoli et al. bertoli06. These approaches are able to solve difficult planning problems like strong planning and strong cyclic planning.
Son and Baral baral01 extend the action description language by allowing sensing actions and allow to query conditional plans. These conditional plans are general plans that consist of sensing actions and conditional statements.
These works address a different problem then ours. When nondeterminism and partial observability are taken into account, finding a plan that satisfies the desired results in the environment is highly demanding. We consider a much less ambitious approach where given a behavior, we aim to check whether or not this behavior gives the desired results in the environment. However, our framework is capable emulating the plans found by these works.
Execution Monitoring
There are logicbased monitoring frameworks that monitor the plan execution and recover the plans in case of failure. The approaches that are studied are replanning [De Giacomo, Reiter, and Soutchanski1998], backtracking to the point of failure and continuing from there [Soutchanski2003], or diagnosing the failure and recovering from the failure situation [Fichtner, Großmann, and Thielscher2003, Eiter et al.2007].
These works consider the execution of a given plan, while we consider a given reactive policy that determines targets and use (online) planning to reach these targets.
Conclusion and Future Work
In this paper, we described a highlevel representation that models reactive behaviors, and integrates target development and online planning capabilities. Flexibility in these components does not bound one to only use action languages, but allows for the use of other formalizations as well. For future work, one could imagine targets to depend on further parameters or to incorporate learning from experience in the framework. It is also possible to use other plans, e.g. short conditional plans, in the planner component.
The longterm goal of this work is to check and verify properties of the reactive policies for action languages. In order to solve these problems practically, it is necessary to use techniques from model checking, such as abstraction, compositional reasoning and parameterization. Also, the use of temporal logic formulas is needed to express complex goals such as properties of the policies. Our main target is to work with action languages, and to incorporate their syntax and semantics with such model checking techniques. The general structure of our framework allows one to focus on action languages, and to investigate how to merge these techniques.
References
 [Baader and Zarrieß2013] Baader, F., and Zarrieß, B. 2013. Verification of Golog programs over description logic actions. Frontiers of Combining Systems 181–196.
 [Bertoli et al.2006] Bertoli, P.; Cimatti, A.; Riveri, M.; and Traverso, P. 2006. Strong planning under partial observability. Artificial Intelligence 170(4):337–384.
 [Bordini et al.2006] Bordini, R. H.; Fisher, M.; Visser, W.; and Wooldridge, M. 2006. Verifying multiagent programs by model checking. Autonomous agents and multiagent systems 12(2):239–256.
 [Calvanese et al.2013] Calvanese, D.; De Giacomo, G.; Montali, M.; and Patrizi, F. 2013. Verification and synthesis in description logic based dynamic systems. In Web Reasoning and Rule Systems. Springer. 50–64.
 [Cimatti, Riveri, and Traverso1998a] Cimatti, A.; Riveri, M.; and Traverso, P. 1998a. Automatic OBDDbased generation of universal plans in nondeterministic domains. In Proc. of AAAI/IAAI, 875–881.
 [Cimatti, Riveri, and Traverso1998b] Cimatti, A.; Riveri, M.; and Traverso, P. 1998b. Strong planning in nondeterministic domains via model checking. AIPS 98:36–43.
 [Claßen and Lakemeyer2008] Claßen, J., and Lakemeyer, G. 2008. A logic for nonterminating Golog programs. In Proc. of KR, 589–599.
 [De Giacomo, Reiter, and Soutchanski1998] De Giacomo, G.; Reiter, R.; and Soutchanski, M. 1998. Execution monitoring of highlevel robot programs. In Proc. of KR, 453–465.
 [De Giacomo, Ternovskaia, and Reiter1997] De Giacomo, G.; Ternovskaia, E.; and Reiter, R. 1997. Nonterminating processes in the situation calculus. In Working Notes of “Robots, Softbots, Immobots: Theories of Action, Planning and Control”, AAAI’97 Workshop.
 [Dennis et al.2012] Dennis, L. A.; Fisher, M.; Webster, M. P.; and Bordini, R. H. 2012. Model checking agent programming languages. Automated Software Engineering 19(1):5–63.
 [Eiter et al.2004] Eiter, T.; Faber, W.; Leone, N.; Pfeifer, G.; and Polleres, A. 2004. A logic programming approach to knowledgestate planning: Semantics and complexity. ACM Trans. Comput. Log. 5(2):206–263.
 [Eiter et al.2005] Eiter, T.; Ianni, G.; Schindlauer, R.; and Tompits, H. 2005. A Uniform Integration of HigherOrder Reasoning and External Evaluations in AnswerSet Programming. In Proc. of IJCAI, 90–96.
 [Eiter et al.2007] Eiter, T.; Erdem, E.; Faber, W.; and Senko, J. 2007. A logicbased approach to finding explanations for discrepancies in optimistic plan execution. Fundamenta Informaticae 79(12):25–69.
 [Fichtner, Großmann, and Thielscher2003] Fichtner, M.; Großmann, A.; and Thielscher, M. 2003. Intelligent execution monitoring in dynamic environments. Fundamenta Informaticae 57(24):371–392.
 [Fink et al.2013] Fink, M.; Germano, S.; Ianni, G.; Redl, C.; and Schüller, P. 2013. Acthex: Implementing HEX programs with action atoms. Logic Programming and Nonmonotonic Reasoning 317–322.
 [Gebser, Grote, and Schaub2010] Gebser, M.; Grote, T.; and Schaub, T. 2010. Coala: A compiler from action languages to ASP. In Proc. of JELIA, 360–364. Springer Heidelberg.
 [Gelfond and Lifschitz1993] Gelfond, M., and Lifschitz, V. 1993. Representing action and change by logic programs. The Journal of Logic Programming 17(2):301–321.
 [Gelfond and Lifschitz1998] Gelfond, M., and Lifschitz, V. 1998. Action languages. Electronic Transactions on AI 3(16).
 [Giunchiglia and Lifschitz1998] Giunchiglia, E., and Lifschitz, V. 1998. An action language based on causal explanation: Preliminary report. In Proc. of AAAI/IAAI, 623–630.
 [Giunchiglia et al.2004] Giunchiglia, E.; Lee, J.; Lifschitz, V.; McCain, N.; and Turner, H. 2004. Nonmonotonic causal theories. Artificial Intelligence 153(1):49–104.
 [Kowalski and Sadri1999] Kowalski, R. A., and Sadri, F. 1999. From logic programming towards multiagent systems. Ann. Math. Artif. Intell. 25(34):391–419.
 [Levesque et al.1997] Levesque, H. J.; Reiter, R.; Lesperance, Y.; Lin, F.; and Scherl, R. B. 1997. GOLOG: A logic programming language for dynamic domains. The Journal of Logic Programming 31(1):59–83.
 [Lifschitz1999] Lifschitz, V. 1999. Action languages, answer sets and planning. In The Logic Programming Paradigm: a 25Year Perspective, 357–373. Springer.
 [Lifschitz2008] Lifschitz, V. 2008. What is answer set programming? In Proc. of. AAAI, 1594–1597.
 [Rao and Georgeff1991] Rao, A. S., and Georgeff, M. P. 1991. Modeling rational agents within a BDIarchitecture. In Proc. of KR, 473–484.
 [Son and Baral2001] Son, T. C., and Baral, C. 2001. Formalizing sensing actions – a transition function based approach. Artificial Intelligence 125(1):19–91.
 [Soutchanski2003] Soutchanski, M. 2003. Highlevel robot programming and program execution. In Proc. of ICAPS Workshop on Plan Execution.
 [Turner2002] Turner, H. 2002. Polynomiallength planning spans the polynomial hierarchy. In Proc. of JELIA, 111–124. Springer.
Comments
There are no comments yet.