| Abstract |
|---|
| Temporal logic is useful for reasoning about time-varying properties. To achieve this it is important to validate temporal logic specifications. Proof methods for propositional temporal logic are PSPACE complete and thus automated tableau-based theorem provers are both computationally and resource intensive. Here we analyse a standard temporal tableau method using parallelism in attempt to both reduce the amount of storage needed and improve efficiency. Two shared memory parallel systems are presented which are based on this decomposition of the algorithm but differ in the configuration of parallel processes. |
| Contact |
| John Keane Department of Computation,,UMIST,,PO Box 88,,Sackville Street,,Manchester,,M20 1QD,,UK jak@co.umist.ac.uk |