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