Third International Conference on Application of Concurrency to System Design, 2003. Proceedings. (2003)
June 18, 2003 to June 20, 2003
Adrianna Alexander , Humboldt-Universit?t zu Berlin
Wolfgang Reisig , Humboldt-Universit?t zu Berlin
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.
W. Reisig and A. Alexander, "Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions," Third International Conference on Application of Concurrency to System Design, 2003. Proceedings.(ACSD), Guimar?es, Portugal, 2003, pp. 167.