Symmetric Temporal Theorem Proving

In this paper we consider the deductive verification of propositional temporal logic specifications of symmetric systems. In particular, we provide a heuristic approach to the scalability problems associated with analysing properties of large numbers of processes. Essentially, we use a temporal resolution procedure to verify properties of a system with few processes and then generalise the outcome in order to reduce the verification complexity of the same system with much larger numbers of processes. This provides a practical route to deductive verification for many systems comprising identical processes.

Authors

• Amir Niknafs-Kermani
• Boris Konev
• Michael Fisher 0001

Keywords

• Protocols
• Cognition
• Complexity theory
• Computer science
• Educational institutions
• Electronic mail
• Scalability
• Essential Step
• Properties Of Systems
• Identification Process
• Temporal Specificity
• Temporal Logic
• Propositional Logic
• Parametrized
• Resolution Methods
• Problem Instances
• Model Checking
• Set Of Formulas
• automated reasoning
• parameterised systems