Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions

Third International Conference on Application of Concurrency to System Design (ACSD'03) p. 167
Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions
Adrianna Alexander, Humboldt-Universität zu Berlin
Wolfgang Reisig, Humboldt-Universität zu Berlin

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSD.2003.1207711
Send link to a friend

Abstract
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.
Back to Top Additional Information
Citation: Adrianna Alexander, Wolfgang Reisig, "Logic of Involved Variables — System Specification with Temporal Logic of Distributed Actions," acsd, p. 167, Third International Conference on Application of Concurrency to System Design (ACSD'03), 2003

	Advanced Search
CS Search Google Search