On TLA as a Logic
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
On TLA as a Logic
|
| Id. |
41559098 |
| Idioma |
inglés
|
| Titulo |
On TLA as a Logic |
| Localización |
http://citeseer.ist.psu.edu/125001.html
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
this paper we describe TLA from a logical perspective; our
description of TLA has three aspects:
1. As a logic, TLA has a precise syntax and semantics. We define these in
the next section. Our intent is not to develop a new TLA, but rather to
explain and to refine Lamport's definition of TLA [19].
2. Like HOL [13] and other logics, TLA can serve for representing reactive
systems in several styles. In particular, a specification may describe
concurrent steps as interleaved or simultaneous; communication between
components may be synchronous or asynchronous. We discuss a few styles
in section 3.
3. Proofs in TLA rely on basic rules of temporal logic, rules for refinement,
and rules for composition. We state the principal rules in sections 4 and 5.
Following [7, 8], we show that some of them arise from general logical (or
algebraic) considerations, largely independent of the details of TLA
This paper is a self-contained presentation of TLA. It is however not
a survey, in that it includes technical novelties and in that it is far from
comprehensive.
Lamport's original work on TLA [19] provides much additional, useful
material, and in particular some motivation for the TLA approach and a proof
system for TLA. Other papers discuss mechanical verification in TLA [11, 16],
refinement and composition [6, 4], real-time systems and hybrid systems [5,
18, 12], and medium-size examples [20]. There are also works on PTLA [1, 29],
a propositional logic based on a preliminary version of TLA. Finally, the logic
TLR has many similarities with TLA [28].
2 Mart'in Abadi and Stephan Merz
2 A Definition of TLA
|
| Tipo |
ps
|
| Palabras clave |
On TLA as a Logic
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
unrestricted |
| Formatos |
ps
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www.research.digital.com/SRC/personal/Martin_Abadi/Papers/markt.ps
[References] oai:CiteSeerPSU:315693
[References] oai:CiteSeerPSU:386841
[References] oai:CiteSeerPSU:663189
[References] oai:CiteSeerPSU:69399
[References] oai:CiteSeerPSU:388341
[References] oai:CiteSeerPSU:391966
[References] oai:CiteSeerPSU:187100
|
| Fecha de contribución |
31-mar-2009 |
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
