A real-time process algebra, called ACSR, has been developed to facilitate the specification and analysis of real-time systems. ACSR supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real-time systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. In addition to operators common to process algebra, ACSR includes the scope operator, which can be used to model timeouts and interrupts. Equivalence between ACSR terms is based on the notion of strong bisimulation. This paper briefly describes the syntax and semantics of ACSR and then presents a set of algebraic laws that can be used to prove equivalence of ACSR processes. The contribution of this paper is the soundness and completeness proofs of this set of laws. The completeness proof is for finite-state ACSR processes, which are defined to be processes without free variables under parallel operator or scope operator.

The correctness of real-time distributed systems depends not only on the function they compute but also on their timing characteristics. Furthermore, those characteristics are strongly influenced by the delays due to synchronization and resource availability. Process algebras have been used successfully to define and prove correctness of distributed systems. More recently, there has been a lot of activity to extend their application to real-time systems. The problem with most current approaches is that they ignore resource constraints and assume either maximum parallelism (i.e., unlimited resources) or pure interleaving (i.e., single resource). Algebra of communicating shared resources (ACSR) is a process algebra designed for the formal specification and manipulation of distributed systems with resources and real-time constraints. A dense time domain provides a more natural way of specifying systems compared to the usual discrete time. Priorities provide a measure of urgency for each action and can be used to ensure that deadlines are met. In ACSR, processes are specified using resource bound, timed actions and instantaneous synchronization events. Processes can be combined using traditional operators such as nondeterministic choice and parallel execution. Specialized operators allow the specification of real-time behavior and constraints. The semantics of ACSR is defined as a labeled transition system. Equivalence between processes is based on the notion of strong bisimulation. A sound and complete set of algebraic laws can be used to transform almost any ACSR process into a normal form.

Recently, significant progress has been made in the development of timed process algebras for the specification and analysis of real-time systems. This paper describes a timed process algebra called ACSR, which supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. The paper also includes a brief overview of other timed process algebras and discusses similarities and differences between them and ACSR.>