DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Decidability and Expressiveness of Logics of Processes.
WASHINGTON UNIV SEATTLE DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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
APPROVED FOR PUBLIC RELEASE