On undecidability of propositional temporal logics on trace systems (Q1199555)

The paper investigates application of the partial order temporal logics on trace systems for concurrent action description. The concepts of traces and trace systems are introduced according to \textit{A. Mazurkiewicz}'s definition [Lect. Notes Comput. Sci. 354, 285-363 (1989; Zbl 0683.68032)]. An example of a trace system is provided. The paper shows how to model temporal logic with a trace system, Partial Order Logic (POL) and Interleaving Set Temporal Logic (ISTL) on trace systems are defined. Corresponding syntax and semantics are considered, and compared with Computational Tree Logic (CTL). The notions are illustrated by relevant examples. The problem of determining the satisfiability of POL and ISTL formulas is studied. The negative result is reported. It is shown that if two actions are specified concurrent according to the propositional versions of Partial Order Logic (POL), Interleaving Set Temporal Logic (ISTL), or Concurrent Computational Tree Logic (CCTL) in case of application of these logics to the trace systems, then they are undecidable. From this result the conclusion is made that these logics cannot be used for automated synthesis of concurrent programs along the standard lines. However, considering significant expressive power of trace systems for concurrent process description, it is stated to be worthwhile to redefine conditions on a logic to make it decidable.