A Local Presentation of Synchronizing Systems
We study systems of sequential agents which communicate by synchronization, whose behaviours are given by a subclass of event structures. Transition system models for such structures typically require global state information which cannot be obtained by taking products of local transition systems. We offer a presentation whereby the notion of local state is modified, and an appropriate product operation precisely captures this class of behaviours. This is shown using a back-and-forth construction.
KeywordsTransition System Global State Event Occurrence Label Transition System Linear Time Temporal Logic
Unable to display preview. Download preview PDF.
- [BC]Boudol, G. and Castellani, I., “Flow models of distributed computations: event structures and nets”, Rapports de Recherche 1482, IN- RIA, July 1991.Google Scholar
- [KR]Krasucki, P., and Ramanujam, R., “Knowledge and the ordering of events in distributed systems”, TARK V, Theoretical Aspects of Reasoning about Knowledge, 1994, 267–283.Google Scholar
- LPRT] Lodaya, K., Parikh, R., Ramanujam, R. and Thiagarajan, P.S., “A logical study of distributed transition systems”, Report IMSc/92/07 1992, to appear in Information and Computation.Google Scholar
- [Thi]Thiagarajan, P.S., “A trace based extension of propositional linear time temporal logic”, Proc IEEE LICS, 1994, 438–447.Google Scholar
- WN] Winskel, G., and Nielsen, M., “Models for concurrency”, in Handbook of Logic in Computer Science, Eds: Abramsky, Gabbay and Maibaum, Oxford Science Publications.Google Scholar