Verification of action theories in ASP: a complete Bounded Model Checking approach Laura Giordano1, Alberto Martelli2 , and Daniele Theseider Dupré1 1 DISIT, Università del Piemonte Orientale {laura.giordano,dtd}@mfn.unipmn.it 2 Dipartimento di Informatica, Università di Torino mrt@di.unito.it Abstract. Temporal logics are well suited for reasoning about actions, as they allow for the specification of domain descriptions including temporal constraints as well as for the verification of temporal properties of the domain. This paper fo- cuses on the verification of action theories formulated in a temporal extension of answer set programming which combines ASP with a dynamic linear time tem- poral logic. The paper proposes an approach to bounded model checking (BMC) which exploits the Büchi automaton construction while searching for a counterex- ample, with the aim of achieving completeness. The paper provides an encoding in ASP of the temporal action domains and of BMC of DLTL formulas. 1 Introduction Temporal logics have been extensively used in the specification and verification of ac- tion domains in many fields, from planning to web services. In planning, both CTL [22, 25] and LTL [4, 3] have been used in the specification of temporally extended goals. The need for state trajectory constraints has been advocated in PDDL3 [15]. [2] ex- ploits a first order linear temporal logic for defining domain dependent search control knowledge in the planner TLPlan, and in [11] strong fairness constraints expressed in LTL are used to restrict nondeterminism in generalized planning. LTL has been used in the verification of agent interaction protocols [18] and for enforcing regulations in automated Web service composition [26]. In the context of reasoning about action, [9] has introduced a second order extension of the temporal logic CTL*, ESG, to reason about non-terminating Golog programs. In this paper, we start from the temporal action theories introduced in [19], formu- lated in a temporal extension of answer set programming (ASP [14]), and we exploit Bounded Model Checking (BMC) techniques for the verification of properties of such action theories. BMC [5] is an efficient model checking techniques which does not re- quire a tableau or automaton construction. Given a system model (a transition system) and a property to be checked, it searches for a counterexample of the property as a path of length k, generating a propositional formula that is satisfiable iff such a counterex- ample exists. The bound k on the length of the path is iteratively increased and, if no counterexample exists, the procedure never stops. As a consequence, bounded model checking provides only a partial decision procedure for checking validity. Techniques for achieving completeness have been described in [5], where upper bounds for k are determined for some classes of properties, namely unnested properties. To deal with completeness, [8] proposes a semantic translation scheme, based on Büchi automata. In [23] Helianko and Niemelä developed a compact encoding of bounded model checking of LTL formulas as the problem of finding stable models of logic programs. Since ASP naturally accommodates for reasoning about actions, in [19] this encoding is extended to deal with Dynamic Linear Time Temporal Logic (DLTL) formulas, for reasoning about action theories including complex actions and programs. These papers do not address the problem of achieving completeness. In this paper we propose an alternative encoding of BMC of DLTL formulas in ASP, with the aim of achieving completeness. Unlike [23, 19], here the search for a counterexample exploits the Büchi automaton construction [16] as well as the transition system. Unlike [8], a “counterexample” path is searched for, without assuming that the Büchi automaton is constructed in advance. Our counterexample is an accepting path of the product Büchi automaton which can be finitely represented as a (k,l)-loop , i.e., a finite path of length k terminating in a loop back to a previous state l, in which the states are all distinct from each other. The procedure for verifying a given property searches for a (k,l)-loop, providing a counterexample to the property, increasing k until either a counterexample is found, or no (k,l)-loop of length greater or equal to k can be found. As in [19], verification is performed on a transition system provided by a domain description in a temporal action theory, and our BMC approach is used for proving properties of domain descriptions. The action theory is given in a temporal extension of ASP, based on the generalization of the notion of answer set [14] to temporal answer sets. The temporal properties of a domain description can be proved by combining the construction of temporal extensions of the domain with the verification of their properties, according to a tableaux-based procedure which provides an encoding of BMC in ASP. The proposed approach provides a decision procedure for the verification of satisfiability and validity properties of an action domain in a temporal action theory. The outline of the paper is the following. First, we introduce the temporal action language and its answer sets, and we introduce verification problems for action theories. We then describe our approach to action theory verification by BMC. Finally we provide an ASP encoding of BMC and discuss related work. 2 Temporal Action Theories In this paper we refer to a formulation of DLTL (dynamic linear time temporal logic), in [24], where the next state modality is indexed by actions and the until operator U π is indexed by a program π which, as in PDL, can be any regular expression built from atomic actions using sequence (;), nondeterministic choice (+) and finite iteration (∗). Let Σ = {a1 , . . . , an } be a finite non-empty alphabet of actions. From the until op- erator, the derived modalities hπi, [a], (next), W U, 3 and 2 can be defined as follows: ∗ hπiα ≡ ⊤U π α, [a]α ≡ ¬hai¬α, α ≡ a∈Σ haiα, αUβ ≡ αU Σ β, 3α ≡ ⊤Uα, ∗ 2α ≡ ¬3¬α, where α is a formula and, in U Σ , Σ is taken to be a shorthand for the program a1 + . . . + an 2.1 Temporal Action Language Let L be a first order language which includes a finite number of constants and vari- ables, but no function symbol. Let P be the set of predicate symbols, V ar the set of variables and C the set of constant symbols. We call fluents atomic literals of the form p(t1 , . . . , tn ), where, for each i, ti ∈ V ar ∪ C. A simple fluent literal (or s-literal) l is an atomic literals p(t1 , . . . , tn ) or its negation ¬p(t1 , . . . , tn ). We denote by LitS the set of all simple fluent literals. LitT is the set of temporal fluent literals: if l ∈ LitS , then [a]l, l ∈ LitT , where a is an action name (an atomic proposition, possibly con- taining variables), and [a] and are the temporal operators introduced in the previous section. Let Lit = LitS ∪ LitT ∪ {⊥}, where ⊥ represents the inconsistency. Given a (simple or temporal) fluent literal l, not l represents the default negation of l. A (sim- ple or temporal) fluent literal possibly preceded by a default negation, will be called an extended fluent literal. A domain description Π is a set of laws describing the effects of actions and their executability preconditions. The laws are formulated as rules of a temporally extended logic programming language. Rules have the form l0 ← l1 , . . . , lm , not lm+1 , . . . , not ln (1) where the li ’s are either simple fluent literals or temporal fluent literals, with the fol- lowing constraints: (i) If l0 is a simple literal, then the body cannot contain temporal literals; (ii) If l0 = [a]l, then the temporal literals in the body must have the form [a]l′ ; (iii) If l0 = l, then the temporal literals in the body must have the form l′ . As usual in ASP, the rules with variables will be used as a shorthand for the set of their ground instances. A state, informally, is a set of ground fluent literals closed with respect to the rules above (see Section 2.2). A state is said to be consistent if it is not the case that both f and ¬f belong to the state, or that ⊥ belongs to the state. A state is said to be complete if, for each fluent name p ∈ P, either p or ¬p belong to the state. The execution of an action in a state may possibly change the values of fluents in the state through its direct and indirect effects, thus giving rise to a new state. We assume that a law as (1) can be applied in all states, while when prefixed with the Init, only applies to the initial state. Example 1. This example describes a mail delivery agent, which checks if there is mail in the mailbox of employees and delivers mail to them. The actions in Σ are: sense (the agent verifies if there is mail in any of the mailboxes), deliver(E) (the agent delivers the mail to employee E), wait. The fluent names are mail(E) (there is mail in the mailbox of E). Π contains the following immediate effects and persistency laws: [deliver(E)]¬mail(E) [sense]mail(E) ← not [sense]¬mail(E) mail(E) ← mail(E), not ¬mail(E) ¬mail(E) ← ¬mail(E), not mail(E) Their meaning is (in the order) that: after delivering the mail to E, there is no mail for E any more; the action sense may (non-monotonically) cause mail(E) to become true. The last two rules define the persistency of fluent mail. Observe that the persistency laws interact with the immediate effect laws above. The execution of sense in a state in which there is no mail for some E (¬mail(E)), may either lead to a state in which mail(E) holds (by the second action law) or to a state in which ¬mail(E) holds (by persistency of ¬mail(E)). Thus, sense is a nonde- terministic action. The following precondition laws: [deliver(E)] ⊥← ¬mail(E) [wait] ⊥← mail(E) specify that, if there is no mail for E, deliver(E) is not executable, while, if there is mail for E, wait is not executable. We assume that there are only two employees, a and b and, in the initial state, there is mail for a and not for b, i.e. Π includes Init mail(a) and Init ¬mail(b). The language is also well suited to describe causal dependencies among fluents [19] by the definition of static and dynamic causal laws similar to the ones in the action languages K [12] and C + [20]. 2.2 Temporal Answer Sets In this section, we recall the notion of temporal answer set in [19], which extends the notion of answer set [14], and we state a new result on the transition system associated with a domain description. To this purpose, we let Π be the ground instantiation of the domain description, and Σ the set of all the ground instances of the action names in Π. A temporal interpretation is defined as a pair (σ, S), where σ ∈ Σ ω is a sequence of actions and S is a consistent set of ground literals of the form [a1 ; . . . ; ak ]l, where a1 . . . ak is a prefix of σ and l is a ground simple fluent literal, meaning that l holds in the state obtained by executing a1 . . . ak . S is consistent iff it is not the case that both [a1 ; . . . ; ak ]l ∈ S and [a1 ; . . . ; ak ]¬l ∈ S, for some l, or [a1 ; . . . ; ak ]⊥ ∈ S. A temporal interpretation (σ, S) is said to be total if either [a1 ; . . . ; ak ]p ∈ S or [a1 ; . . . ; ak ]¬p ∈ S, for each a1 . . . ak prefix of σ and for each fluent name p. The notion of satisfiability of a rule in a temporal interpretation (σ, S), as well as the notion of reduct Π (σ,S) of (a domain description) Π relative to (σ, S) can be defined as natural extensions of Gelfond and Lifschitz’ ones [14]. With these notions, a temporal answer set of Π is defined as a temporal interpretation (σ, S) such that S is minimal (in the sense of set inclusion) among the S ′ such that (σ, S ′ ) is a partial interpretation satisfying the rules in the reduct Π (σ,S) . The case of total temporal answer sets is of special interest, as a total temporal answer set (σ, S) can be regarded as temporal model (σ, VS ), where, for each finite prefix a1 . . . ak of σ, VS (a1 , . . . , ak ) = {p : [a1 , . . . , ak ]p ∈ S}. In the following, we restrict our consideration to domain descriptions Π, such that all the answer sets of Π are total. If the initial state is not complete, we consider all the possible ways to complete the initial state by introducing in Π, for each fluent name f , the rules: Init f ← not ¬f and Init ¬f ← not f . A total temporal interpretation (σ, S) provides, for each prefix a1 . . . ak , a complete (σ,S) state corresponding to that prefix. We denote by wa1 ...ak the state obtained by the execu- (σ,S) tion of the actions a1 . . . ak in the sequence, namely wa1 ...ak = {l : [a1 ; . . . ; ak ]l ∈ S}. Given a domain description Π over Σ with total answer sets, a transition system (W, I, T ) can be associated with Π as follows: (i) W is the set of all the possible consistent and complete states of the domain description; (ii) I is the set of all the states in W satisfying the initial state laws in Π; (iii) T ⊆ W × Σ × W is the set of all triples (w, a, w′ ) such that: w, w′ ∈ W , a ∈ Σ and for some total answer set (σ, S) of Π: (σ,S) (σ,S) w = w[a1 ;...;ah ] and w′ = w[a1 ;...;ah ;a] , for some h. It is possible to show that the next states of a given state w in the transition system (W, I, T ) above only depend on the state w. Let Πw be the domain description obtained form Π by removing all the laws prefixed by Init while adding to Π Init l, for all l ∈ w. Proposition 1. Let w be a state in W which is reachable form an initial state by the action sequence a1 . . . ah . If (w, a, w′ ) ∈ T , then there is an answer set (σ ′ , S ′ ) of Πw , such that (1) σ = a1 . . . ah σ ′ and (2) [a]l ∈ S ′ iff l ∈ w′ . Vice versa, if there is an answer set (σ ′ , S ′ ) of Πw satisfying conditions (1) and (2) above, then (w, a, w′ ) ∈ T . Proposition 1 guarantees that, given a state w and an action a, a next state function nextT Sstate can be defined to compute all the states reachable in the transition system from w by a. Such a function is used in the following to describe the BMC construction. 2.3 Verification of Enriched Domain Descriptions As a total temporal answer set of a domain description can be interpreted as an DLTL model, it is easy to combine domain descriptions with DLTL formulas. This can be done by adding to the domain description Π a set of DLTL formulas C used as constraints on the executions of the domain description. We denote by (Π, C) the enriched domain description, and we define the extensions of (Π, C) to be the temporal answer sets (σ, S) of Π satisfying the constraints C. For example, hbegini⊤ 2[begin]hsense; (deliv(a) + deliv(b) + wait); begini⊤ impose that the agent continuously executes a loop where it senses mail and delivers the mail. DLTL formulas can be used to encode properties to be verified on the enriched domain description. We may want to check that, if there is mail for a, the agent will eventually deliver it, i.e.: 2(mail(a) ⊃ 3¬mail(a)). This does not hold, as there is a possible scenario in which there is always mail for a and for b, but the mail is repeatedly delivered to b and never to a. Given an enriched domain description (Π, C), some problems, e.g. planning, can be formulated as satisfiability of a formula ϕ, and others, such as the one in the example above, as validity of a formula ϕ. Usually, the validity of a property ϕ formulated as a DLTL formula is reduced to the unsatisfiability of ¬ϕ. In this case, if a model satisfying ¬ϕ is found, it represents a counterexample to the validity of ϕ. 3 Model Checking Satisfiability and validity problems can be solved by means of model checking tech- niques. The standard approach to model checking for LTL is based on Büchi automata. The satisfiability problem for a LTL formula α can be solved by constructing a Büchi automaton Bα [16] such that the language of ω-words accepted by Bα is non-empty if and only if α is satisfiable. Given a system modeled by a transition system T S, which corresponds to a Büchi automaton BT S , model checking verifies that the property α holds for the system, by constructing the product automaton of BT S and B¬α , and by checking for emptiness of the accepted language. Biere et al. [5] showed that model checking can be more efficient if, instead of building the product automaton, a path of the transition system satisfying ¬α is searched for. This technique is called bounded model checking (BMC), since it looks for infinite paths which can be represented as a finite path of length k with a back loop from state k to a previous state l in the path (a (k,l)-loop); the search proceeds iteratively, increasing the length k until a model satisfying α is found — if one exists. A BMC problem can be efficiently reduced to a propositional satisfiability problem or to an ASP problem [23]. If no model exists and the transition system contains a loop, the iterative procedure in general does not stop, i.e., it is a partial decision procedure for validity. Techniques for achieving completeness are described in [5] for some kinds of LTL formulas. 4 Bounded Model Checking with Büchi Automata In this paper, we propose an approach to model checking which combines the advan- tages of BMC, in particular the possibility of formulating it easily and efficiently as an ASP problem, with the advantages of reasoning on the product Büchi automaton described above, mainly its completeness. In the following we show how to adapt the procedure for building a Büchi automa- ton corresponding to a given DLTL formula [17] to the “on-the-fly” construction of the product Büchi automaton, and we show how this construction can be used to build a (k,l)-loop corresponding to a run of the product Büchi automaton. In the following construction we assume that, as in [17], until formulas are indexed with finite automata rather than regular expressions. Thus, we have αU A(q) β instead of αU π β, where L(A(q)) = [[π]]. We denote with A(q) a finite automaton A with initial state q. The following equivalences hold for the until operator [24]: W W ′ αU A(q) β ≡ (β ∨ (α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β)) (q is a final state of A) W W ′ αU A(q) β ≡ (α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β) (q is not a final state of A) The construction of the nodes makes use of tableau rules which handle DLTL signed formulas, i.e. formulas prefixed with the symbol T or F. These rules are applied to a set of formulas1 as follows: – φ ⇒ ψ1 , ψ2 , if φ belongs to the set of formulas, then add ψ1 and ψ2 to the set – φ ⇒ ψ1 |ψ2 , if φ belongs to the set of formulas, then make two copies of the set and add ψ1 to one of them and ψ2 to the other one. The rules are the following: Tor: T(α ∨ β) ⇒ Tα|Tβ For: F(α ∨ β) ⇒ Fα, Fβ Tneg: T¬α ⇒ Fα Fneg: F¬α ⇒ Tα W W ′ TuntilFS: TαU A(q) β ⇒ T(β ∨ (α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β)) (q final state) 1 In this section “formula” means “signed DLTL formula”. W W ′ TuntilNFS: TαU A(q) β ⇒ T(α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β)(q not final state) W W ′ FuntilFS: FαU A(q) β ⇒ F(β ∨ (α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β)) (q final state) W W ′ FuntilNFS: FαU A(q) β ⇒ F(α ∧ a∈Σ hai q′ ∈δ(q,a) αU A(q ) β) (q not final state) WWe use a function tableau which takes as input a set of formulas s, adds to it T a∈Σ hai⊤, and returns a (possibly empty) set of sets of formulas, obtained by repeat- edly applying the above rules (by possibly creating new sets) until all non-elementary formulas in all sets have been expanded. We call elementary formulas the formulas ofWthe form Tφ or Fφ where φ is either ⊤, or ⊥, or a proposition or haiα. Formula T a∈Σ hai⊤ makes explicit that in DLTL each state must be followed by a next state. If the expansion of a set of formulas produces an inconsistent set, then this set is deleted. A set of formulas s is inconsistent in the following cases: (i) T⊥ ∈ s; (ii) F⊤ ∈ s; (iii) Tα ∈ s and Fα ∈ s; (iv) Thaiα ∈ s and Thbiβ ∈ s with a 6= b, because in a linear time logic two different actions cannot be executed in the same state. We describe now how to build a path of the product automaton, which is constructed by the BMC procedure while searching for a counterexample. Each state s of the path is a tuple s = (F , w, x, f ), where F is an expanded set of formulas, w is a state of the transition system whose literals are represented as signed formulas, x ∈ {0, 1} and f ∈ {↓, X} are used to track fulfillment of until formulas, as we will describe below. Given a domain description Π with the associated transition system T S, and a DLTL formula α describing constraints and properties to be proved, the initial states will have the form (F0 , w0 , 0, X), where F0 is a set of formulas obtained by applying function tableau to α, and w0 is an initial state of T S, such that F0 ∪ w0 is consistent. Transitions of the product automaton are defined by function next states(s, a), defined in Figure 2, which returns the set of successor states of s after a. This function makes use of the functions nextT Sstates(w, a), which returns the set of the states of the transition system T S reached with a transition a from state w, and nextF (F , a), which returns a set of formulas obtained by propagating the formulas in F through action a. Function nextF is defined in Figure 1. This function first checks whether it is possible to execute action a from F , then propagates elementary temporal formulas through a and expands them with tableau. function nextF(F, a) if F does not contain a formula Thaiα then return ∅ else return tableau({Tα|Thaiα ∈ F} ∪{Fα|Fhaiα ∈ F}) Fig. 1. Function nextF The fields x and f are used to characterize accepting states of the product automa- ton, and are used to check that all until formulas are fulfilled in a finite number of steps. If a state si of an accepting run ρ contains the until formula TαU A(q) β, then there must be a state sj , i ≤ j in ρ satisfying the conditions given by the semantics of un- til. We say that sj fulfills the until formula. If si does not fulfill the until formula, then it is possible to show that, according to the axioms of until, si contains a formula function next states((F, w, x, f ), a) return {(F ′ , w′ , x′ , f ′ ) such that F ′ ∈ nextF(F, a), w′ ∈ nextT Sstates(w, a), F ′ ∪ w′ is consistent, A(q) if there exist no ThaiαUx β ∈ F ′ ′ then x = 1 − x; f = X else x′ = x; f ′ =↓ } Fig. 2. Function next states ′ Thai iαU A(q ) β, where q ′ ∈ δ(q, ai )2 and, according to function nextF (Fi , ai ), si+1 ′ contains a formula TαU A(q ) β. We say that this until formula is derived from formula TαU A(q) β in state si . If a state contains an until formula which is not derived from a predecessor state, we say that the formula is new. New until formulas are obtained during the expansion of tableau. In order to check fulfillment of until formulas, we must be able to track them along the states of the run. This is done by using the field x and by extending accordingly signed formulas so that all true until formulas have a label 0 or 1, i.e. they have the A(q) form TαUl β where l ∈ {0, 1}. For each state (F , w, x, f ), the label of an until formula in F is assigned as follows: if it is a derived until formula, then its label is the same as that of the until formula in the predecessor state it derives from, otherwise, if the formula is new, it is given the label 1 − x. Function tableau must be suitably modified in order to deal with the labels of until formulas. We assume that it has two parameters: a set of formulas and the value of x. Let us assume that in a state si we have x = 0. Then all new until formulas of si have label 1, and all until formulas with label 0 must be derived from previous states. If si belongs to an accepting run, all until formulas will be fulfilled in a finite number of steps. The value 0 of x is propagated to the next states until a state sj does not contain any more until formulas with label 0. Then x is switched to 1, and we proceed in the same way. Whenever x changes its value, we set f = X. A state with f = X is an accepting state of the product automaton, and a run ρ containing infinite accepting states is an accepting run. It is an obvious consequence of the construction that: Proposition 2. (i) Any accepting run of the product automaton corresponds an infinite path of the transition system (i.e., a temporal answer set of Π) satisfying the initial DLTL formula α; (ii) every infinite path of the transition system which is a model of α corresponds to an accepting run of the product automaton. The proof, omitted for lack of space, exploits Theorems 4 and 5 in [17]. Our approach to BMC relies on the well known result [7] that the language accepted by a Büchi automaton is nonempty iff there is a reachable accepting state with a cycle back to itself. The construction of the (k,l)-loop is described by the function BM C in Figure 3. The construct choose in S returns any of the elements of set S or null if 2 δ is the transition relation of A. function BM C(max k) k := 0 do a0 a path := choose in {s0 → s1 →1 . . . sk+1 such that sj 6= sm for 0 ≤ j < m ≤ k, sl = sk+1 for some l ≤ k, sacc is an accepting state for some l ≤ acc ≤ k} k := k + 1 while path = null ∧ k ≤ max k return path Fig. 3. Function BM C function max() i := 0 do i := i + 1 a0 a path := choose in {s0 → s1 →1 . . . si such that sj 6= sm for 0 ≤ j < m ≤ i} while path 6= null return i − 1 Fig. 4. Function max a a S = ∅. With s0 →0 s1 →1 . . . si we represent a finite path of the product automaton, where s0 is an initial state and si ∈ next states(si−1 , ai−1 ). Given an integer k, we look for a path of length k + 1, such that sk+1 = sl for some previous state sl in the path. Furthermore the loop must contain an accepting state. If such a loop is found, it finitely represents an accepting run. Otherwise, k is increased until max k is reached. Observe that the standard approach for bounded model checking in [5] does not guarantee termination, because the path of length k is a path of the transition system, and thus it is not possible to restrict the search to simple paths without missing so- lutions. On the other hand, we can consider only simple paths, that is paths without repeated states. This property allows to define a terminating algorithm, thus achieving completeness, by passing the length of the longest simple path as parameter to BM C. The length of the longest simple path can be found iteratively, searching for a simple path of length i (without loop), and incrementing i at each step (See Figure 4). Since the number of different states if finite, this procedure terminates. The set of tableau rules can be easily extended to deal with other boolean connec- tives and derived modal operators. In the following, we use tableau rules for 2 and ⋄, using the equivalences 2β ≡ (β ∧ 2β)) and 3β ≡ (β ∨ 3β)). Observe that, as false box formulae correspond to negated until formulas, we need to label them with x. Example 2. Consider the domain description given in Example 1 with the constraints and the property given in Section 2.3. We describe some steps of the (non determin- istic) construction of a (k,l)-loop for k = 7. For the initial state s0 we have w0 = {Tmail(a), Fmail(b)}, x0 = 0, f0 = X. F0 contains the following formulas: F0 .1 : Thbegini⊤ F0 .2 : T2[begin]hA(q0 )i⊤ F0 .3 : F21 (mail(a) ⊃ 3¬mail(a)) F0 .4 : T[begin]hA(q0 )i⊤− from F0 .2 F0 .5 : T 2[begin]hA(q0 )i⊤ from F0 .2 F0 .6 : F 21 (mail(a) ⊃ 3¬mail(a)) from F0 .3 The first two formulas are the two constraints, where the automaton A(q0 ) is equiva- lent to the regular program sense mail; (deliver(a) + deliver(b) + wait); begin (A has states {q0 , q1 , q2 , q3 }, initial state q0 , final state q3 and transition function q1 = δ(q0 , sense), q2 = δ(q0 , del(a)) = δ(q0 , del(b)) = δ(q0 , wait), q3 = δ(q2 , begin)). The third formula is the negation of the property. Note that the 2 operator has label 1 since x0 = 0. All other formulas are obtained by applying the tableau rules3 . Since F0 contains the formula Thbegini⊤, we can only execute action begin in s0 . In s1 we have w1 = {Tmail(a), Fmail(b)}, from the domain description, and x1 = 1, f0 = X. x1 changes its value from the previous state, because there are no formulas in s0 with label 0. F1 is obtained by propagating the “next” formulas in F0 and by applying tableau to them: F1 .1 : ThA(q0 )i0 ⊤ from F0 .4 F1 .2 : T2[begin]hA(q0 )i⊤ from F0 .5 F1 .3 : F21 (mail(a) ⊃ 3¬mail(a)) from F0 .6 F1 .4 : ThsenseihA(q1 )i0 ⊤ from F1 .1 F1 .5 : T[begin]hA(q0 )i⊤ from F1 .2 F1 .6 : T 2[begin]hA(q0 )i⊤ from F1 .2 F1 .7 : F(mail(a) ⊃ 3¬mail(a)) from F1 .3 F1 .8 : F¬mail(a)) from F1 .7 F1 .9 : F3¬mail(a)) from F1 .7 F1 .10 : F 3¬mail(a)) from F1 .9 Because of F1 .4 the next action will be sense. This action is non deterministic, and we choose w2 = {Tmail(a), Tmail(b)}. By continuing with the construction, we can get the following path (we omit the value of the Fi ’s in the states, and we write a form mail(a) and b for mail(b)): begin sense del(b) (F0 , {Ta, Fb}, 0, X) → (F1 , {Ta, Fb}, 1, X) → (F2 , {Ta, Tb}, 0, X) → begin sense del(b) (F3 , {Ta, Fb}, 0, ↓) → (F4 , {Ta, Fb}, 0, ↓) → (F5 , {Ta, Tb}, 1, X) → begin sense (F6 , {Ta, Fb}, 1, ↓) → (F7 , {Ta, Fb}, 1, ↓) → (F8 , {Ta, Tb}, 0, X) Since F8 = F2 , the two states n8 and n2 are equal. Thus we have an arc back from s7 to s2 , and the path from s2 to s7 contains an accepting state. The path represents a counterexample to the property we wanted to prove. Let us modify the domain description by adding a fluent pr(E) which associates a priority to the mailboxes. We can add the following rules: [deliver(E)]¬pr(E) [deliver(E)]pr(E ′ ) ← E 6= E ′ , mail(E ′ ) [deliver(E)] ⊥← ¬pr(E), pr(E ′ ), E 6= E ′ 3 For lack of space we consider only the most significant formulas. By applying function max, we obtain that the longest path has length 17. By exe- cuting function BM C(17) we get no solution. Therefore the property 2(mail(a) ⊃ 3¬mail(a)) holds in the modified domain description. 5 An ASP Encoding of BMC with Büchi Automata We now provide a translation into standard ASP of the above procedure for building a path of the product Büchi automaton. We use predicates like fluent, action, state to express the type of atoms. As we are interested in infinite runs represented as (k,l)-loops, we assume a bound K to the number of states. States are represented in ASP as integers from 0 to K, where K is given by the predicate laststate(State). The predicate occurs(Action,State) describes transitions. Occurrence of exactly one action per state can be encoded as: -occurs(A,S):- occurs(A1,S),action(A),action(A1),A!=A1,state(S). occurs(A,S):- not -occurs(A,S),action(A),state(S). As we have seen, states are associated with a set of fluent literals, a set of signed formulas, and the values of x and f . Fluent literals are represented with the predicate holds(Fluent,State), T or F formulas with tt(Formula,State) or ff(Formula, State), x with the predicate x(Val,State) and f with the predicate acc(State), which is true if State is an accepting state. States on the path must be all different, and thus we need to define a predicate eq(S1,S2) to check whether the two states S1 and S2 are equal: eq(S1,S2):- state(S1), state(S2),not diff(S1,S2). diff(S1,S2):- state(S1),state(S2),tt(F,S1),not tt(F,S2). diff(S1,S2):- state(S1),state(S2),holds(F,S1),not holds(F,S2). and similarly for other components of a state. The following constraint requires all states up to K to be different: :-state(S1),state(S2),S1!=S2,eq(S1,S2),laststate(K),S1<=K,S2<=K. Furthermore we need constraints stating that there is a transition from state K to a previous state L4 , and that there is a state S, L ≤ S ≤ K, such that acc(S) holds, i.e. S is an accepting state. To do this we compute the successor of state K, and check that it is equal to S. loop(L):- state(L), laststate(K), L<=K,SuccK=K+1, eq(L,SuccK). accept:- loop(L), state(S), laststate(K), L<=S, S<=K, acc(S). :- not accept. Given a domain description Π and a set of DLTL formulas ϕ1 , . . . ϕn , representing constraints or negated properties, we want to compute the temporal answer sets of the domain description Π satisfying the temporal formulas, if any. The rules in Π can be easily translated to ASP, similarly to [14]. In the following we provide the translation of our running example, see [19] for details. action(sense). action(deliver(a)). action(deliver(b)). 4 Since states are all different, there will be at most one state equal to the successor of K. action(wait). fluent(mail(a)). fluent(mail(b)). action effects: holds(mail(E),NS):- occurs(sense,S), fluent(mail(E)),NS=S+1, not -holds(mail(E),NS). -holds(mail(E),NS):-occurs(deliver(E),S),fluent(mail(E)),NS=S+1. persistence: holds(F,NS):- holds(F,S), fluent(F),NS=S+1,not -holds(F,NS). -holds(F,NS):- -holds(F,S),fluent(F),NS=S+1,not holds(F,NS). preconditions: :- occurs(deliver(E),S),-holds(mail(E),S). :- occurs(wait,S), holds(mail(E),S). initial state: -holds(mail(a),0). -holds(mail(b),0). DLTL formulas are represented as ASP terms. In the encoding, each formula αU A(q) β is represented as until(A,q,alpha,beta), where the automaton A is described by the predicates trans(A,Q1,Act,Q2) defining transitions, and final(A,Q) defining final states. Predicate x(L,S) gives the value L = 0, 1 of x in state S. We introduce the terms until(A,q,alpha,beta,L) and diamond(Act,alpha) for encoding labeled until formulas and haiα formulas. The expansion of signed formulas can be formulated by means of ASP rules corresponding to the tableau rules given in the previous section. Disjunction: tt(F1,S) v tt(F2,S):- tt(or(F1,F2),S). ff(F1,S):- ff(or(F1,F2),S). ff(F2,S):- ff(or(F1,F2),S). Negation: ff(F,S):- tt(neg(F),S). tt(F,S):- ff(neg(F),S). Until: tt(until(Aut,Q,F1,F2,1-N),S):- state(S), tt(until(Aut,Q,F1,F2),S),x(N,S),label(N). tt(or(F2,and(F1,diamond(Act,until(Aut,Q1,F1,F2,L)))),S):- tt(until(Aut,Q,F1,F2,L),S),state(S),label(L),final(Aut,Q), occurs(Act,S),choose(until(Aut,Q,F1,F2,L),S,Act,Q1). tt(and(F1,diamond(Act,until(Aut,Q1,F1,F2,L))),S):- state(S), tt(until(Aut,Q,F1,F2,L),S),label(L),not final(Aut,Q), occurs(Act,S),choose(until(Aut,Q,F1,F2,L),S,Act,Q1). ff(F2,S):- state(S),ff(until(Aut,Q,F1,F2),S), final(Aut,Q). ff(diamond(Act,until(Aut,Q1,F1,F2)),S):-state(S), occurs(Act,S),ff(until(Aut,Q,F1,F2),S),trans(Aut,Q,Act,Q1). Diamond tt(F,NS):- tt(diamond(Act,F),S), NS=S+1. ff(F,NS):- ff(diamond(Act,F),S),occurs(Act,S), NS=S+1. Note that, to express splitting of sets of formulas, as in the case of disjunction, we can exploit disjunction in the head of clauses, provided by some ASP languages such as DLV, or choice constructs available in other languages. The predicate choose below non deterministically chooses a transition Q1 among those possible for action Act in the automaton Aut, and uses that choice in the expansion of the until formula: choose(until(Aut,Q,F1,F2,L),S,Act,Q1):- state(S),action(Act), not-choose(until(Aut,Q,F1,F2,L),S,Act,Q1),trans(Aut,Q,Act,Q1). -choose(until(Aut,Q,F1,F2,L),S,Act,Q1):- state(S),action(Act), choose(until(Aut,Q,F1,F2,L),S,Act,Q2),Q1!=Q2. Inconsistency of signed formulas is formulated with the following constraints: :- ff(true,S), state(S). :- tt(F,S), ff(F,S), state(S). :- tt(diamond(Act1,F),S),tt(diamond(Act2,F),S), Act1!=Act2. :- tt(F,S), not holds(F,S). :- ff(F,S), not -holds(F,S). As a difference W with the tableau construction, rather than introducing the translation of formula T a∈Σ hai⊤ in the initial state, we include the rule tt(diamond(A,true),S):- occurs(A,S). as we know that at least one action (and at most one) occurs in a state. Predicates x and acc are defined as follows: cont(S):-state(S),x(Lab,S),tt(diamond( ,until( , , ,Lab)),S). x(Lab,SN):- x(Lab,S),SN=S+1, cont(S). -acc(SN):- x(Lab,S),SN=S+1, cont(S). x(1-Lab,SN):- x(Lab,S),SN=S+1, not cont(S). acc(SN):- x(Lab,S),SN=S+1, not cont(S). x(0,0). acc(0). Finally, we must add a fact tt(tr(ϕi ),0) for each DLTL formula ϕi to be satisfied in the model, where tr(ϕi ) is the ASP term representing ϕi . It is easy to see that the (groundization of the) encoding in ASP is linear in the size of the formula φ to be verified and in the number f of ground fluents while quadratic in the size of k. We can prove that there is a one to one correspondence between the extensions of a domain description satisfying a given temporal formula and the answer sets of the ASP program encoding the domain and the formula. Proposition 3. Let Π be a domain description whose temporal answer sets are total, let tr(Π) be the ASP encoding of Π (for a given k), and let φ be a DLTL formula. If there is a temporal answer set of Π that satisfies the formula φ, then there exists an answer sets of the ASP program tr(Π) ∪ tt(tr(φ), 0) (where tr(φ) is the ASP term representing φ); and vice versa. For achieving completeness, the search for the longest simple path can be done by removing from the above ASP encoding the rules for defining loops and the rules for defining the Büchi acceptance condition. The translation has been run in iClingo [13]. For the dining philosophers problems in [23], the scalability of the approach in this paper is similar to the one for the method (without Büchi automaton) in [19] and the one in [23], when looking for a counterex- ample. E.g., a counterexample for DP(12) is found in 183 seconds, wrt 274 seconds for a Clingo implementation of the method in [19] — see also Appendix C in that pa- per. The search for the longest simple path is substantially more costly and practically feasible only for problems where the action domain is sufficiently constrained. 6 Conclusions The paper presents a bounded model checking approach for the verification of prop- erties of temporal action theories in ASP. The temporal action theory is formulated in a temporal extension of ASP, where DLTL constraints in domain descriptions allow for state trajectory constraints to be captured. The approach provides a uniform ASP metodology for specifying and verifying domain descriptions, which can be used for several reasoning tasks, including business process verification [10] and planning. Helianko and Niemelä [23] developed a compact encoding of bounded model check- ing of LTL formulas as the problem of finding stable models of logic programs. In [19] this encoding is extended to address the verification of action domains including DLTL constraints. In this paper, we follow a different approach to BMC which exploits the Büchi automaton construction to achieve completeness. [8] first proposed the use of the Büchi automaton in BMC. As a difference, our encoding in ASP is defined without assuming that the Büchi automaton is computed in advance. The action language in this paper is related to the logic programming based plan- ning language K [12] and with the languages C and C + [21, 20]. Unlike K, C and C + our action language does not allow for concurrent actions, but it provides general temporal constraints. K, C and C + can perform several kinds of reasoning, such as, prediction, postdiction and planning. However, they do not exploit standard temporal logic con- structs to reason about actions. ESG [9] is a second order extension of CTL* for reasoning about nonterminating Golog programs. The paper presents a method for verification of a first order CTL fragment of ESG, using model checking and regression based reasoning. Because of first order quantification, this fragment is in general undecidable. In [1] the verification problem for action logic programs with nonterminating behav- ior is addressed using an action formalism based on a temporalized description logic, ALCO-LTL. DLTL does not allow for first order constructs as ALCO-LTL, while it allows for the specification of regular expressions. In [6] Cabalar introduces normal forms for Temporal Equilibrium Logic (TEL), an extension of the Answer Set semantics to arbirary theories in the syntax of Linear Temporal Logic. The rules in Π, in our action theories, appear to be in normal form. It would be interesting to investigate the possibility of mapping the LTL fragment of our action theories into TEL. Acknowledgments We thank the anonymous referees for their helpful comments. This work has been par- tially supported by the project of Regione Piemonte “ICT4Law”. References 1. Franz Baader, Hongkai Liu, and Anees ul Mehdi. Verifying properties of infinite sequences of description logic actions. In ECAI, pages 53–58, 2010. 2. F. Bacchus and F. Kabanza. Using temporal logics to express search control knowledge for planning. Artificial Intelligence, 116(1-2):123–191, 2000. 3. Jorge A. Baier, Fahiem Bacchus, and Sheila A. McIlraith. A heuristic search approach to planning with temporally extended preferences. Artif. Intell., 173(5-6):593–618, 2009. 4. C. Baral and J. Zhao. Non-monotonic temporal logics for goal specification. In IJCAI 2007, pages 236–242, 2007. 5. A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in Computers, 58:118–149, 2003. 6. Pedro Cabalar. A normal form for linear temporal equilibrium logic. In JELIA, LNCS 6341, pages 64–76, 2010. 7. Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT Press, 2001. 8. E.M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking. In VMCAI, pages 85–96, 2004. 9. J. Claßen and G. Lakemeyer. A logic for non-terminating Golog programs. In Proc. KR 2008, pages 589–599, 2008. 10. D. D’Aprile, L. Giordano, V. Gliozzi, A. Martelli, G.L. Pozzato, and D. Theseider Dupré. Verifying business process compliance by reasoning about actions. In CLIMA 2010, LNCS 6245, 2010. 11. Giuseppe De Giacomo, Fabio Patrizi, and Sebastian Sardiña. Generalized planning with loops under strong fairness constraints. In Proc. KR 2010, 2010. 12. T. Eiter, W. Faber, N. Leone, G. Pfeifer, and A. Polleres. A logic programming approach to knowledge-state planning: Semantics and complexity. ACM TOCL, 5(2):206–263, 2004. 13. M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, and S. Thiele. Engineering an incremental ASP solver. In Proc. ICLP08, volume 5366 of LNCS, pages 190–205, 2008. 14. M. Gelfond. Handbook of Knowledge Representation, ch. 7, Answer Sets. Elsevier, 2007. 15. A. Gerevini and D. Long. Plan constraints and preferences in PDDL3. Technical Report, Department of Electronics and Automation, University of Brescia, Italy, 2005. 16. R. Gerth, D. Peled, M.Y.Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In 15th Work. Protocol Specification, Testing and Verification, 1995. 17. L. Giordano and A. Martelli. Tableau-based automata construction for dynamic linear time temporal logic. Annals of Mathematics and AI, 46(3):289–315, 2006. 18. L. Giordano, A. Martelli, and C. Schwind. Specifying and verifying interaction protocols in a temporal action logic. Journal of Applied Logic, 5:214–234, 2007. 19. L. Giordano, A. Martelli, and D. Theseider Dupré. Reasoning about actions with temporal answer sets. TPLP, To appear. Available at http://arxiv.org/abs/1110.3672. 20. E. Giunchiglia, J. Lee, V. Lifschitz, N. McCain, , and H. Turner. Nonmonotonic causal theories. Artificial Intelligence, 153(1-2):49–104, 2004. 21. E. Giunchiglia and V. Lifschitz. An action language based on causal explanation: Preliminary report. In AAAI/IAAI, pages 623–630, 1998. 22. F. Giunchiglia and P. Traverso. Planning as model checking. In Proc. The 5th European Conf. on Planning (ECP’99), pages 1–20, 1999. 23. K. Heljanko and I. Niemelä. Bounded LTL model checking with stable models. TPLP, 3(4-5):519–550, 2003. 24. J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied logic, 96(1-3):187–207, 1999. 25. M. Pistore and P. Traverso. Planning as model checking for extended goals in non- deterministic domains. In Proc. IJCAI 2001, pages 479–486, 2001. 26. S. Sohrabi and S. A. McIlraith. Optimizing web service composition while enforcing regu- lations. In ISWC 2009, Chantilly, USA, LNCS 5823, pages 601–617, 2009.