<%@ page language="java" contentType="text/html" %>
<%-- Include common initialisation code --%>
<%@ include file="/arch/common.jsp" %>
<%-- The current tab --%>
<% String currentTab = "Research"; %>
<%-- Content of navigation pane --%>
<%@ include file="nav.jsp" %>
<% showCurrentLink=true; %>
<%-- Current navigation location --%>
<% String currentNav = "Reports and Theses"; %>
<%-- Include the code for the document header --%>
<%@ include file="/arch/header.jsp" %>
Research Report CS-RR-317
<%-- Include the code for the lines and navigation --%>
<%@ include file="/arch/middle.jsp" %>
M. Wahab,
The Semantics of TLA on the PVS Theorem Prover
(October 1, 1996).
Abstract
An implementation of Lamport's Temporal Logic of Actions (TLA) on
a higher order logic theorem prover is described. TLA is a temporal
logic, for which a syntax and semantics are defined, based on an action
logic which is represented by higher order functions. The temporal logic
includes quantifiers for variables with constant values and for variables
whose values change over time. The semantics of the latter depend on an
auxiliary function which cannot be defined by primitive recursion and
an alternative is given based on the Hilbert e operator.
Download
cs-rr-317.ps.gz
<%-- Include the code for the document footer --%>
<%@ include file="/arch/footer.jsp" %>