Real-time logics: Fictitious clock as an abstraction of dense time

Jean Franqois Raskin, Pierre Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

In this paper we study two possible Semantics for the realtime logic MTL (Metric Temporal Logic). In the first semantics, called dense time semantics, time is modeled by the positive real numbers. In the second one, called fictitious clock semantics, real-time information is delivered by a global fictitious clock. We show that the fictitious clock semantics can be viewed as an abstraction of the dense time semantics. This abstraction relation is formalized by a parametric conservative connection. This formalization can be used to partially decide undecidable problems in the dense time semantics by reasoning on the fictitious clock semantics.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 3rd International Workshop, TACAS 1997, Proceedings
PublisherSpringer Verlag
Pages165-182
Number of pages18
ISBN (Print)3540627901, 9783540627906
DOIs
Publication statusPublished - 1 Jan 1997
Event3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997 - Enschede, Netherlands
Duration: 2 Apr 19974 Apr 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1217
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997
Country/TerritoryNetherlands
CityEnschede
Period2/04/974/04/97

Fingerprint

Dive into the research topics of 'Real-time logics: Fictitious clock as an abstraction of dense time'. Together they form a unique fingerprint.

Cite this