Third International Conference on Application of Concurrency to System Design (ACSD'03)
Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions
Guimar?es, Portugal
June 18-June 20
ISBN: 0-7695-1887-7
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.
Citation:
Adrianna Alexander, Wolfgang Reisig, "Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions," acsd, pp.167, Third International Conference on Application of Concurrency to System Design (ACSD'03), 2003