A logical study of distributed transition systems

Lodaya, K. ; Parikh, R. ; Ramanujam, R. ; Thiagarajan, P. S. (1995) A logical study of distributed transition systems Information and Computation, 119 (1). pp. 91-118. ISSN 0890-5401

PDF - Author Version

Official URL: http://www.sciencedirect.com/science/article/pii/S...

Related URL: http://dx.doi.org/10.1006/inco.1995.1078


We extend labelled transition systems to distributed transition systems by labelling the transition relation with a finite set of actions, representing the fact that the actions occur as a concurrent step. We design an addition-based temporal logic in which one can explicity talk about steps. The logic is studied to establish a variety of positive and negative results in terms of axiomatizability and decidability. Our positive results show that the step notion is amenable to logical treatment via standard techniques. They also help us to obtain a logical characterization of two well known models for distributed systems: labelled elementary net systems and labelled prime event structures. Our negative results show that demanding deterministic structures when dealing with a "non-interleaved" notion of transitions is, from a logical standpoint, very expressive. They also show that another well known model of distributed systems called asynchronous transition systems exhibits a surprising amount of expressive power in a natural logical setting.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
ID Code:50502
Deposited On:25 Jul 2011 11:44
Last Modified:18 May 2016 04:46

Repository Staff Only: item control page