The INFOLOG linear tense propositional logic of events and transactions

TY - JOUR

T1 - The INFOLOG linear tense propositional logic of events and transactions

AU - Fiadeiro, José

AU - Sernadas, Amílcar

N1 - Copyright 2008 Elsevier B.V., All rights reserved.

PY - 1986/1/1

Y1 - 1986/1/1

N2 - 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 both safety and liveness properties of the specified systems. Its usefulness is illustrated by 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.

AB - 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 both safety and liveness properties of the specified systems. Its usefulness is illustrated by 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.

U2 - 10.1016/0306-4379(86)90023-2

DO - 10.1016/0306-4379(86)90023-2

M3 - Article

SN - 0306-4379

VL - 11

SP - 61

EP - 85

JO - Information Systems

JF - Information Systems

IS - 1

ER -