Abstract

A theory of state-oriented, partially-ordered model named, Communicating Minimal prefix machines (CMpms) that represent a fixed set of processes, is presented. Each of these Mpms is a possibly infinite, State Transition System . Communication among a set of Mpms is by synchronization. Enriched by a global, causal dependency relation among the Mpm-states that is partial , the disjoint union of CMpms comprise a sum machine . It is shown that the set of all global states of the product machine of CMpms is obtainable dynamically from the local Mpm-states of the sum machine using the monotonicity property, linking the product machine's global states and the sum machine's local ones. In this sense, the product-machine is generated virtually , simulated by the sum-machine. More interestingly, it is shown that from every given set of Communicating Finite state machines (CFsms), a truncated (finite) version of a set of CMpms and so a sum machine can be generated in a recursive functional manner. The set of global states of the product machine of CMpms surjectively map onto that of CFsms. Consequently, it is possible to generate all the global states of the latter using the local states of the sum machine composed by a corresponding set of CMpms. The sum machine models true causality and hence true sequence, true concurrency and true choice among local states, as exhibited by the original input CFsms specification without enumerating all the runs of the system nor all the nondeterministic interleavings of each run as opposed to the product machine . A Spatial, temporal logic or space-time logic named CML (Computational Mpms Logic), is proposed that combines the conventional branching time feature with what is proposed as branching space feature: the latter corresponds to concurrency just as the former to conflicts , as exhibited by the input specification. CML therefore introduces operators to reason about properties of interleavings within each run, orthogonal to the branching time operators, to reason about runs . The logic turns out to be more expressive than the ones in vogue for specifying properties of concurrent systems. In addition, CML coupled with the sum machine model, enables the implementation of a deterministic model checker algorithm to verify the properties of a given CFsm system that is free of exponential complexity caused by the enumeration of runs as well as that of all interleavings within each run.