THE INFOLOG LINEAR TENSE PROPOSITIONAL LOGIC OF EVENTS AND TRANSACTIONS

被引:13
作者
FIADEIRO, J
SERNADAS, A
机构
[1] Escola Politecnica de Lisboa, Lisbon, Port, Escola Politecnica de Lisboa, Lisbon, Port
关键词
COMPUTER METATHEORY - Formal Logic;
D O I
10.1016/0306-4379(86)90023-2
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
An extended linear tense propositional logic is presented for the specification and verification of the behavior of very dynamic information systems. The temporal evolution of a system is described with causal rules specifying trigger/reaction relationships between events. Besides the presentation of the language, semantics and axiomatization of the proposed triggering logic, a practical proof system is outlined which provides effective tools for proving several properties of a system using semaphores. The relationship between the event structure and the tense structure of the logic is also discussed. The proposed logic is an important fragment of the INFOLOG calculus that is being developed for information systems design.
引用
收藏
页码:61 / 85
页数:25
相关论文
共 42 条
  • [1] BARRINGER H, 1984, 16TH P ACM S THEOR C
  • [2] CARMO J, 1985, INFORMATION SYSTEMS
  • [3] Casanova M. A., 1980, ACM Transactions on Programming Languages and Systems, V2, P386, DOI 10.1145/357103.357111
  • [4] CASTILHO J, 1982, 8TH P VLDB C MEX CIT, P93
  • [5] COELHO H, 1985, DECIS SUPPORT SYST, V1, P143
  • [6] Cresswell M., 1968, INTRO MODAL LOGIC
  • [7] DIJKSTRA E, 1968, PROGRAMMING LANGUAGE
  • [8] Dreben B., 1979, DECISION PROBLEM SOL
  • [9] FIADEIRO J, 1985, SPECIFICATION VERIFI
  • [10] GOLSHANI F, 1983, 9TH P INT C VER LARG, P331