Details

Autor(en) / Beteiligte

• Alexander, A.
• Reisig, W.

Titel

Logic of involved variables - system specification with temporal logic of distributed actions

Ist Teil von

• Third International Conference on Application of Concurrency to System Design, 2003. Proceedings, 2003, p.167-176

Ort / Verlag

IEEE

Erscheinungsjahr

2003

Quelle

IEEE Electronic Library Online

Beschreibungen/Notizen

• 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.