Modeling Dynamical Sytems in the Situation Calculus:
Some Representational and Computational Issues
for Automated Reasoning
Raymond Reiter
Department of Computer Science
University of Toronto
For the past several years, the Cognitive Robotics Group at the
University of Toronto has been exploring the feasibility of the
situation calculus as a theoretical and computational foundation
for modeling dynamical systems. It is a challenging research
problem to capture, in a single formal and computational
framework, the full range of characteristics associated with
such settings: the frame, ramification and qualification
problems, exogenous and natural events, chance events and the
unpredictability of action effects, complex actions and
procedures and the ability of an agent to perform such actions,
time, concurrency, hypothetical and counterfactual reasoning
about action occurrences and time, perceptual actions and their
effects on an agent's mental state, the complex relationships
among reasoning, perception and action, planning, belief
revision in the presence of conflicting observations, etc.
The principal objective of this project is to provide just such
a general theory and implementation of actions and time, and, as
already noted, our formal foundation for this has been the
situation calculus.
While we remain far from achieving these long-range objectives,
we have had some modest success in this undertaking. Starting
with a solution to the frame problem for deterministic, simple
actions, we have defined and implemented GOLOG, a novel
situation calculus-based logic programming language for defining
complex system behaviors, and experimented with it in robotics
applications, and for software agents. Recently, GOLOG has been
generalized to CONGOLOG and RGOLOG, concurrent languages for
representing reactive systems, and multiple processes. There is
a situation calculus account of sensing (knowledge-producing)
actions, and this has been extended to include noisy
sensors. The solution to the frame problem for deterministic
primitive actions has been extended to nondeterministic ones. A
situation calculus calculus account has been given of planning
for agents which can sense their environments. Agent goals and
rational actions have been formalized in the situation
calculus. Concurrency, natural actions and continuous time have
all been given situation calculus-based accounts, with GOLOG
implementations. Various situation calculus planners have been
implemented.
Grounded as our approach is in classical logic, all reasoning
and computation rely on first order theorem proving. My talk
will focus on how we have succeeded in building efficient
implementations, and what are the underlying assumptions that
make this possible. For certain applications, for example
robotics, some of these assumptions are unrealistic, and I shall
describe some of the automated reasoning problems which must be
addressed in these settings.
For a preview of some of these themes, and the approach taken by
the University of Toronto Cognitive Robotics Group, see:
http://www.cs.toronto.edu/~cogrobo/