Labelled Tableaux for Temporal Logic with Cardinality Constraints

Dixon, C., Konev, B., Schmidt, R. A. and Tishkovsky, D. (2012)

Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). IEEE Computer Society, 111-118. BiBTeX, DOI, PDF.

Frequently when formalising systems that change over time, we must represent statements, coming from physical constraints or representational issues, stating that exactly n literals (or less than n literals) of a set hold. While we can write temporal formulae to represent this information, such formulae both complicate and increase the size of the specification and adversely affect the performance of provers. In this paper, we consider reasoning about problems specified in propositional linear time temporal logics in the presence of such constraints on literals. We present a sound, complete and terminating tableau calculus which embeds constraints into its construction avoiding their explicit evaluation. We use MetTeL, an automated tableau prover generator, to provide an implementation of the calculus and give experimental results using the prover.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 20 May 13
Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk