Reasoning about nondeterministic and concurrent actions: A process algebraapproach

We present a framework for reasoning about processes (complex actions) that are constituted by several concurrent activities performed by various inte racting agents, The framework is based on two distinct formalisms: a repres entation formalism, which is a CCS-like process algebra associated with an explicit global store; and a reasoning formalism, which is an extension of modal mu-calculus, a powerful logic of programs that subsumes dynamic logic s such as PDL and Delta PDL, and branching temporal logics such as CTL and CTL*. The reasoning service of interest in this setting is model checking i n contrast to logical implication. This framework, although directly applic able only when complete information on the system behavior is available, ha s several interesting features for reasoning about actions in Artificial In telligence. Indeed, it inherits formal and practical tools from the area of Concurrency in Computer Science, to deal with complex actions, treating su itably aspects like nonterminating executions, parallelism communications, and interruptions. (C) 1999 Published by Elsevier Science B.V. All rights r eserved.