Memory in an agent system is a process of reasoning: it is the l earning process of strengthening a concept. The interaction between an agent and the environment can pla y an important role in constructing its memory and may affect its future behaviour. In fact, through memory an agent is potentially able to recall and to learn from experiences so that its beliefs and i ts future course of action are grounded in these experiences. In computational logic, [2] introduces DLEK (Dynamic Logic of Explicit beliefs and Knowledge) as a logical formalization of the short-term and long-term memory. The underlying idea is to represent reasoning about the formation of beliefs throu gh perception and inference in non-omniscient resource-bounded agents. 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 LE K" and "Timed DLEK") obtained by introducing a special function which associates to each b elief the arrival time and controls timed inferences. Through this function it is easier to keep the ev olution of the surrounding world under control and the representation is more complete. This abstr act is an evolution version of [3], where we have introduced explicit time instants and time intervals i n formulas, and it is extracted from [4].

In the literature there different kind of timed logical fram eworks exist, where time is specified directly using hybrid logics (cf., e.g., [2]), temporal epistemic lo gic (cf., e.g., [4]) or simply by using Linear Temporal Logic. We propose a temporal module which can be ado pted to "temporalize" many logical framework. This module is in practice a particular kind of fu nction that assigns a "timing" to atoms. We have exploited this T function in two different settings. The first one is the formalization of the reasoning on the formation of beliefs and the interaction wi th background knowledge in non-omniscient agents' memory.

Implementing Machine Ethics in Intelligent Agents involves trustworthiness and safety, meaning that agents should do what is expected they should do (at least, even in case of malfunctioning of any kind, concerning high-priority goals) and should not behave in unexpected potentially harmful ways. This topics are strongly related with "assurance", i.e., to ensuring that system users can rely upon the system. This paper deals with assurance of logical agent systems via temporal-logic-based runtime self-monitoring and checking.

The objective of my research project is the formal treatment of memory issues in Intelligent Software Agents. I extend recent work which proposed a (partial) formalization of SOAR architecture in modal logic, reasoning on a particular type of agents: resource-bounded agents. I introduce explicit treatment of time instants and time intervals by means of Metric Temporal Logic, both in the background logic and in mental operations.