Improving temporal logic tableaux using integer constraints

Abstract

It is fairly easy, if somewhat tedious, to prove that our rules preserve satisfiability. Completeness, however, is a much tougher question, and the proof is quite involved. This is one of the reasons why the present note is merely a position paper. The other reason is that so far we did not show that the idea of incorporating linear constraints into temporal logic tableaux is in some sense a real improvement over the current state of the art. On the other hand, we would like to point out at least a few advantages that might be gained from it:

• Better performance if compared to conventional temporal tableaux. Admittedly, this is not obvious from the present appearance of the rules, but there is ample room for optimisation, for example, in the synchronisation rules.

• Implementing real-time logics like the ones suggested in [1].

• Extend the use of linear constraints to a translation of temporal logic satisfiability into integer programming (as it has been done in [6] for many-valued logic). This would allow easy amalgamation with other non-standard features like multiple truth values (needed, for instance, for hardware verification at the switch level [8]) or non-monotonicity [2] in a homogenous framework.

• Perspective of a constraint-based approach to non-classical deduction if integrated with ideas from [4].

• Lifting to restricted first-order versions.