TY - JOUR
T1 - A Complete Axiomatization of Finite-state ACSR Processes
AU - Brémond-Grégoire, Patrice
AU - Choi, Jin Young
AU - Lee, Insup
N1 - Funding Information:
* This research was supported in part by AFOSR F49620-95-1-0508, ARO DAAH04-95-1-0092, NSF CCR 93-11622, and NSF CCR 94-15346. -Department of Computer Science and Engineering, Korea University, Seoul, Korea.
PY - 1997/11/1
Y1 - 1997/11/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0347936128&partnerID=8YFLogxK
U2 - 10.1006/inco.1997.2657
DO - 10.1006/inco.1997.2657
M3 - Article
AN - SCOPUS:0347936128
SN - 0890-5401
VL - 138
SP - 124
EP - 159
JO - Information and Computation
JF - Information and Computation
IS - 2
ER -