A CALCULUS BASED ON ABSENCE OF ACTIONS 1.pdf

A CALCULUS BASED ON ABSENCE OF ACTIONS1 Padmanabhan Krishnan Department of Computer Science University of Canterbury, PBag 4800 Christchurch, New Zealand E-mail: paddy@cosc.canterbury.ac.nz Abstract In this article we present a process algebra where the behaviour can be specied when certain actions cannot be exhibited. This is useful in specifying time outs, interrupts etc. We present a few properties which form the basis for a sound and complete axiomatisation of a bisimulation equivalence relation. A comparison with other approaches is presented. 1 Introduction Most approaches to concurrency and synchronisation are based on the presence of information. The rules that govern behaviour usually state that if a certain type of behaviour is possible, then another type of behaviour is also possible. But such a framework is not sucient especially when one has to include concepts such as interrupts and priorities. To specify the semantics (and hence to implement) features such as interrupts and priorities, it is essential to have both the presence of and the absence of information. That is, we need to specify that if a certain behaviour is impossible, then some other behaviour is possible. The use of negative information has many uses including default reasoning in articial intelligence [Rei80] and the select-else construct in Ada [Ada83]. In the default reasoning situation, the classical example is the assumption that all birds can y which is discarded when penguin is a bird and penguins cannot y is asserted. Thus the validity of the assertion that all birds can y requires the absence of information on penguins. In Ada, the `else alternative in a `select statement is executed only if the other `entries cannot be accepted. To execute the `else alternative, knowing that there are no pending entry calls is essential. While there have been various approaches to include priorities and interrupts in the context of concurrency, the work by Saraswat [SJG95] et. al. is the