Modeling a solution for a control problem in distributed systems by restrictions

Abstract

For an independent representation of the constraints on processes in distributed system parts the formalism of Loosely Coupled Systems is introduced. The event structure is derived only from prespecified restrictions of behaviour, concurrency of events is described in elementary and local terms. Formal construction methods (constraint module and slack phase techniques) are defined and used to model a solution for a control problem under various constraints (fairness). The correctness of the solution is proved using a general and new formal procedure: A restricted case graph is evaluated which is minimal with respect to the needed information. For the sake of evaluation the system is reduced to another one by a simple and efficient algorithm. It is proved that the wanted restricted case graph is an invariant under the algorithm. In the reduced system the restricted case graph is very simple to compute.