Embedding time granularity in a logical specification language for synchronous real-time systems

DOI10.1016/0167-6423(93)90025-KMaRDI QIDQ685609zbMATH OpenFDO

Authors E. Ciapessoni, E. Corsetti, Angelo Montanari, Pierluigi San Pietro

Publication date 17 October 1993

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(93)90025-K

zbMATH Keywords

granular systemsmetric temporal logicsreal-time systemsspecification languagespecifications

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Logical specification of reactive and real-time systems
• scientific article; zbMATH DE number 4128370
• A really temporal logic
• A survey on temporal logics for specifying and verifying real-time systems
• Branching within time: An expressively complete and elementarily decidable temporal logic for time granularity

Cited in

(6)

• Two-sorted metric temporal logics
• Decidability results for metric and layered temporal logics
• Modelling temporal behaviour in complex systems with Timebands
• Completeness results for two-sorted metric temporal logics
• scientific article; zbMATH DE number 5044784 (Why is no real title available?)
• A timeband framework for modelling real-time systems

Describes a project that uses

Uses Software

• LOTOS

This page was built for publication: Embedding time granularity in a logical specification language for synchronous real-time systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685609)