Accession Number:

ADA090688

Title:

Decidability and Expressiveness of Logics of Processes.

Descriptive Note:

Doctoral thesis,

Corporate Author:

WASHINGTON UNIV SEATTLE DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Abrahamson,Karl Raymond

Report Date:

1980-08-01

Pagination or Media Count:

178.0

Abstract:

We define and study several logics of processes. The logics GPL and MPL are based on a second order tense logic, where the two types of variable range over computation sequences and points on computation sequences. GPL is a version of the predicate calculus, similar to Parikhs general logic. MPL is a modal logic, and is the only modal process logic we know of which incorporates two fundamentally different types of modality. When syntactic programs are included in MPL, MPL is at least expressive as PDL, Parikhs SOAPL, Pneulis tense logic or Nishimuras process logic, and contains both Lamports linear and branching time logics. We present a tableau method for deciding validity in MPL, based on a new type of directed graph, called an LL-graph. From the tableau method we derive a complete proof system for MPL. Although GPL and MPL are based on the same notions, we find some interesting differences between the two. MPL is decidable in double exponential time, while even a proper subset of GPL, which can express the same properties as MPL, is nonelementary. We are able to show that GPL is decidable only when processes are tree-like, in Parikhs sense. In contrast, our method for deciding MPL in general requires processes which are not tree-like. Author

Descriptors:

• *DECISION MAKING
• *MATHEMATICAL LOGIC
• *AUTOMATA
• ALGORITHMS
• COMPUTER PROGRAMMING
• SEMANTICS
• THESES
• ROUTING
• CALCULUS
• BOOLEAN ALGEBRA
• THEOREMS

Subject Categories:

• Theoretical Mathematics
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE