Temporal Logic with Capacity Constraints

9 years 13 days ago
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.
Clare Dixon, Michael Fisher, Boris Konev
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Authors Clare Dixon, Michael Fisher, Boris Konev
Comments (0)