Accession Number:

ADA109853

Title:

Synthesis of Communicating Processes from Temporal Logic Specifications,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1981-09-01

Pagination or Media Count:

29.0

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

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software
  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE