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

Date

2005-05-23T20:41:26Z

Advisors

Journal Title

Journal ISSN

ISSN

DOI

Volume Title

Publisher

Type

Technical Report

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

Rights

Research Institute