Reasoning about Nondeterministic and Concurrent Actions: A Process Algebra Approach

In this paper, we study reasoning about actions fol-lowing a model checlcing approach in contrast to the usual validity checlcing 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 asso-ciated with an explicit global store. To reason about system properties we introduce an extension of modal p-calculus. This setting, although directly applica-ble 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, coor-dinations among agents. On the other hand, reasoning by model checking is typically much easier than more general logical services such as validity checking