Reasoning about Actions with Temporal Answer Sets ?

Abstract

In this paper we de ne a Temporal Action Theory through a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL). DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. In our language, general temporal constraints can be included in domain descriptions. We de ne the notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Bounded Model Checking techniques are used for the veri cation of DLTL formulas. The approach can deal with systems with in nite runs.

-

Introduction automaton from a DLTL formula has been proposed in [ 14 ], generalizing the tableau-based algorithm for LTL [ 12 ].

In this paper we de ne an extension of ASP rules by allowing temporal modalities and we introduce a notion of temporal answer set, which naturally allows to deal with possibly in nite action sequences. The temporal answer sets which satisfy the constraints in the domain description are recognized as the extensions of the domain description.

We provide a translation into standard ASP rules of action laws, causal laws, etc. in the domain description. The temporal answer sets of an action theory can then be computed as the standard answer sets of the translation. To compute the extensions of a domain description, the temporal constraints which are part of the domain description, are then evaluated over temporal answer sets using bounded model checking techniques [ 5 ]. The approach proposed for the veri cation of DLTL formulas extends the one developed in [ 18 ] for bounded LTL model checking with Stable Models.

The proposed action theory can deal naturally with systems with in nite runs, and we provide an example concerning a controlled system from the automotive domain. 2

Dynamic Linear Time Temporal Logic In this section we brie y de ne the syntax and semantics of DLTL as introduced in [ 19 ]. In such a linear time temporal logic the next state modality is indexed by actions. Moreover, (and this is the extension to LTL) the until operator U is indexed by a program as in Propositional Dynamic Logic (PDL). In addition to the usual 2 (always) and 3 (eventually) temporal modalities of LTL, new modalities [ ] and h i are allowed. Informally, a formula [ ] is true in a world w of a linear temporal model if holds in all the worlds of the model which are reachable from w through any execution of the program . A formula h i is true in a world w of a linear temporal model if there exists a world of the model reachable from w through an execution of the program , in which holds. The program can be any regular expression built from atomic actions using sequence (;), non-deterministic choice (+) and nite iteration ( ). The modalities 2, 3 and (next) of linear temporal logic can be seen to be derivable.

