This paper presents a process algebra for distributed systems in which some actions may take precedence over others. The algebra is distinguished by the design decision that it only allows actions to pre-empt others at the same ``location'' and therefore captures a notion of localized precedence. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence and present logical characterizations of our behavioral relations. Simple examples highlight the utility of the theory.
We present TwoTowers, a tool for analyzing functional and performance properties of concurrent systems expressed as terms in the stochastically timed reward process algebra EMPAv. TwoTowers builds on two existing tools, CWB-NC and MarCA, that have been retargeted to carry out functional and performance analysis (respectively) of EMPAv system specifications. As an example, we describe the application of TwoTowers to the Lehmann-Rabin randomized distributed algorithm for th dining philosopher problem.
PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilsitic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parmeterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example.
We introcude several new notions of infinite testing, for both probabilistic and nonprobabilistic processes, and carefully examine their distinguishing power. We consider three kinds of infinite tests, simple, Buechi and fair. We show that Buechi tests do not change the distinguishing power of nondeterministic testing. In the probabilistic setting, we show that all three have the same distinguishing power as finite tests. Finally, we show that finite probabilistic tests are stronger than nondeterministic fair tests.
| Go to Rance Cleaveland's publication home page. |
Last modified: April 7, 1999
Rance Cleaveland