Temporal Logic with Capacity Constraints

Often when formalising dynamic systems, constraints such as exactly “n” of a set of values hold. In this paper, we consider reasoning about propositional linear time temporal logics in the presence of such constraints. First, we provide experimental results from a developed prover for a tableau-like algorithm with constraints, showing the advantages of this method over other tableau provers. However, this involves explicitly evaluating the constraints, an expensive breadth-first search style of construction and the input formula to be in a particular normal form. To avoid this, we provide a sound, complete and terminating tableau algorithm, which does not require formula to be input in a particular normal form, embeds constraints into its construction avoiding their explicit evaluation and enables depthfirst search style expansion.

• Type: Conference
• Year: 2007
• Where: FROCOS
• Authors: Clare Dixon, Michael Fisher, Boris Konev
• Keywords: FROCOS 2007, Particular Normal Form, Search Style, Terminating Tableau Algorithm