Using PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encoding

Date
2005-05-23T20:41:26Z
Authors
Cau, A. (Antonio)
Moszkowski, B. C.
Journal Title
Journal ISSN
ISSN
DOI
Volume Title
Publisher
Peer reviewed
Abstract
Interval 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.
Description
Keywords
interval temporal logic, tempura
Citation
Research Institute