| Communicating Agents For Concurrent Temporal Tableaux (2007) | |||||||||||||||
Abstract | |||||||||||||||
| . We consider the analysis and deconstruction of a tableau proof method for propositional temporal logic (PTL) in order that it may be reformulated as an agent-based design. Our motivation for its deconstruction is the identification of potential parallelism in the algorithm. Subsequently we describe a system that has been designed by deconstructing a tableau proof algorithm for PTL, and reconstructing it through the specification of the functionality and relationships between a collection of concurrently cooperating heterogeneous agents. 1 Introduction Temporal logics enable us to reason about the elements of a domain that may change over time. We shall consider here a propositional temporal logic that is linear and discrete (point-based) and enables us to make inferences about present and future-tense features of the modelled domain. The tableau method for PTL [5] seeks to convert all future-tense statements into statements about things that are true in the current temporal state, a... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||