A blackboard approach to parallel temporal tableaux
Robert Johnson · 1995
Before we can contemplate specifying, verifying and animating reactive systems using temporal logics the computational effectiveness of the reasoning process must be vastly improved. While parallel processing will not decrease the total amount of processing required to solve a problem, (in fact it usually increases it) it has the potential to solve the problem faster than sequential systems by distributing the load for for concurrent computation. We illustrate a mechanism by which we are able to harness the available potential of the tableau method for temporal logic, and give an account of an implementation that will permit us to selectively tailor the amount of parallelism for a particular physical architecture. Our approach builds a single, regulated, shared data structure with many concurrent processes acting on it. 1. Introduction In order to port an existing algorithm to a parallel architecture a number of points must be addressed. Firstly, maximal parallelism must be identifie...