| Communicating Agents For Concurrent Temporal Tableaux (2008) | |||||||||||||||
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. As a result we may use this approach to deconstruct a proof algorithm, 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 and enables us to make inferences about present and futuretense features of the modelled domain. A detailed appraisal may be found in [1]. The tableau method for PTL [6] seeks to convert all future-tense statements into statements about things that are true in the current temporal state, and things that m... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||