Reasoning about Nondeterministic and Concurrent Actions: A Process Algebra Approach

No. 1: Agents, AI in Art and Entertainment, Knowledge Representation, and Learning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 13

Nonmonotonic Reasoning

In this paper, we study reasoning about actions following a model checking approach in contrast to the usual validity checking one. Specifically, we model a dynamic system as a transition graph which represents all the possible system evolutions in terms of state changes caused by actions. Such a transition graph is defined by means of a suitable process algebra associated with an explicit global store. To reason about system properties we introduce an extension of modal m-calculus. This setting, although directly applicable only when complete information on the system is available, has several interesting features for reasoning about actions. On one hand, it inherits from the vast literature on process algebras tools for dealing with complex systems, treating suitably important aspects like parallelism, communications, interruptions, coordinations among agents. On the other hand, reasoning by model checking is typically much easier than more general logical services such as validity checking.