eCommons

 

Verification of Temporal Properties

dc.contributor.authorFix, Limoren_US
dc.contributor.authorGrumberg, Ornaen_US
dc.date.accessioned2007-04-23T16:31:11Z
dc.date.available2007-04-23T16:31:11Z
dc.date.issued1993-08en_US
dc.description.abstractThe 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.extent1916538 bytes
dc.format.extent436218 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR93-1368en_US
dc.identifier.urihttps://hdl.handle.net/1813/6142
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleVerification of Temporal Propertiesen_US
dc.typetechnical reporten_US

Files

Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
93-1368.pdf
Size:
1.83 MB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
93-1368.ps
Size:
425.99 KB
Format:
Postscript Files