In intelligent agents, memory has a very important and decisive role for the choice of future behaviors, since it is progressively formed through the agent's interactions with the external environment. Previous works exist in the logic concerning the formalization of the reasoning on the formation of beliefs in non-omniscient agents. We extend this work by inserting the concept of time through a particular function that assigns a \timing" to beliefs, inferences and modal operators.
Memory in an agent system is a process of reasoning: in particular, it is the learning process of strengthening a concept.
The interaction between the agent and the environment can play an
important role in constructing its memory and may a ect its future behaviour, the
latter due to the proactive and deliberative capabilities of the agent themselves.
In fact, through memory an agent is potentially able to recall and to learn from
experiences so that its beliefs and its future course of action are grounded in these
experiences. Most of the methods to design agent memorization mechanisms have
been inspired by models of human memory [
Atkinson and Shi rin in [3] proposed a model of human memory which consists of three distinct memory stores, the sensory register where information are stored which are detected from senses, the short term memory (or working memory) where explicit beliefs are stored and the long term memory which stores the background knowledge; information passes from store to store in a linear way.
This model has been further enhanced by Gero and Liew in [4], and [5] for constructive memory. Memory construction occur whenever an agent uses past experience in the current environment in a situated manner. The exploitation of \memories" requires the interaction among this di erent memory components. Such correlation can be obtained in various ways, e.g., via neural networks, via mathematical models or via logical deduction.
In computational logic, [6] introduces DLEK (Dynamic Logic of Explicit beliefs and Knowledge) as a logical formalization of SOAR (State Operator And Result) Architecture [7], which is one of the most popular cognitive architecture. The underlying idea is to represent reasoning about the formation of beliefs through perception and inference in non-omniscient resource-bounded agents. They consider perception, short-term memory (also called \working memory"), long-term memory (also called \background knowledge") and their interaction. DLEK is a logic that consists of a static part called LEK (Logic of Explicit beliefs and Knowledge), which is an epistemic logic, and a dynamic component, which extends the static one with \mental operations". Resource-boundedness in DLEK is modeled via the assumption that beliefs are kept in the short-term memory, while implications that allow reasoning to be performed are kept in the long-term memory. New beliefs can be formed in DLEK either from perception, or from previous beliefs in short-term memories and rules in the background knowledge. Inferences that add new beliefs are performed one step at a time via an interaction between short- and long-term memories in consequence of an explicit \mental operation" that will occur whenever an agent deems it necessary and can allot the needed time [8, 9].
DLEK has however no notion of time, while agents' actual perceptions are inherently timed and so are many of the inferences drawn from such perceptions. In this paper we present an extension of LEK/DLEK to T-LEK/T-DLEK (\Timed LEK" and \Timed DLEK") obtained by introducing a special function which associates to each belief the arrival time and controls timed inferences. Through this function it is easier to keep the evolution of the surrounding world under control and the representation is more complete. The issue of time in agents has been coped with in several other works, (see, e.g., among many, [10{ 13]), where however the objective is that of dealing with time in communication and coordination among agents; thus, our attempt to deal with time in memory management is a novelty in the literature.
In the rest of the paper, Sections 2 and 3 present syntax, semantics of the extended logic, the axiomatization, and the canonical model. In Section 4 we propose a brief discussion on complexity and conclude. This paper is an extended version of [14], where we have introduced explicit time instants and time intervals in formulas. This is relevant because agents' perceptions (that may become beliefs) are always inherently timed, and so are the conclusions that can be drawn from them. But to avoid problems with the management of the intervals and in order to not lose the logic of the formalization, in this paper we have introduced a new function that associated to each atom the interval of validity, moreover we can inherit the proofs of lemmas, theorems from [6]. 2
As in [6], our logic consists of two di erent components: a static component, called T-LEK, which is mix between an Epistemic Logic and Metric Temporal Logic ([15]), and a dynamic component, called T-DLEK, which extend the static one with mental operation, which are vary important for \controlling" beliefs (adds new belief, update belief, etc). 2.1
As it is customary in logic programming, we assume a signature specifying (countable) sets of predicate, function, and constant symbols. From constant and function symbols, compound terms are built as usual. The Herbrand universe is the collection of all such terms (which includes constant symbols). We assume that the integer numbers and the symbol 1 are included among the constant symbols and that the arithmetic operators are included among the function symbols. Consequently, arithmetic expressions are terms of the signature. Atoms have the form pred ( 1; : : : ; n) where pred is a predicate symbol, n 0 is its arity and 1; : : : ; n are terms. We denote by Atm the countable set of atoms of the signature (i.e., the Herbrand base).
In our scenario we x Atm = fp(t1; t2); q(t3; t4), ... ,h(ti; tj )g where ti 6 tj and p; q; h are predicates, that can be equal or not. Moreover p(t1; t2) stands for \p is true from the time instant t1 to t2" with t1; t2 2 N (Temporal Representation of the external world); as a special case we can have p(t1; t1) which stands for \p is true in the time instant t1". Obviously we can have predicates with more terms tha only two but in that case we x that the rst two must be those that identify the time duration of the belief (i.e. open(1; 3; door) which means \the agent knows that the door is open from time one to time 3"). Instead in the previous work [14] we considered atoms of the form pI with I = [t1; t2], which are the conjunction pt1 ^ pt1+1 ^ ^ pt2 and also pt stand for pIt with It = [t; t]; we have decided to change approach because pI is too detached from propositional logic.
Below is the de nition of the formulas of the language LT -LEK , with a slight abuse, in this grammar we use I as terminal symbol standing for time intervals (possibly speci ed through arithmetic expressions, as said earlier): '; := p(t1; t2) j :' j I ' j B ' j K 'j ' ^ j ' ! Others Boolean connectives >, ?, $ are de ned from : and ^ as usual. In the formula I the MTL Interval \always" operator is applied to a formula; I is a \time-interval" which is a closed nite interval [t; l] or an in nite interval [t; 1) (considered open on the upper bound), for any expressions/values t; l such that 0 t l and [0;1) will sometimes be written simply as . The operator B is intended to denote belief and the operator K to denote knowledge. More precisely the B identi es beliefs present in the working memory, instead K identi es what rules present in the background knowledge.
Terms/atoms/formulas as de ned so far are ground, namely there are no variables occurring therein. We introduce variables and use them in formulas in a restricted manner, as usual for example in answer set programming [16]. Variables can occur in formulas in any place constants can occur and are intended as place holders for elements of the Herbrand universe. More speci cally, a ground instance of a term/atom/formula involving variables is obtained by uniformly substituting ground terms to all variables (grounding step), with the restriction that any variable occurring in an arithmetic expression (i.e., specifying a time instant) can be replaced by a (ground) arithmetic expressions only. Consequently, a non-ground term/atom/formula represents the possibly in nite set of its ground instances, namely, its grounding. Notice that the rational of considering ground formulas is that they represent perceptions (either new or already recorded in agent's memory) coming in general from the external world(we say \in general" as, in fact, in some of the aforementioned agent-oriented frameworks perceptions can also result from internal events, i.e., from an agent's observations of its own internal activities). As it is customary in logic programming, variable symbols are indicated with an initial uppercase letter whereas constants/functions/predicates symbols are indicated with an initial lowercase letter.
The language LT -DLEK of Temporalized DLEK (T-DLEK) is obtained by augmenting LT LEK with the expression [ ] , where denotes a mental operation and is a ground formula. The mental operations that we consider are essentially the same as in [6]: { +', where ' is a ground formula of the form p(t1; t2) or :p(t1; t2): the mental operation that serves to form a new belief from a perception '. A perception may become a belief whenever an agent becomes \aware" of the perception and takes it into explicit consideration. Notice that ' may be a negated atom. { \('; ): believing both ' and , an agent starts believing their conjunction. { `('; ), where is a ground atom, say p(t1; t2): an agent, believing that ' is true and having in its long-term memory that ' implies (in some suitable time interval including [t1; t2]), starts believing that p(t1; t2) is true. { a('; ) where ' and are ground atoms, say p(t1; t2) and q(t3; t4) respectively: an agent, believing p(t1; t2) and having in the long-term memory that p(t1; t2) implies :q(t3; t4), removes the timed belief q(t3; t4) if the intervals match. Notice that, should q be believed in a wider interval I such that [t1; t2] I, the belief q(:; :) is removed concerning intervals [t1; t2] and [t3; t4], but it is left for the remaining sub-intervals (so, its is \restructured"). The last mental operation, which is a sort of \update" or \restructuring operator", substitutes ' ([6]), that instead represents arbitrary \forgetting", i.e., removing a belief from the short-term memory. In fact in [6] there are +', ', `('; ) and a('; ).
Example 1: We propose a small example to illustrate the form and the role of rules in the working memory and in the long-term memory. If at time t=2 it is starting raining, in the agent's working memory there will be the following belief: B(raining(2; 2)). And if we have in the background knowledge K(rain(t1; t2) ! take(t1; t2; umbrella)) and 2 2 [t1; t2] than the agent can infer B(take(2; 2; umbrella)), which is a new belief stored in the working memory. And if we have also K(rain(t1; t2)^take(t1; t2; umbrella) ! go(t1 +1; 1; shops)) than the agent can infer B(go(3; 1; shops)) which means that after getting the umbrella the agent can go around the shops.
Example 2: An example of a non-ground T-LEK formula is:
K( [t1;t2](enrollment (T ; T )) !
[t1;t2]( [T;T +14]send payment (T1 ; T1 ))) where we suppose that an agent knows that it is possible to enroll in the university in the period [t1; t2] and that, after the enrollment, the payment must be sent within fourteen days (still staying within the interval [t1; t2]). Since, by the restrictions on formulas stated earlier, it must be the case that T1 2 [T; T + 14] and both T , T + 14 must be in [t1; t2], only a nite set of ground instances of this formula can be formed by substituting natural numbers to the variables T; T1 (speci cally, the maximum number of ground instances is t2 t1 14 + 1 assuming to pay on the last day t2). In case one would consider the more general formula: K( [t1;t2](enrollment (T ; T ; X )) !
[t1;t2]( [T;T +14]send payment (T1 ; T1 ; X ))) where X represents a student of that university, i.e., student (:; :; X ) holds for some ground instance of X, then the set of ground instances would grow, as a di erent instance should be generated for each student (i.e., for each ground term replacing X). In practice, however, ground instances need not to be formed a priori, but rather they can be generated upon need when applying a rule; in the example, just one ground instance should be generated when some student intends to enroll in that university at a certain time T = t^. 2.2
Semantics of DLEK and T-DLEK are both based on a set W of worlds. In both DLEK and T-DLEK we have the valuation function: V : W ! 2Atm . Also we de ne the \time" function T that associates to each formula the time interval in which this formula is true and operates as follows: { T (p(t1; t2)) = [t1; t2], which stands for \p is true in the time interval [t1; t2]" where t1; t2 2 N; as a special case we have T (p(t1; t1)) = t1, which stands for \p is true in the time instant t1" where t1 2 N (time instant); { T (:p(t1; t2)) = T (p(t1; t2)), which stands for \p is not true in the time interval [t1; t2]" where t1; t2 2 N; { T (' op ) = T (') U T ( ) with op 2 f_; ^; !g, which means the unique smallest interval including both T (') and T ( ); { T (B') = T ('); { T (K') = T ('); { T ( I ') = I where I is a time interval in N; { T ([ ]') there are di erent cases depends on which kind of mental operations we applied: 1. T (+') = T ('); 2. T (\('; )) = T (') U T ( ); 3. T (`('; )) = T ( ); 4. T (a('; )) returns the restored interval where is true.
For a world w, let t1 the minimum time instant of T (p(t1; t1)) where p(t1; t1) 2 V (w) and let t2 be the supremum time instant (we can have t2 = 1) among the atoms in V (w). Then, whenever useful, we denote w as wI where I = [t1; t2], which identi es the world in a given interval.
The notion of LEK/T-LEK model does not consider mental operations, discussed later, and is introduced by the following de nition.
De nition 1. A T-LEK model is a tuple M = hW ; N ; R; V ; T i where: { W is the set of worlds; { V : W ! 2Atm valuation function; { T \time" function; { R W W is the accessibility relation, required to be an equivalence relation so as to model omniscience in the background knowledge s.t. R(w) = fv 2 W j wI R vI g called epistemic state of the agent in wI , which indicates all the situations that the agent considers possible in the world wI or, equivalently any situation the agent can retrieve from long-term memory based on what it knows in world wI ; { N : W ! 22W is a \neighbourhood" function, 8w 2 W , N (w) de nes, in terms of sets of worlds, what the agent is allowed to explicitly believe in the world wI ; 8wI ; vI 2 W , and X W :
set composed of reachable worlds; 2. if wI R vI , then N (wI ) N (vI ): if the world vI is compliant with the epistemic state of world wI , then the agent in the world wI should have a subset of beliefs of the world vI .
A preliminary de nition before the Truth conditions : let M = hW ; N ; R; V ; T i a T-LEK model. Given a formula ', for every wI 2 W , we de ne k ' kwMI = fvI 2 W j M; vI j= 'g \ R(wI ): Truth conditions for T-DLEK formulas are de ned inductively as follows: { M; wI j= p(t1; t2) i p(t1; t2) 2 V (wI ) and T (p(t1; t2)) I; { M; wI j= :' i M; wI 2 ' and T (:') I; { M; wI j= ' ^ i M; wI j= ' and M; wI j= with T ('); T ( ) I; { M; wI j= ' _ i M; wI j= ' or M; wI j= with T ('); T ( ) I; { M; wI j= ' ! i M; wI 2 ' or M; wI j= with T ('); T ( ) I; { M; wI j= B ' i k ' kwMI 2 N (wI ) and T (') I; { M; wI j= Ki ' i for all vI 2 R(wI ), it holds that M; vI j= ' and T (') I; { M; wI j= J ' i T (') J I and for all vI 2 R(wI ), it holds that M; vI j= '; In particular, considering formulas of the forms B ' and K ', we observe
M that M; wI j= B ' if the set k ' kwI of worlds reachable from wI which entail ' in the very same model M belongs to the neighbourhood N (wI ) of wI . Hence, knowledge pertains to formulas entailed in model M in every reachable world, while beliefs pertain to formulas entailed only in some set of them, where this set must however belong to the neighbourhood and so it must be composed of reachable worlds. Thus, an agent is seen as omniscient with respect to knowledge, but not with respect to beliefs.
Concerning a mental operation performed by any agent i, we have: M; wI j= [ ] ' i M ; wI j= ' and T (') I where M = hW ; N (wI ); R; V ; T i Here represents a mental operation a ecting the sets of beliefs. In particular, such operation can add new beliefs by direct perception, by means of one inference step, or as a conjunction of previous beliefs. When introducing new beliefs, the neighbourhood must be extended accordingly, as seen below; in particular, the new neighbourhood N (wI ) is de ned for each of the mental operations as follows. { Learning perceived belief:
N +'(wI ) = N (wI ) [ k ' kwMI with T (') I.
The agent adds to its beliefs perception ' (namely, an atom or the negation of an atom) perceived at a time in T ('); the neighbourhood is expanded to as to include the set composed of all the reachable worlds which entail ' in M . { Beliefs conjunction: 8< N (wI ) [ k ^ kwMI if M; wI j= B( ) ^ B( ) N \( ; )(wI ) = and T (\( ; )) I
: N (i; wI ) otherwise The agent adds ^ as a belief if it has among its previous beliefs both and , with I including all time instants referred to by them; otherwise the set of beliefs remain unchanged. The neighbourhood is expanded, if the operation succeeds, with those sets of reachable worlds where both formulas are entailed in M . { Belief inference:
8 N (wI ) [ N `( ; )(wI ) = < k kwMI if M; wI j= B( ) ^ K( ! )
and T (` ( ; )) I : N (wI ) otherwise The agent adds the ground atom as a belief in its short-term memory if it has among its previous beliefs and has in its background knowledge K( ! ), where all the time stamps occurring in and in belong to I. Observe that, if I does not include all time instants involved in the formulas, the operation does not succeed and thus the set of beliefs remains unchanged. If the operation succeeds then the neighbourhood is modi ed by adding as a new belief. { Beliefs revision (applied only on ground atoms).
Given Q = q(j; k) s.t. T (q(j; k)) = T (q(t1; t2)) \ T (q(t3; t4)) with j; k 2 N and P = M; wI j= B(p(t1; t2)) ^ B(q(t3; t4)) ^ K(p(t1; t2) ! :q(t3; t4)) and T (a (p(t1; t2); q(t3; t4))) I and there is no interval J ) T (p(t1; t2)) s.t. B(q(t5; t6)) where T (q(t5; t6))=J : N a(p(t1;t2);q(t3;t4))(wI ) = N (wI ) n k Q kwMI if P
N (i; wI ) otherwise The agent believes that q(t3; t4) holds only in the interval T (q(t3; t4)) and has the perception of p(t1; t2) where T (p(t1; t2)) T (q(t3; t4)). Then, the agent replaces previous belief q(t3; t4) in the short-term memory with q(t5; t6) where T (q(t5; t6))=T (q(t3; t4)) n T (q(t1; t2)). In general, the set T (q(t3; t4)) n T (q(t1; t2)) is not necessarily an interval: being T (p(t1; t2)) T (q(t3; t4)), with T (p(t1; t2))=[t1; t2], and T (q(t3; t4))=[t3; t4], we have that T (q(t3; t4)) n T (q(t1; t2))=[t3; t1 1][[t2 + 1; t4]. Thus, q(t3; t4) is replaced by q(t3; t1 1) and q(t2 + 1; t4) (and similarly if t4 = 1).
We write j=T -DLEK ' to denote that ' is true in all worlds wI , of every TLEK model M .
Example 3: Let us consider the example of a person who is married or divorced, where only the perform can perform the action to be married or divorced. Let us assume that performed actions are recorded among an agent's perceptions, with the due time stamp. For reader's convenience, actions are denoted using a su x \A". For simplicity, actions are supposed to always succeed and to produce an e ect within one time instant. Let us consider the following rules (kept in long-term memory):
K(marry (T ; T )A ! married (T + 1 ; 1))
K(divorce(T ; T )A ! divorced (T + 1 ; 1)): Let us now assume that a person married, e.g., at time 5; then, a belief will be formed of the person is married from time 6 on; however, if that person later divorced, e.g., at time 8, as a consequence result that s(he) is divorced from time 9. It can be seen that the application of previous rules in consequence of an agent's action of marring/divorcing determines some \belief restructuring" in the short-term memory of the agent. In absence of other rules concerning marriage, we intend that a person can not be simultaneously married and divorced. The related belief update is determined by the following rules:
K(married (T ; 1) ! :divorced (T ; 1))
K(divorced (T ; 1) ! :married (T ; 1)) With the above timing, the result of their application is that the belief formed at time 5, i.e., married(6; 1) will be replaced by married(6; 8) plus divorced(9; 1). Property 1: For the mental operations previously considered we have the following (where '; are as explained earlier): { j=T -DLEK [+']B'.
Namely, as a consequence of the operation +' (thus after the perception of ') the agent i adds ' to its beliefs. { j=T -DLEK (B' ^ B ) ! [\('; )]B(' ^ ).
Namely, if an agent has ' and as beliefs, then as a consequence of the mental operation \('; ) the agent starts believing ' ^ ; { j=T -DLEK (K(' ! ) ^ B ') ! [`('; )] B .
Namely, if an agent has ' as one of its beliefs and has K('! ) in its background knowledge, then as a consequence of the mental operation `('; ) the agent starts believing ; { j=T -DLEK (K(p(t1; t2) ! :q(t3; t4)) ^ B (p(t1; t2)) ^ B (q(t3; t4))) ! [a(p(t1; t2); q(t3; t4))] (B (q(t5; t6))) where T (q(t5; t6)) = T (q(t3; t4)) n T (q(t1; t2)).
Namely, if an agent has q(t3; t4) as one of its beliefs, q is not believed outside T (q(t3; t4)), the agent perceives p(t1; t2) where T (p(t1; t2)) T (q(t3; t4)), and has K(p(t1; t2) ! :q(t3; t4)) in its background knowledge. Then after the mental operation a(p(t1; t2); q(t3; t4)) the agent starts believing q(t5; t6)) where T (q(t5; t6)) = T (q(t3; t4)) n T (q(t1; t2)). 3
The logic T-DLEK can be axiomatized as an extension of the axiomatization of DLEK as follows. We implicitly assume modus ponens, standard axioms for classical propositional logic, and the necessitation rule. The T-LEK axioms are the following:
The axiomatization of T-DLEK, involves these axioms: 1. [ ]f $ f where f = p or f = pt or f = pI ; 9.
$ ' $ '[ = ] with in '.
where '[ = ] denotes the formula obtained by replacing 2. [ ]:' $ :[ ]'; 3. [ ](' ^ ) $ [ ]' ^ [ ] ; 4. [ ]K(') $ K [ ](') ; _ B' ^ K('!: ) ^ K [a('; )] $: ; ; 8. [\('; )]B $ B [\('; )]
_ (B' ^ B ) ^ K [\('; )] $ (' ^ ) ; We write T-DLEK ` ' to indicate that ' is a theorem of TDLEK.
Both logics T-LEK and T-DLEK are sound for the class of T-LEK models. The proof that T-DLEK is strongly complete can be achieved by using a standard canonical model argument.
The canonical T-LEK model is a tuple Mc = hWc; Nc; fRc; Vc; Tci where: { Wc is the set of all maximal consistent subsets of LT -LEK ; so, as in [6], canonical models are constructed from worlds which are sets of syntactically correct formulas of the underlying language and are in particular the largest consistent ones. As before, each w 2 Wc can be conveniently indicated as wI . { For every wI 2 W and wI RcvI if and only if K' 2 wI i K' 2 vI ; i.e., Rc is an equivalence relation on knowledge; as before, we de ne Rc(wI ) = fvI 2 W j wI Rci vI g. Thus, we cope with our extension from knowledge of formulas to knowledge of formulas. { Analogously to [6], for wI 2 W , 2 LT -LEK we de ne A (wI ) = fvI 2
Rc(wI ) j 2 vI g. Then, we put Nc(wI ) = fA (wI ) j B 2 wI g. { Vc is a valuation function de ned as before. { Tc is a \time" function de ned as before.
As stated in Lemma 2 of [6], there are the following immediate consequences of the above de nition: if wI 2 Wc and i 2 Ag, then { for 2 LT -LEK , it holds that K
wI RcvI we have 2 vI ; { for 2 LT -LEK , if B 2 wI and wI RcvI then B 2 vI .
2 wI if and only if 8vI 2 W such that
Thus, while Rc-related worlds have the same knowledge and Nc-related worlds have the same beliefs, as stated in Lemma 3 of [6] there can be Rc-related worlds with di erent beliefs. The above properties can be used analogously to what is done in [6] to prove that, by construction, the following results hold:
if Mc; wI .
T-DLEK ` $ ~.
2 LT -DLEK then there exists ~ 2 LT -LEK such that Under the assumption that the interval I is nite, the previous lemmas allow us to prove the following theorems. The limitation to nite intervals is not related to features of the proposed approach, but to well-known paradoxes of temporal logics on in nite intervals.
Theorem 1. T-LEK is strongly complete for the class of T-LEK models. Theorem 2. T-DLEK is strongly complete for the class of T-LEK models.
With the new formalization of time intervals proposed in this paper, the proof of Theorem 2 immediately follows from the proof proposed in [6]. 4
In this work we extended an existing approach to the logical modeling of shortterm and long-term memories in Intelligent Resource-Bounded Agents by introducing the T function, which manages the interval when an atom is true. Through this function we are also able to assign a \timing" to the epistemic operators B and K. Moreover we add the always operator I of the Metric Temporal Logic to increase the expressiveness of our logic. We considered not just adding new beliefs, rather we introduced a new mental operation not provided in DLEK, to allow for removing/restructuring existing beliefs. The resulting TDLEK logic shares similarities in the underlying principles with hybrid logics (cf., e.g., [17]) and with temporal epistemic logic (cf., e.g., [18]); as concerns the di erences, the former has time instants but no time intervals, and the latter has neither time instants nor time intervals.
With regard to complexity for the mono agent case, which we are in, for LEK it has been proved that the satis ability problem is decidable and it has been proved to be in NP-complete, instead for DLEK it has been conjectured to be PSPACE. It is easy to believe that our extensions cannot spoil decidability because the T function do not interfere. Inference steps to derive new beliefs are analogous to D-LEK: just one modal rule at a time is used and a sharp separation is postulated between the working memory, where inference is performed, and the long-term memory.
Future developments could be the extension to the multi-agent case also reconsidering the complexity. 2. Logie, R.H.: Visuo-spatial working memory. (1994) 3. Atkinson, R.C., Shi rin, R.M.: Human memory: A proposed system and its control processes. Psychology of learning and motivation 2 (1968) 89{195 4. Liew, P.S., Gero, J.S.: An implementation model of constructive memory for situated design agent. (2002) 257{276 5. Gero, J.S., Peng, W.: Understanding behaviors of a constructive memory agent:
A markov chain analysis. Knowledge-Based Systems 22(8) (2009) 610{621 6. Balbiani, P., Duque, D.F., Lorini, E.: A logical theory of belief dynamics for resource-bounded agents. In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, AAMAS 2016, ACM (2016) 644{652 7. Laird, J.E., Lebiere, C., Rosenbloom, P.S.: A standard model of the mind: Toward a common computational framework across arti cial intelligence, cognitive science, neuroscience, and robotics. AI Magazine 38(4) (2017) 13{26 8. Alechina, N., Logan, B., Whitsey, M.: A complete and decidable logic for resourcebounded agents. In: 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), 19-23 August 2004, New York, NY, USA, IEEE Computer Society (2004) 606{613 9. Grant, J., Kraus, S., Perlis, D.: A logic for characterizing multiple bounded agents.
Autonomous Agents and Multi-Agent Systems 3(4) (2000) 351{387 10. Bansal, A.K., Ramamohanarao, K., Rao, A.S.: Distributed storage of replicated beliefs to facilitate recovery of distributed intelligent agents. In Singh, M.P., Rao, A.S., Wooldridge, M., eds.: Intelligent Agents IV, Agent Theories, Architectures, and Languages, 4th International Workshop, ATAL '97, Proceedings. Volume 1365 of Lecture Notes in Computer Science., Springer (1997) 77{91 11. Omicini, A., Ricci, A., Viroli, M.: Timed environment for web agents. Web Intelligence and Agent Systems 5(2) (2007) 161{175 12. Micucci, D., Oldani, M., Tisato, F.: Time-aware multi agent systems. In Weyns, D., Holvoet, T., eds.: Multiagent Systems and Software Architecture, Proceedings of the Special Track at Net.ObjectDays, Katholieke Universiteit Leuven, Belgium (2006) 71{78 13. Chesani, F., Mello, P., Montali, M., Torroni, P.: Monitoring time-aware commitments within agent-based simulation environments. Cybernetics and Systems 42(7) (2011) 546{566 14. Costantini, S., Formisano, A., Pitoni, V.: Timed memory in resource-bounded agents. In Ghidini, C., Magnini, B., Passerini, A., Traverso, P., eds.: AI*IA 2018 Advances in Arti cial Intelligence - XVIIth International Conference of the Italian Association for Arti cial Intelligence, Proceedings. Volume 11298 of Lecture Notes in Computer Science., Springer (2018) 15{29 15. Koymans, R.: Specifying real-time properties with metric temporal logic. Real
Time Systems 2(4) (1990) 255{299 16. Gelfond, M., Kahl, Y.: Knowledge Representation, Reasoning, and the Design of Intelligent Agents The Answer-Set Programming Approach. Cambridge University Press (2014) 17. Areces, C., Blackburn, P., Marx, M.: Hybrid logics: Characterization, interpolation and complexity. J. Symb. Log. 66(3) (2001) 977{1010 18. Engelfriet, J.: Minimal temporal epistemic logic. Notre Dame Journal of Formal Logic 37(2) (1996)