| 1. |
- Prasad, K V S, 1952
(författare)
-
A Calculus of Broadcasting Systems
- 1991
-
Ingår i: Samson Abramsky, T. S. E. Maibaum (Eds.): TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91). Springer 1991 Lecture Notes in Computer Science. - 3540539824 ; , s. 338-358
-
Konferensbidrag (refereegranskat)abstract
- CBS is a simple and natural CCS-like calculus where processes speak one at a time and are heard instantaneously by all others. Speech is autonomous, contention between speakers being resolved nondeterministically,but hearing only happens when someone else speaks.Observationally meaningful laws dier from those of CCS. The changefrom handshake communication in CCS to broadcast in CBS permits severaladvances. (1) Priority, which attaches only to autonomous actions,is simply added to CBS in contrast to CCS, where such actions are theresult of communication. (2) A CBS simulator runs a process by returninga list of values it broadcasts. This permits a powerful combination,CBS with the host language. It yields several elegant algorithms. Onlyprocesses with a unique response to each input are needed in practice, soweak bisimulation is a congruence. (3) CBS subsystems are interfaced bytranslators; by mapping messages to silence, these can restrict hearingand hide speech. Reversing a translator turns its scope inside out. Thispermits a new specification for a communication link: the environmentof each user should behave like the other user.This paper reports the stable aspects of an evolving study.
|
|
| 2. |
- Prasad, K V S, 1952
(författare)
-
A Calculus of Value Broadcasts
- 1993
-
Ingår i: Arndt Bode, Mike Reeve, Gottfried Wolf (Eds.): PARLE '93, Parallel Architectures and Languages Europe, 5th International PARLE Conference, Munich, Germany, June 14-17, 1993, Proceedings. Springer 1993 Lecture Notes in Computer Science. - 3540568913 ; , s. 391-402
-
Konferensbidrag (refereegranskat)abstract
- Computation can be modelled as a sequence of values, each broadcast by one agent and instantaneously audible to all those in parallel with it. Listening agents receive the value; others lose it. Subsystems interface via translators; these can scramble values and thus hide or restrict them. Examples show the calculus describing this model to be a powerful and natural programming tool. Weak bisimulation, a candidate for observational equivalence, is defined on the basis that receiving a value can be matched by losing it.
|
|
| 3. |
- Prasad, K V S, 1952
(författare)
-
Broadcasting with Priority
- 1994
-
Ingår i: Springer 1994 Lecture Notes in Computer Science, Programming Languages and Systems - ESOP'94, 5th European Symposium on Programming, Edinburgh, U.K., April 11-13, 1994, Proceedings. - 3540578803 ; , s. 469-484
-
Konferensbidrag (refereegranskat)abstract
- Adding priorities to CCS is difficult, and involves two-stage operational semantics or other complications. By contrast, priorities can be added very simply to a calculus of broadcasting systems (CBS). The reason is the input /output distinction made in CBS, with output actions being autonomous. Priority makes sense only for autonomous actions. As in unprioritised CBS, both strong and weak bisimulation are congruences, and capture the intuitively desired equivalences. CBS is also a powerful and natural language, offering an interesting new programming paradigm. Several examples show that priorities extend both the power and the paradigm.
|
|
| 4. |
- Prasad, K V S, 1952
(författare)
-
Combinators and Bisimulation Proofs for Restartable Systems
- 1991
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- During recent years, calculi for reasoning about concurrent systems have been developed; examples are CCS (Calculus of Communicating Systems), CSP (Communicating Sequential Processs) and ACP (Algebra of Communicating Processes). Their theory has been studied intensively; rather less has been done in applying these calculi to problems of significant size. The reported work in this direction suggests that we should be prepared to develop new formal systems and notation for the problems we attack, and also that the sheer mechanics are difficult enough that we need new techniques to organise and structure proofs.In this thesis we study bisimulation proofs, applied to a small set of related problems. We define a class of new operators to capture the structure in these problems, and use them to produce significantly smaller and clearer proofs than were previously possible. In order to avoid complexities due to interleavings, we use a new calculus, MCCS, that can be seen as lying between CCS and ASCCS (a variant of CCS); like the latter, MCCS allows synchronisation but is not a synchronous calculus.We begin by summarising the new layout for bisimulation proofs developed for a proof of a simple fault tolerant system carried out in CCS. This proof forms the Appendix to the thesis.Next, we define MCCS and study its properties. deriving most of themm from a proof of a simple fault tolerant system carried out in CCS. This proof forms the Appendix to the thesis.Next, we define MCCS and study its properties, deriving most of them from the related calculi, SCCS, ASCCS and CCS. This study also clarifies the relations between these older calculi, finding them to be closer than had been previously expressed in [Mil83]. In the process, we contribute to the study of ASCCS, the least studied of the three.Our new operators are designed specifically to help analyse the structure of systems into normal and exception processing; the major theorem in each case is the Synchronised Displacement Theorem. We comment on other possible design choices. We use the new operators and MCCS to reformulate and prove a variant of the example in the Appendix.A natural question that arises when we deal with new operators is whether they are derivable from the old. We study this matter, contributing a new technique for proving operators non-derivable. We prove many of the operators in SCCS and CCS to be independent, i.e. not definable in terms of the other operators.
|
|
| 5. |
- Prasad, K V S, 1952
(författare)
-
Programming with Broadcasts.
- 1993
-
Ingår i: Springer 1993 Lecture Notes in Computer Science, Eike Best (Ed.): CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings.. - 3540572082 ; , s. 173-187
-
Konferensbidrag (refereegranskat)abstract
- [Pra91, Pra92] develop CBS, a CCS-like calculus [Mil89] where processes communicate by broadcasting values along a single channel. These values are hidden or restricted by translation to noise. This paper types CBS and restricts it to processes with a unique response to each input. Non-determinism arises only if two processes in parallel both wish to transmit. These restrictions do not reduce the programming power of CBS. But strong and weak bisimulation can now be defined exactly as in CCS, yet capture observationally meaningful relations. Weak bismulation is a congruence. This paper also shows how to program in CBS in a (lazy) ML framework. A simple CBS simulator is given, and a parallel implementation discussed. The simulator represents data evaluation, recursion and conditionals directly in Lazy ML. It implements an extended CBS with evaluation as well as communication transitions.
|
|
