Process semantics of temporal logic specification

L. Fiadeiro, J. F. Costa, A. Sernadas, T. S.E. Maibaum

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

A process semantics for temporal logic specification is provided by relating a category of temporal theories and interpretations between theories where specification configuration and interconnection is achieved via colimits of diagrams, and a category of algebraic models of processes where parallel composition is explained in terms of limits of diagrams. This semantics is proved to be exact in the sense that given a diagram in the categories of theories and a model of it as a diagram in the category of processes, the limit of the process diagram is a model of the colimit of the theory diagram. In fact, any denotation of a system of interconnected specifications corresponds to a configuration of their denotations as a system of interconnected processes.

Original languageEnglish
Title of host publicationRecent Trends in Data Type Specification
Subtitle of host publication8th Workshop on Specification of Abstract Data Types joint with the 3rd COMPASS Workshop
EditorsMichel Bidoit, Christine Choppy
Place of PublicationBerlin
PublisherSpringer Verlag
Pages236-253
Number of pages18
ISBN (Electronic)9783540475453
ISBN (Print)9783540563792
DOIs
Publication statusPublished - 1993
Event8th Workshop on Specification of Abstract Data Types was held joint with the 3rd COMPASS Workshop, 1991 - Dourdan, France
Duration: 26 Aug 199130 Aug 1991

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume655
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th Workshop on Specification of Abstract Data Types was held joint with the 3rd COMPASS Workshop, 1991
Country/TerritoryFrance
CityDourdan
Period26/08/9130/08/91

Keywords

  • Temporal Logic
  • State Component
  • Algebraic Model
  • Parallel Composition
  • Kripke Structure

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Process semantics of temporal logic specification'. Together they form a unique fingerprint.

Cite this