Let be a nite non-empty alphabet. The members of are actions. Let and ! be the set of nite and in nite words on , where ! = f0; 1; 2; : : :g. Let 1 = [ !. We denote by ; 0 the words over ! and by ; 0 the words over . Moreover, we denote by the usual pre x ordering over and, for u 2 1, we denote by prf(u) the set of nite pre xes of u.

We de ne the set of programs (regular expressions) P rg( ) generated by as follows:

P rg( ) ::= a j 1 + 2 j 1; 2 j where a 2 and 1; 2; range over P rg( ). A set of nite words is associated with each program by the mapping [[ ]] : P rg( ) ! 2 , which is de ned in the standard way.

Let P = fp1; p2; : : :g be a countable set of atomic propositions containing > and ?. The set of DLT L formulas over is de ned as follows:

DLTL( ) ::= p j : j _ j U where p 2 P, ; range over DLTL( ) and 2 P rg( ).

A model of DLTL( ) is a pair M = ( ; V ) where 2 ! and V : prf ( ) ! 2P is a valuation function. Given a model M = ( ; V ), a nite word 2 prf ( ) and a formula , the satis ability of a formula at in M , written M; j= , is de ned as follows: { M; j= p i p 2 V ( ); { M; j= : i M; 6j= ; { M; j= _ i M; j= or M; j= ; { M; j= U i there exists 0 2 [[ ]] such that 0 2 prf ( ) and M; . Moreover, for every 00 such that " 00 < 03, M; 00 j= . 0 j= A formula is satis able i there is a model M = ( ; V ) and a nite word 2 prf ( ) such that M; j= .

The formula U is true at if \ until " is true on a nite stretch of behavior which is in the linear time behavior of the program .

The derived modalities h i and [ ] can be de ned as follows: h i >U and [ ] :h i: .

Furthermore, if we let = fa1; : : : ; ang, the U (until), (next), 3 and 2 operators of LTL can be de ned as follows: Wa2 hai , U U , 3 >U , 2 :3: , where, in U , is taken to be a shorthand for the program a1 + : : : + an. Hence both LTL( ) and PDL are fragments of DLTL( ). As shown in [ 19 ], DLTL( ) is strictly more expressive than LTL( ). In fact, DLTL has the full expressive power of the monadic second order theory of !-sequences. 3

Action theories in Temporal ASP Let P be a set of atomic propositions, the uent names. A simple uent literal l is a uent name f or its negation :f . Given a uent literal l, such that l = f or l = :f , we de ne jlj = f . We denote by l the complementary literal of l (namely, p = :p and :p = p). Also, we denote by Lit the set of all simple uent literals. LitT is the set of (temporal) uent literals: if l 2 Lit, then l 2 LitT ; if l 2 Lit, then [a]l; l 2 LitT (for a 2 ). Given a (temporal) uent literal l, not l represents the default negation of l. A (temporal) uent literal possibly preceded by a default negation, will be called an extended uent literal.

A domain description D is de ned as a tuple ( ; F rame; C), where contains action laws, causal laws, precondition laws and the initial state, Init; Frame provides a classi cation of uents as frame uents and non-frame uents; C is a set of temporal constraints. 3 We de ne 0 i 9 00 such that 00 = 0. Moreover, where l1; : : : ; lm and l10; : : : ; lk0 are simple uent literals. Its meaning is that executing action a in a state in which the conditions l10; : : : ; lm0 hold causes either the e ect l1 or : : : or the e ect lk to hold.

In case of deterministic actions, there is a single disjunct in the head of the action law. For instance, from the Russian turkey problem domain, we have: 2([shoot]:alive loaded) (the action of shooting the turkey makes the turkey dead if the gun is loaded) and 2[load]loaded (loading the gun makes the gun loaded). An example of non-deterministic action is the action of spinning the gun, after which the gun may be loaded or not: 2([spin]loaded or [spin]:loaded true).

Causal laws are intended to express \causal" dependencies among uents. Static causal laws in have the form: where l; l1; : : : ; lm are simple uent literals. Their meaning is that: if l1; : : : ; lm hold in a state, l is also caused to hold in that state. For instance, the causal law 2(f rightened turkey in sight; alive) says that the turkey being in sight causes it to be frightened, if it is alive.

Dynamic causal laws in have the form: 2( l

l1; : : : ; lm; lm+1; : : : ; lk); meaning that: if l1; : : : ; lm hold in a state and lm+1; : : : ; lk hold in the next state, then l is caused to hold in the next state.

Precondition laws have the form:

l1; : : : ; lm); with a 2 and l1; : : : ; lk are simple uent literals. The meaning is that the execution of an action a is not possible if l1; : : : ; lk hold (that is, no state results from the execution of a in a state in which l1; : : : ; lk holds). An action for which there is no precondition law is always executable.

The initial state, Init, is a (possibly incomplete) set of simple uent literals, i.e., the uents which are known to hold initially.

For instance, Init = falive; :turkey in sight; :f rightenedg.

As in [ 22, 21 ] we call frame uents those uents to which the law of inertia applies. We consider frame uents as being dependent on the actions. Frame is a set of pairs (p; a), where p 2 P and a 2 , meaning that p is a frame uent for action a, that is, p is a uent to which persistency applies when action a is executed. Instead, non-frame uents with respect to a do non persist and may change value non-deterministically, when a is executed.

Unlike [ 13 ], we adopt a non-monotonic solution to the frame problem, as usual in the context of ASP. The persistency of frame uents from a state to the next one can be enforced by introducing persistency laws of the form:

l; not [a]l); for each simple uent literal l and action a 2 , such that (jlj; a) 2 F rame. Its meaning is that, if l holds in a state, then l holds in the state obtained by executing action a, if it can be assumed that :l does no hold in the resulting state.

For capturing the fact that a uent p which is non-frame with respect to a 2 may change its value non-deterministically when a is executed, we introduce the axiom: 2([a]p or [a]:p true) for all p and a such that (p; a) 62 F rame. When a is executed, either the nonframe uent literal p holds in the resulting state, or :p holds. We will call F rameD the set of laws introduced above for dealing with frame and non-frame uents. They have the same structure as action laws, but frame axioms contain default negation in their bodies. Indeed, both action and causal laws can be extended for free by allowing default negation in their body. This extension has been considered for instance in [ 8 ].

As concerns the initial state, we assume that its speci cation is, in general, incomplete. However, we reason on complete initial states obtained by completing the initial state in all the possible ways, and we assume that, for each uent p, the domain description contains the law: p or :p true meaning that either p is assumed to hold in the initial state, or :p is assumed to hold. This approach is in accordance with our treatment of non-deterministic actions and, as we will see, gives rise to extensions in which all states are complete, where each extension represents a run, i.e. a possible evolution of the world from the initial state. We will call InitD the set of laws introduced above for completing the initial state.

The temporal constraints in C are arbitrary temporal formulas of DLTL. They are used to restrict the space of the possible extensions. For instance, :loaded U turkey in sight states that the hunter does not load the gun until the turkey is in sight. A temporal constraint can also require a complex behavior to be performed.

The program = load; ((:turkey in sight)?; wait) ; (turkey in sight)?; spin; shoot describes the behavior of the hunter who loads the gun, waits for a turkey until it appears and, when there is one in sight, spins the gun and shoots. The action in sight? is a test action. DLTL does not include test actions. We de ne a test action p? as an atomic action with no e ect, which is executable only if p holds: 2([p?]? :p). 4

Example system

model As a further example, we describe an adaptation of the qualitative causal model of the \common rail" diesel injection system from [ 6, 24 ] where: { Pressurized fuel is stored in a container, the rail, in order to be injected at high pressure into the cylinders. We ignore in the model the output ow through the injectors. { Fuel from the tank is input to the rail through a pump. { A regulating system, including, in the physical system, a pressure sensor, a pressure regulator and an Electronic Control Unit, controls pressure in the rail; in particular, the pressure regulator, commanded by the ECU based on the measured pressure, outputs fuel back to the tank. { The control system repeatedly executes the sense pressure action while the physical system evolves through internal events4.

Examples of formulas from the model are as follows:

2([pump weak f ault]f in low)

shows the e ect of the fault event pump weak f ault.

Flows in uence the (derivative of) the pressure in the rail, and the derivative in uences pressure, e.g.: 2(p decr f out ok; f in low) 2(p incr f out very low; f in low) 2(p steady f out low; f in low) 2([p change]p low p ok; p decr) 2([p change]p ok p low; p incr) 2([p change]? p steady) 2([p change]? p decr; p low) 2([p change]? p incr; p normal)

2([sense pressure]p obs ok p ok)

2([sense pressure]p obs low p low)

2(f out ok normal mode; p obs ok)

2([switch mode]comp mode)

2(f out very low comp mode; p obs low)

2(f out low comp mode; p obs ok)

The model of the pressure regulating subsystem includes: 4 We make several further abstraction wrt [ 6, 24 ]. In particular, we consider \normal" and \low" abstractions for the pressure value, and we assume that the qualitative abstraction of the \normal" range of numeric values is large enough, the frequency (in the real system) of readings from the pressure sensor is high enough, and the reaction of the regulating system is fast and strong enough so that, when the system is driven away from the nominal behavior by a change which is small enough, it quickly evolves to a state which is steady in the qualitative abstraction. Alternatively, temporal constraints can be used to state, e.g., that a sense pressure action is executed at most every k internal events. This choice has, of course, a major in uence on properties that hold for the system model. Finding proper abstractions is a key problem in qualitative reasoning (see, e.g., [ 26 ]) and we do not aim at solving it here. Initially, everything is normal and pressure is steady:

p ok, p steady, f in ok, f out ok, normal mode We have the following constraints in C:

2(hp changeitrue (p ok ^ p decr) _ (p low ^ p incr)

2(hswitch modeitrue normal mode ^ p obs low)

[sense pressure]h( fsense pressureg) ihsense pressureitrue

2[pump weak f ault]:3hpump weak f aultiT rue

The rst models conditions under which a pressure change has to occur (su cient preconditions). The 2nd models the fact that a mode switch occurs when the system is operating in normal mode and the pressure measured is low. The 3rd one models the fact that the control system repeatedly executes sense pressure, but other actions may occur in between. The 4th imposes that at most one fault may occur in a run.

Given this speci cation, we can, for instance, check that if pressure is low in one state, it will be normal in the 3rd next one, namely, that the temporal formula 2(p low ! p ok) is satis ed in all the extensions.

Given the observation p obs low in a state, we can ask if there is an extension of the domain description which explains it. A diagnosis of the fault is a run from the initial state to a state in which p obs low holds and which does not contain previous fault observation in the previous states. In general, we can compute a diagnosis of the fault obsf by nding an extension of the domain description which satis es the formula: (:obs1 ^: : :^:obsn) U obsf , where obs1, : : : ; obsn are all the possible observations of fault. Here, p obs low is the only possible fault observation, hence a diagnosis for it is an extension of the domain description which satis es 3p obs low. 5

Temporal answer sets and extensions for domain descriptions Given a domain description D = ( ; F rame; C), the set of rules in [F rameD[ InitD is a general logic program extended with a restricted use of temporal modalities. The action modalities [a] and may occur in front of simple literals within rules and the 2 modality occurs in front of all rules in . In order to de ne the extensions of a domain description, we introduce a notion of temporal answer set, extending the notion of answer set [ 11 ]. The extensions of a domain description will be de ned as the temporal answer sets of [ F rameD [ InitD satisfying the integrity constraints C.

In the following, for conciseness, we will speak of simple literals and of temporal literal rather than of simple uent literals or temporal uent literal. Also, we will call rules the laws in [ F rameD [ InitD, which have the general form: 2(l10 or : : : or lh0

l1 ^ : : : ^ lm ^ not lm+1 ^ : : : ^ not lk); where the li0; lj 's are simple or temporal literals. Additional rules of the form [a1; : : : ; ah](l10 or : : : or lh0 l1 ^: : :^lm); where the li0; lj 's are simple or temporal literals, will be used in the following.

As we have seen, temporal models of DLTL are linear models, consisting in an action sequence and a valuation function V associating a propositional evaluation with each state in the sequence (denoted by a pre x of ) . To capture this linear structure of temporal models, the notion of answer set has to be extended accordingly. We de ne a partial temporal interpretation S as a set of literals of the form [a1; : : : ; ak]l where a; : : : ; ak 2 , meaning that literal l holds in S in the state obtained by executing the actions a1; : : : ; ak in the order. Let us de ne a notion of partial interpretation over .

De nition 1. Let 2 !. A partial temporal interpretation S over is a set of temporal literals of the form [a1; : : : ; ak]l, where a1 : : : ak is a pre x of , and it is not the case that both [a1; : : : ; ak]l and [a1; : : : ; ak]:l belong to S (namely, S is a consistent set of temporal literals).

We de ne a notion of satis ability of a literal l in a temporal interpretation S in the state a1 : : : ak as follows. A literal l is true in a partial temporal interpretation S in the state a1 : : : ak (and we write S; a1 : : : ak j=t l), if [a1; : : : ; ak]l 2 S; a literal l is false in a partial temporal interpretation S in the state a1 : : : ak (and we write S; a1 : : : ak j=f l), if [a1; : : : ; ak]l 2 S; and, nally, a literal l is unknown in a partial temporal interpretation S in the state a1 : : : ak (and we write S; a1 : : : ak j=u l), otherwise.

The notion of satis ability of a literal in a partial temporal interpretation in a given state, can be extended to temporal literals and to rules in a natural way. Given a partial temporal interpretation S over , and a pre x a1 : : : ak of we say that

S; a1 : : : ak j=t [a]l if [a1; : : : ; ak; a]l 2 S or a1 : : : ak; a is not a pre x of S; a1 : : : ak j=f [a]l if [a1; : : : ; ak; a]l 2 S or a1 : : : ak; a is not a pre x of S; a1 : : : ak j=u [a]l, otherwise.

For the temporal literals of the form l:

S; a1 : : : ak j=t l if [a1; : : : ; ak; b]l 2 S, where a1 : : : akb is a pre x of . S; a1 : : : ak j=f l if [a1; : : : ; ak; b]l 2 S, where a1 : : : akb is a pre x of .

S; a1 : : : ak j=u l, otherwise.

For default negation of a simple or temporal literal l:

S; a1 : : : ak j=t not l if S; a1 : : : ak j=f l or S; a1 : : : ak j=u l; S; a1 : : : ak j=f not l, otherwise.

The three valued evaluation of conjunctions and disjunctions of literals is de ned as usual in ASP (see, for instance, [ 11 ]). Finally, we say that a rule 2(H Body) is satis ed in a partial temporal interpretation S if, for all action sequences a1 : : : ak (including the empty one), S; a1 : : : ak j=t Body implies S; a1 : : : ak j=t H. We say that a rule [a1; : : : ; ah](H Body); is satis ed in a partial temporal interpretation S if S; a1 : : : ah j=t Body implies S; a1 : : : ah j=t H.

We are now ready to de ne the notion of answer set for a set P of rules that do not contain default negation. Let P be a set of rules over an action alphabet , not containing default negation, and let !. De nition 2. A partial temporal interpretation S over is a temporal answer set of P if S is minimal (in the sense of set inclusion) among the partial interpretations satisfying the rules in P .

We want to de ne answer sets of a program P possibly containing negation. Given a partial temporal interpretation S over 2 !, we de ne the reduct, P S , of P relative to S extending the transformation in [ 11 ] to compute a di erent reduct of P for each pre x a1; : : : ; ah of .

De nition 3. The reduct, PaS1;:::;ah , of P relative to S and to the pre x a1; : : : ; ah of , is the set of all the rules [a1; : : : ; ah](H l1 ^ : : : ^ lm); such that 2(H l1 ^ : : : ^ lm ^ not lm+1 ^ : : : ^ not lk) is in P and, for all i = m + 1; : : : ; k, either S; a1; : : : ; ah j=f li or S; a1; : : : ; ah j=u li, (where l; l1; : : : ; lk are simple or temporal literals). The reduct P S of P relative to S over is the union of all reducts PaS1;:::;ah for all pre xes a1; : : : ; ah of .

De nition 4. A partial temporal interpretation S over if S is an answer set of the reduct P S . is an answer set of P

The de nition above is a natural generalization of the usual notion of answer set to programs with temporal rules. Observe that the reduct P S is inherently in nite, as well as the answer sets. This is in accordance with the fact that temporal models are in nite. We can prove the following: Proposition 1. Given a domain description D over and an in nite sequence , any answer set of [ F rameD [ InitD over is a total answer set over .

In the following, we de ne the notion of extension of a domain description D = ( ; F rame; C) over in two steps: rst, we nd the answer sets of [ F rameD [ InitD; second, we lter out all the answer sets which do not satisfy the temporal constraints in C. For the second step, we need to de ne when a temporal formula is satis ed in a total temporal interpretation S. Observe that, a total answer set S over can be easily transformed into a temporal model as de ned in Section 2. Given a total answer set S over we de ne the corresponding temporal model as MS = ( ; VS ), where p 2 VS (a1; : : : ; ah) if and only if [a1; : : : ; ah]p 2 S, for all atomic propositions p. We say that a total answer set S over satis es a DLTL formula if MS ; " j= .

De nition 5. An extension of a domain description D = ( ; F rame; C) over , is any (total) answer set S of [ F rameD [ InitD satisfying the constraints in C.

Notice that, in general, a domain description may have more than one extension even for the same action sequence : the di erent extensions of D with the same account for the di erent possible initial states (when the initial state is incompletely speci ed) as well as for the di erent possible e ects of nondeterministic actions.

Translation to ASP We now show how to translate a domain description to standard ASP.

A model is a sequence of actions and a valuation function giving the value of uents in the states of the model. It can be represented in ASP by the predicates next(State; State0), occurs(Action; State) and holds(Literal; State). Predicate next must be de ned so that each state has exactly one successor state. An action law 2([a]l l1; : : : ; lm) can be easily translated as holds(l; S0) next(S; S0); occurs(a; S); holds(l1; S); : : : ; holds(lm; S) and similarly for the other kind of formulas of the action theory5. Occurrence of exactly one action in each state is also encoded. To deal with constraints, we use the predicate sat(F orm; S), to express satis ability of a formula DLTL in a state of a model, where F orm is an ASP atom representing formula , and S is a state. Let at[ ] be the ASP atom representing the formula. We exploit the equivalence between regular expressions and nite automata and we make use of an equivalent formulation of DLTL formulas in which until formulas are indexed with nite automata rather than regular expressions [ 14 ]. Thus we have U A(q) instead of U , where L(A(q)) = [[ ]]. More precisely, let A = (Q; ; QF ) be an -free nondeterministic nite automaton over the alphabet without an initial state, where Q is a nite set of states, : Q ! 2Q is the transition function, and QF is the set of nal states. Given a state q 2 Q, we denote with A(q) an automaton A with initial state q.

In the de nition of predicate sat for until formulas, we make use of the following axioms [ 19 ]:

U A(q) ( _ ( ^ Wa2 hai Wq02 (q;a) U A(q0) )) (q is a nal state of A)

U A(q) ^ Wa2 hai Wq02 (q;a) U A(q0) (q is not a nal state of A) The de nition of sat is:

uent: or: neg: until: sat(at[f ]; S)

holds(f; S): sat(at[ _ ]; S) sat(at[ _ ]; S) sat(at[: ]; S) sat(at[ ]; S): sat(at[ ]; S): not sat(at[ ]; S): sat(at[ U A(q) ]; S) sat(at[ ]; S); occurs(a; S); next(S; S0); sat(at[ U A(q0) ]; S0): 5 For instance, the causal law 2( l l1 ^ l2) is trasnslated to holds(l; S0) next(S; S0); holds(l1; S); holds(l2; S0); the precondition law 2([a]? l1; : : : ; lm); to occurs(a; S); holds(l1; S); : : : ; holds(lm; S).

(for each a 2 sat(at[ U A(q) ]; S) sat(at[ ]; S): (if q is a nal state of A)

and q0 2 (q; a))

Since states are complete, we can identify negation as failure with classical negation, thus having a two valued interpretation of DLTL formulas.

We must also add a constraint not sat(at[ ]; 0) for each temporal constraint in the domain description.

Given a DLTL formula , we can generate the corresponding ASP rules with the above transformation. It is easy to see that the number of the rules will be nite, since each rule will be applied to a subformula of , or to a formula derived from an until subformula. We say that a formula U A(q0) is derived from a formula U A(q) if q0 is reachable from q in A.

It can be proved that there is a one to one correspondence between the extensions of a temporal domain description and the answer sets of its translation in ASP.

Available ASP systems allow to deal only with nite sets of ground literals, and thus they do not allow to represent in nite sequences of states. To cope with this problem we exploit the property that any in nite LTL (and DLTL) model can be nitely represented by a nite sequence of states with a loop. Of course, the de nition of predicate next must be modi ed accordingly, to capture the fact that each state has a unique next state and the last state has one of its predecessors in the sequence as the next state6

We show that the above de nition of sat works also in this case by considering, in particular, the case of until formulas. If S is a state belonging to the loop the goal sat(at[ U A(q) ]; S) can depend cyclically on itself. This happens if the only rule which can be applied to prove the satis ability of U A(q) or one of its derived formulas in each state of the loop is the rst rule of until. In this case sat( U A(q) ; S) will be unde ned, which amounts to say that U A(q) is false. This is correct, since, if this happens, must be true in each state of the loop, and must be false in all states of the loop corresponding to nal states of A. Thus, by unfolding the cyclic sequence into an in nite sequence, U A(q) will never be satis ed.

Following the approach used in bounded model checking [ 5 ], satis ability of a domain description D can be proved by iteratively increasing the length k of 6 Special attention is also required in the computation of the uents which hold in the state si of the sequence which is the next state of the last state (the target of the loop back). Such a state is the next state of two di erent states (the last state and the state si 1). To deal with this case, we have added a new predicate holds next(L; S), which computes the literals L which are caused to hold in the state next to S, according to the application of the action, causal and persistency laws. The predicate hold next is used to freeze the e ects of action execution and is de ned as holds in the translation above. Then, holds is de ned from hold next, by the rules: holds(L; S) : holds next(L; S) and :holds(L; S) : :holds next(L; S). the sequence searched for, until a cyclic model is found (if one exists). On the other hand, validity of a formula can be proved, as usual in model checking, by verifying that D extended with : is not satis able. For instance, the translation of the domain description in section 4, for a given k > 5, has a nite number of answer sets, some in which no fault occurs, some in which the fault occurs in state 0; 1; : : : ; k 6. Such extensions correspond to temporal answer sets of the given domain description and the formula 2(p low ! p ok) holds in these extensions. The techniques in [ 5 ] (in particular, section 5.1) can be used, in general, to achieve completeness in proving validity.

In many cases (e.g. planning) we want to reason only on nite pre xes of in nite models. This can be achieved by just adding to the domain description one action dummy, and the constraints 3hdummyitrue and 2(hdummyitrue ! hdummyihdummyitrue) stating that, from some point on, only dummy will be executed. If the ASP computation return a model, it consists of a nite sequence satisfying the domain description ending with a loop of dummy actions. 7

Conclusions and related work In this paper we developed an extension of ASP for dealing with temporal action theories with general DLTL constraints, which include regular programs indexing temporal modalities. The approach naturally deals with non-terminating computations and relies on bounded model checking techniques for the veri cation of temporal DLTL formulas.

In the last decade, ASP has been shown to be well suited for reasoning about dynamic domains [ 11 ]. In [ 3 ] Baral and Gelfond provide an encoding in ASP of the action speci cation language AL, which extends the action description language A [ 10 ] by allowing static and dynamic causal laws, executability conditions and concurrent actions. The proposed approach has been used for planning [ 23 ] and diagnosis (see[ 1 ]). In [ 8, 9 ] a logic-based planning language, K, is presented which is well suited for reasoning about incomplete knowledge and is implemented on the top of the DLV system. In [ 16, 15 ] the languages C and C+ provide an account of causality and deal with actions with indirect and non-deterministic e ects and with concurrent actions. While our action language does not deal with concurrent actions and incomplete knowledge, our proposal extends the ASP approach for reasoning about dynamic domains with in nite computations.

Bounded model checking [ 5 ] is based on the idea to search for a counterexample of the property to be checked in executions which are bounded by some integer k. The value of k is increased until a counterexample is found, the problem becomes intractable or a known upper bound is reached. SAT based bounded model checking methods do not su er from the state explosion problem as the methods based on BDDs. Helianko and Niemela [ 18 ] have developed a compact encoding of bounded model checking of LTL formulas as the problem of nding stable models of logic programs. In this paper, we have de ned a similar approach for encoding bounded model checking of DLTL formulas in ASP. While the construction of a Buchi automaton [ 19, 14 ] from a DLTL formula requires a speci c machinery to deal with program expressions with respect to the usual construction for LTL, bounded LTL model checking can be naturally extended to deal with program expressions in temporal modalities, by a direct encoding in ASP of the recursive de nition of the modalities.

The presence of temporal constraints in our action language has some relation with the work on temporally extended goals in [ 7, 4 ]. These papers, however, are concerned with the problem of expressing preferences among goals and exceptions in goal speci cation.

The action language presented in this work is an ASP formulation of the action theory de ned in [ 13 ] which, instead, was based on a monotonic solution to the frame problem. Due to the di erent treatment of the frame problem, the notion of extension de ned here is not equivalent to the one in [ 13 ]. In particular, the formalization of causal rules in [ 13 ] does not allow reasoning by cases. Moreover, the completion solution requires action and causal laws to be strati ed to avoid unexpected extensions when action and causal laws contain cyclic dependencies.

References

1. M. Balduccini and M. Gelfond: Diagnostic Reasoning with A-Prolog , Theory and Practice of Logic Programming , 3 ( 4 -5): 425 { 461 , 2003 .

2. F. Bacchus and F. Kabanza . Planning for temporally extended goals . In Annals of Mathematics and AI , 22 :5{ 27 , 1998 .

3. C. Baral and M. Gelfond . Reasoning agents in dynamic domains . In Logic-Based Arti cial Intelligence , 257 { 279 , 2000 .

4. C. Baral , J . Zhao: Non-monotonic Temporal Logics for Goal Speci cation . IJCAI 2007 : 236 { 242 .

5. A. Biere , A. Cimatti , E. M. Clarke , O. Strichman , Y. Zhu , Bounded model checking . Advances in Computers 58 : 118 { 149 , 2003 .

6. F. Cascio , L. Console , M. Guagliumi , M. Osella , A. Panati , S. Sottano , and D. Theseider Dupre . Generating on-board diagnostics of dynamic automotive systems based on qualitative deviations . AI Communications , 12 ( 1 ): 33 { 44 , 1999 .

7. Dal Lago , U. ; Pistore , M. ; and Traverso, P. 2002 . Planning with a Language for Extended Goals . In Proc. AAAI02 .

8. T. Eiter , W. Faber , N. Leone , G. Pfeifer , A. Polleres , Planning under Incomplete Knowledge . Computational Logic 2000 , 807 { 821 .

9. T. Eiter , W. Faber , N. Leone , G. Pfeifer , A. Polleres , A logic programming approach to knowledge-state planning: Semantics and complexity . ACM Trans. Comput. Log . 5 ( 2 ): 206 { 263 , 2004 .

10. M. Gelfond and V. Lifschitz . Representing action and change by logic programs . Journal of logic Programming , 17 : 301 { 322 , 1993 .

11. M. Gelfond . Handbook of Knowledge Representation, chapter 7 . Answer Sets . Elsevier, 2007 .

12. R. Gerth , D. Peled , M.Y. Vardi and P. Wolper. Simple On-the- y Automatic veri - cation of Linear Temporal Logic . In Proc. 15th Work . Protocol Speci cation, Testing and Veri cation , Warsaw, June 1995, North Holland.

13. L. Giordano , A. Martelli , and C. Schwind . Reasoning About Actions in Dynamic Linear Time Temporal Logic . In The Logic Journal of the IGPL , 9 ( 2 ): 289 { 303 , 2001 .

14. L. Giordano and A. Martelli . Tableau-based Automata Construction for Dynamic Linear Time Temporal Logic . Annals of Mathematics and Arti cial Intelligence , 46 ( 3 ): 289 { 315 , Springer 2006.

15. E. Giunchiglia, J. Lee , V. Lifschitz , N. McCain , and H. Turner . Nonmonotonic causal theories . Artif . Intell., 153 ( 1-2 ): 49 { 104 , 2004 .

16. E. Giunchiglia and V. Lifschitz . An action language based on causal explanation: Preliminary report . In AAAI/IAAI , pages 623 { 630 , 1998 .

17. F. Giunchiglia and P. Traverso . Planning as Model Checking . In Proc. The 5th European Conf. on Planning (ECP'99) , 1 { 20 , Durham (UK), 1999 .

18. K. Heljanko , I. Niemela, Bounded LTL model checking with stable models . TPLP 3 ( 4 -5): 519 { 550 ( 2003 )

19. J.G. Henriksen and P.S. Thiagarajan . Dynamic Linear Time Temporal Logic . in Annals of Pure and Applied logic , vol. 96 , n. 1-3 , 187 { 207 , 1999 .

20. F. Kabanza , M. Barbeau and R. St-Denis Planning control rules for reactive agents . In Arti cial Intelligence , 95 ( 1997 ) 67 { 113 .

21. G.N. Kartha and V. Lifschitz . Actions with Indirect E ects (Preliminary Report) . In Proc. KR ' 94 , 341 { 350 , 1994 .

22. V. Lifschitz . Frames in the Space of Situations . In Arti cial Intelligence , Vol. 46 , 365 { 376 , 1990 .

23. R. Morales , M. Gelfond , Tran Cao Son, and Phan Huy Tu. Approximation of Action Theories and Its Application to Conformant Planning . Arti cial Intelligence , 2008 .

24. A. Panati and D. Theseider Dupre . Causal simulation and diagnosis of dynamic systems . In AI*IA 2001: Advances in Arti cial Intelligence , Springer Verlag LNCS 2175.

25. R. Reiter . The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression . In Arti cial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy , V. Lifschitz, ed., 359 { 380 , Academic Press, 1991 .

26. M. Sachenbacher and P. Struss . Task-dependent qualitative domain abstraction . Arti cial Intelligence , 162 ( 1-2 ), 121 { 143 , 2005 .