Embedding time granularity in a logical specification language for synchronous real-time systems (Q685609): Difference between revisions
From MaRDI portal
Created a new Item |
Set profile property. |
||
(4 intermediate revisions by 3 users not shown) | |||
Property / author | |||
Property / author: Pierluigi San Pietro / rank | |||
Property / author | |||
Property / author: Pierluigi San Pietro / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: LOTOS / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 01:58, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Embedding time granularity in a logical specification language for synchronous real-time systems |
scientific article |
Statements
Embedding time granularity in a logical specification language for synchronous real-time systems (English)
0 references
17 October 1993
0 references
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.
0 references
granular systems
0 references
real-time systems
0 references
specification language
0 references
metric temporal logics
0 references
specifications
0 references