Output details
11 - Computer Science and Informatics
University of Westminster
Handling periodic properties: deductive verification for quantified temporal logic specifications
<10> Originality: Periodic properties are important in many areas, in particular in software integration. One of them, that “event or process occurs at every even moment of a computation”, is a famous milestone in mathematical modelling of reliable integration. Quantified propositional temporal logic can express this property but it lacked an efficient deductive based verification method – the problem which is solved in this paper.
Significance: The paper introduces natural deduction based proof technique for the above formalism thus opening prospects for the efficient implementation.
Rigour: Mathematical proofs of the soundness and completeness of the proposed method are established.