On undecidability of propositional temporal logics on trace systems
type: Item
instance of: scholarly article
title: On undecidability of propositional temporal logics on trace systems
zbMATH Open document ID: 0771.03006
DOI: 10.1016/0020-0190(92)90007-I
author: Wojciech Penczek
published in: Information Processing Letters
publication date: 1993-01-16T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 68Q10
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03D35
Mathematics Subject Classification ID: 03B80
Mathematics Subject Classification ID: 12L05
zbMATH DE Number: 94475
zbMATH Keywords: concurrency
zbMATH Keywords: partial order temporal logics
zbMATH Keywords: trace systems
zbMATH Keywords: concurrent action
zbMATH Keywords: satisfiability
zbMATH Keywords: expressive power
reviewed by: Frada Burstein
MaRDI profile type: Publication
cites work: Using branching time temporal logic to synthesize synchronization skeletons
cites work: Recurring Dominoes: Making the Highly Undecidable Highly Understandable
cites work: Q3026978
cites work: Q4733386
cites work: Q4733400
cites work: Concurrent systems and inevitability
cites work: Q4733399
cites work: Synthesis of Communicating Processes from Temporal Logic Specifications
cites work: Q4038718
cites work: Q4268475
cites work: Q4205072
cites work: Q3814798
cites work: Q4733433
Recommended article: Model checking properties on reduced trace systems
Recommended article: Q4353629
Recommended article: Q4281547
Recommended article: Towards automata for branching time and partial order
Recommended article: Step traces
Recommended article: Q3774928
Recommended article: Q4864475
Recommended article: Theory of traces
Recommended article: TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
Recommended article: Q4247293
description: scientific article; zbMATH DE number 94475