|
We identify a network of sequential processes that communicate by
synchronizing frequently on common actions. More precisely, we demand
that there is a bound k such that if the process p executes k steps
without hearing from process q---directly or indirectly---then it will
never hear from q again. The non-interleaved branching time behavior
of a system of connectedly communicating processes (CCP) is given by
its event structure unfolding. We show that the monadic second order
(MSO) theory of the event structure unfolding of every CCP is
decidable. Using this result, we also show that an associated
distributed controller synthesis problem is decidable for linear time
specifications that do not discriminate between two different
linearizations of the same partially ordered execution.
[.pdf]
|