Accession Number : ADA328579
Title : Completing the Temporal Picture,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Manna, Zohar ; Pnueli, Amir
PDF Url : ADA328579
Report Date : DEC 1989
Pagination or Media Count : 31
Abstract : The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves on previous temporal systems, such as (MP83a) and (MP83b), in that it reduces the validity of program properties into pure assertional reasoning, not involving additional temporal reasoning. The proof system is based on the classification of temporal properties according to the Borel hierarchy, providing an appropriate proof rule for each of the main classes, such as safety, response, and progress properties.
Descriptors : *COMPUTER LOGIC, *COMPUTER PROGRAM VERIFICATION, ALGORITHMS, SOFTWARE ENGINEERING, COMPUTATIONS, MATHEMATICAL LOGIC, HIERARCHIES, FIELDS(COMPUTER PROGRAMS), STRUCTURED PROGRAMMING.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE