A logic for real-time systems specification, its algebraic semantics, and equational calculus

被引：0
|
作者：
Baum, GA [1 ]
Frias, MF
Maibaum, TSE
机构：
[1] Natl Univ La Plata, LIFIA, Dept Informat, La Plata, Buenos Aires, Argentina
[2] Univ Buenos Aires, Dept Comp, RA-1053 Buenos Aires, DF, Argentina
[3] Univ London Imperial Coll Sci Technol & Med, London SW7 2BZ, England
来源：
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY | 1999年 / 1548卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a logic for real time systems specification which is an extension of first order dynamic logic by adding (a) arbitrary atomic actions rather than only assignments, (b) variables over actions which allow to specify systems partially, and (c) explicit time. The logic is algebraized using closure fork algebras and a representation theorem for this class is presented. This allows to define an equational (but infinitary) proof system for the algebraization.
引用
收藏
页码：91 / 105
页数：15
相关论文
共 50 条
12345