A state-oriented, partial-order model and modal logic for concurrent systems verification
Dr. Vasumathi K Narayanan
Given an input set of n communicating finite state machines (CFSms), instead of composing them into a traditional product machine or its reduced graph versions, it is shown that a set of n unfoldings of the CFSms can be built with a minimal set of global state vectors stored statically and the rest genereted dynamically as needed for verification. Named a sum machine, its state-oriented, partial-order model represents sequentiality, conflict and concurrency all at the same computational layer as opposed to event-based semantics. Conflict relation in event paradigm has to be dealt with separately since concurrency and causality are complementary and comprise the flow relation completely thus leaving out choice/conflict. In sum machine semantics, concurrency and causality have a non-null intersection, a result used to represent conflict along with sequence and concurrency and applied in an efficient model-checker algorithm.
Configurations of sum machine are equivalent to partial runs of product machine. By defining local and general configurations and showing that the latter can be derived as a set union of the former, we essentially generate reachable global-state vectors by exploring only the local states of sum machine. A third-order modal logic is defined over sum machine model with its branching-time and branching-space features to build an efficient model-checker.
Keywords: Concurrent systems, state-oriented semantics, event-based semantics, product machine, reduced state graphs, CFsms, sum machine, causality, sequentiality, conflict, simultaniety, concurrency, configurations, runs, interleavings, monadic third-order temporal logic, branching-time, branching-space, model-checking.