arrow
返回

Temporal logics for real-time system specification

delete2000-03-01
delete73
delete
OA
AI
P
Pierfrancesco Bellini
R
R. Mattolini
P
Paolo Nesi
DOI:10.1145/349194.349197delete
delete原文链接
delete分享
delete收藏
查看原文
摘要

摘要

En 中文
The specification of reactive and real-time systems must be supported by formal, mathematically-founded methods in order to be satisfactory and reliable. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulas, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few years can be used for specifying reactive systems, although not all are suitable for specifying real-time systems. In this paper we present a series of criteria for assessing the capabilities of temporal logics for the specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specifications is identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples.
Keyword:
logic specification languages
metric of time
modal logic
reactive systems
real-time
specification model
temporal constraints
temporal logics
temporal relationships
AI总结

AI总结

对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。

期刊

ACM Computing Surveys 封面图
ACM Computing Surveys
IF:
28
论文数:
2.4K
被引数:
3.5W

机构

暂无机构信息
引用论文

引用论文

Cognitive Profile in Tramadol Addicts
err2018-07-01
err0
errOAAI
errSaber Mahdi; Hameed Baddary; Maha Mobasher; Tarek Ahmed
err分享
err收藏
Plant community patterns in a gypsum area of NE Spain. II. Effects of ion washing on topographic distribution of vegetation
err1999-04-01
err0
PREAI
errJoaquı́n Guerrero-Campo; Francisco Alberto; Melchor Maestro; John Hodgson; Gabriel Montserrat-Martı́
err分享
err收藏
Delayed Afterdepolarization in Intact Canine Sinoatrial Node as a Novel Mechanism for Atrial Arrhythmia
err2010-10-06
err0
errOAAI
errBOYOUNG JOUNG; HONG ZHANG; TETSUJI SHINOHARA; MITSUNORI MARUYAMA; SEONGWOOK HAN; DAEHYEOK KIM; EUE‐KEUN CHOI; YOUNG‐KEUN ON; SHIEN‐FONG LIN; PENG‐SHENG CHEN
err分享
err收藏
Introduction
err1997-01-01
err0
PREAI
errStéphane Hua; Eric Buffetaut
err分享
err收藏
Structure and Membrane Interaction of Myristoylated ARF1
err2009-01-01
err0
errOAAI
errYizhou Liu; Richard A. Kahn; James H. Prestegard
err分享
err收藏
学者 查看更多内容