Decidability and Expressiveness of Logics of Processes

摘要

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 Parikh's 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+, Parikh's SOAPL, Pneuli's tense logic or Nishimura's process logic, and contains both Lamport's 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 Parikh's sense. In contrast, our method for deciding MPL in general requires processes which are not tree-like. (Author)