Is There a Future for Deductive Temporal Verification?

In this paper, we consider a tractable sub-class of propositional linear time temporal logic, and provide a complete clausal resolution calculus for it. The fragment is important as it can be used to represent simple Buchi automata. We also show that, just as the emptiness check for a Buchi automaton is tractable, the complexity of deciding unsatisfiability, via resolution, of our logic is polynomial (rather than exponential). Consequently, a Buchi automaton can be represented within our logic, and its emptiness can be tractably decided via deductive methods. This may have a significant impact upon approaches to verification, since techniques such as model checking inherently depend on the ability to check emptiness of an appropriate Buchi automaton. Thus, we also discuss how such a logic might form the basis for practical deductive temporal verification

Authors

• Clare Dixon
• Michael Fisher 0001
• Boris Konev

Keywords

• Automata
• Logic
• Calculus
• Computer science
• Polynomials
• Emptiness
• Model Checking
• Temporal Logic
• Deductive Methods
• Propositional Logic
• Moment In Time
• Complex Procedures
• Normal Form
• Sequence Of States
• Inference Rules
• Disjoint Sets
• Loop Iteration
• State Index
• Complex Search
• Set Of Propositions
• XOR Operation
• Classical Logic
• Unit Resolution
• Step Resolution
• fragments of PTL
• deductive verification
• complexity
• clausal temporal resolution.