Formalisms for agents reasoning with stochastic actions and perceptions.
The thesis reports on the development of a sequence of logics (formal languages based on mathematical logic) to deal with a class of uncertainty that agents may encounter. More accurately, the logics are meant to be used for allowing robots or software agents to reason about the uncertainty they have about the effects of their actions and the noisiness of their observations. The approach is to take the well-established formalism called the partially observable Markov decision process (POMDP) as an underlying formalism and then design a modal logic based on POMDP theory to allow an agent to reason with a knowledge-base (including knowledge about the uncertainties). First, three logics are designed, each one adding one or more important features for reasoning in the class of domains of interest (i.e., domains where stochastic action and sensing are considered). The final logic, called the Stochastic Decision Logic (SDL) combines the three logics into a coherent formalism, adding three important notions for reasoning about stochastic decision-theoretic domains: (i) representation of and reasoning about degrees of belief in a statement, given stochastic knowledge, (ii) representation of and reasoning about the expected future rewards of a sequence of actions and (iii) the progression or update of an agent’s epistemic, stochastic knowledge. For all the logics developed in this thesis, entailment is defined, that is, whether a sentence logically follows from a knowledge-base. Decision procedures for determining entailment are developed, and they are all proved sound, complete and terminating. The decision procedures all employ tableau calculi to deal with the traditional logical aspects, and systems of equations and inequalities to deal with the probabilistic aspects. Besides promoting the compact representation of POMDP models, and the power that logic brings to the automation of reasoning, the Stochastic Decision Logic is novel and significant in that it allows the agent to determine whether or not a set of sentences is entailed by an arbitrarily precise specification of a POMDP model, where this is not possible with standard POMDPs. The research conducted for this thesis has resulted in several publications and has been presented at several workshops, symposia and conferences.