MODAL LOGIC OF CONCURRENT NONDETERMINISTIC PROGRAMS.

A description is given of a logic, L, for reasoning about concurrent programs. Programs are similar to those of dynamic logic, with a shuffle operator included. L is a modal logic. The modalities included are extended by constraints, so that they can be used to express assertions such as ″p holds as long as q does.″ Programs contain labels. Using labels, it is possible to isolate the behavior of a single process or segment of a process, while at the same time keeping the segment in the context of the whole parallel system. A certain subset of the propositional case of L is known to be decidable.