Reasoning about nondeterministic and concurrent actions: A process algebra approach

摘要

We present a framework for reasoning about processes (complex actions) that are constituted by several concurrent activities performed by various interacting agents. The framework is based on two distinct formalisms: a representation formalism, which is a CCS-like process algebra associated with an explicit global store, and a reasoning formalism, which is an extension of modal mucalculus, a powerful logic of programs that subsumes dynamic logics such as PDL and ΔPDL, and branching temporal logics such as CTL and CTL∗. The reasoning service of interest in this setting is model checking in contrast to logical implication. This framework, although directly applicable only when complete information on the system behavior is available, has several interesting features for reasoning about actions in Artificial Intelligence. Indeed, it inherits formal and practical tools from the area of Concurrency in Computer Science, to deal with complex actions, treating suitably aspects like nonterminating executions, parallelism, communications, and interruptions.