Synthesis of Communicating Processes from Temporal Logic Specifications,

Abstract

In this paper, we apply Propositional Temporal Logic (PTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give a PTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL. This model can then be interpreted as a program. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1981
Accession Number
ADA109853

Entities

People

  • Pierre Wolper
  • Zohar Manna

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Computations
  • Computer Science
  • Computers
  • Construction
  • Decomposition
  • Digital Circuits
  • Elimination
  • Identities
  • Language
  • Military Research
  • Network Protocols
  • Reasoning
  • Scientific Research
  • Sequences
  • Specifications

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Linguistics
  • Data Mining and Knowledge Discovery.