Show simple item record

dc.contributor.authorCau, A. (Antonio)
dc.contributor.authorMoszkowski, B. C.
dc.date.accessioned2005-05-23T20:41:26Z
dc.date.available2005-05-23T20:41:26Z
dc.date.created2005-05-12
dc.date.issued2005-05-23T20:41:26Z
dc.identifier.urihttp://hdl.handle.net/2086/8
dc.description.abstractInterval temporal logic (ITL) is a logic that is used to specify and reason about systems. The logic has a powerful proof system but rather than doing proofs by hand, which is tedious and error prone, we want a tool that can check each proof step. Instead of developing a new tool we will use the existing prototype verification system (PVS) as a basic tool. The specification language of PVS is used to encode interval temporal logic semantically and syntactically. With this we can encode the ITL proof system within PVS. Several examples of proofs in ITL that are done per hand are checked with PVS.en
dc.description.sponsorshipFunded by EPSRC Research Grant GR/K25922en
dc.format.extent81097 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoenen
dc.relation.ispartofseriesSTRL internal monographen
dc.subjectinterval temporal logicen
dc.subjecttempura
dc.subject.lcshProof theory
dc.titleUsing PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encodingen
dc.typeTechnical Reporten
dc.researchgroupSoftware Technology Research Laboratory (STRL)


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record