Verification of Temporal Properties
dc.contributor.author | Fix, Limor | en_US |
dc.contributor.author | Grumberg, Orna | en_US |
dc.date.accessioned | 2007-04-23T16:31:11Z | |
dc.date.available | 2007-04-23T16:31:11Z | |
dc.date.issued | 1993-08 | en_US |
dc.description.abstract | The paper presents a relatively complete deductive system for proving branching time temporal properties of reactive programs. No deductive system for verifying branching time temporal properties has been presented before. Our deductive system enjoys the following advantages. First, given a well-formed specification there is no need to translate it into a normal-form specification since the system can handle any well-formed specification. Second, given a specification to be verified, the proof rule to be applied is easily determined according to the top level operator of the specification. Third, the system reduces temporal verification to assertional reasoning rather than to temporal reasoning. | en_US |
dc.format.extent | 1916538 bytes | |
dc.format.extent | 436218 bytes | |
dc.format.mimetype | application/pdf | |
dc.format.mimetype | application/postscript | |
dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR93-1368 | en_US |
dc.identifier.uri | https://hdl.handle.net/1813/6142 | |
dc.language.iso | en_US | en_US |
dc.publisher | Cornell University | en_US |
dc.subject | computer science | en_US |
dc.subject | technical report | en_US |
dc.title | Verification of Temporal Properties | en_US |
dc.type | technical report | en_US |