01: Bericht 91. München, Germany: Ludwig-Maximilians-Universiät, Institut für Informatik, 1991.
Abstract: The author develops a temporal logic with an explicit parallel operator. The usual Kripke-models are extended by a local reachability relation resulting in the so-called state structures with locality (sswl). It is shown that the conflict-free sswl correspond to the state spaces of occurrence nets. Sequential and parallel composition are defined such that the conflict-free sswl can uniquely be decomposed into sequential and parallel components. The author defines linear and branchihng Net Logic (NL) whose language consists essentially of the boolean and the regular operators as well as the parallel operator. The decidability and the structural operator make NL particularly suited for the structured description of concurrent systems.
Keywords: concurrency (as a) modality; temporal logic; parallel operator; extended Kripke-model; local reachability relation; state structure (with) locality; conflict-free; state space (of) occurrence net(s); sequential composition; parallel composition; decomposition; linear (and) branchihng net logic; decidability.