Articles written in Sadhana
Volume 17 Issue 1 March 1992 pp 131-165
A distributed computer system consists of different processes or
In this paper, we first discuss formal models of distributed systems in which concurrency is specified
In the second half of the paper, we develop a family of logics to specify and reason about the behavioural properties of the models we have described. The logics we define are extensions of temporal logic with new modalities to directly describe concurrency.
This paper is essentially a survey of work done by the authors during the last few years on modelling distributed systems with true concurrency and using logic to reason about these models. The emphasis is on motivating definitions through examples and on presenting major results, without going into too many formal details. We provide pointers to the literature where these details can be found.