Embedding time granularity in a logical specification language for synchronous real-time systems
type: Item
instance of: scholarly article
title: Embedding time granularity in a logical specification language for synchronous real-time systems
zbMATH Open document ID: 0781.68083
DOI: 10.1016/0167-6423(93)90025-K
author: E. Ciapessoni
author: E. Corsetti
author: Angelo Montanari
author: Pierluigi San Pietro
published in: Science of Computer Programming
publication date: 1993-10-17T00:00:00Z
review text: The paper presents a logical language for specifying a wide-ranging class of real-time systems: the systems whose components have dynamic behaviour regulated by very different time constants (granular systems). It confines itself to the treatment of the class of synchronous granular systems, whose components are temporally qualified with respect to the same clock. The proposed specification language is a metric and layered temporal logic (MLTL) extending metric temporal logics with contextual and projection operators to deal with time granularity. MLTL allows the specifier (i) to associate a time granularity with a formula (contextual operator), (ii) to move a formula in the past/future without changing granularity (displacement operator), and (iii) to shift a formula to coarser/finer time granularities (projection operator). The combined use of the three operators makes it possible to build granular system specifications by referring to the `natural' scale in the specification of any component and by properly constraining interactions between components. MLTL is provided with a model-theoretic semantics and a sound axiomatization.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 417471
zbMATH Keywords: granular systems
zbMATH Keywords: real-time systems
zbMATH Keywords: specification language
zbMATH Keywords: metric temporal logics
zbMATH Keywords: specifications
describes a project that uses: LOTOS
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 417471