A Complete Axiomatization of Finite-state ACSR Processes

Patrice Brémond-Grégoire, Jin Young Choi, Insup Lee

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)124-159
Number of pages36
JournalInformation and Computation
Volume138
Issue number2
Publication statusPublished - 1997 Nov 1

Fingerprint

Axiomatization
Real time systems
Algebra
Mathematical operators
Synchronization
Process Algebra
Operator
Real-time
Completeness
Semantics
Equivalence
Specifications
Resources
Bisimulation
Soundness
Instantaneous
Specification
Term
Model

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

A Complete Axiomatization of Finite-state ACSR Processes. / Brémond-Grégoire, Patrice; Choi, Jin Young; Lee, Insup.

In: Information and Computation, Vol. 138, No. 2, 01.11.1997, p. 124-159.

Research output: Contribution to journalArticle

Brémond-Grégoire, P, Choi, JY & Lee, I 1997, 'A Complete Axiomatization of Finite-state ACSR Processes', Information and Computation, vol. 138, no. 2, pp. 124-159.
Brémond-Grégoire, Patrice ; Choi, Jin Young ; Lee, Insup. / A Complete Axiomatization of Finite-state ACSR Processes. In: Information and Computation. 1997 ; Vol. 138, No. 2. pp. 124-159.
@article{951863aa6440476086046291849f42dd,
title = "A Complete Axiomatization of Finite-state ACSR Processes",
abstract = "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.",
author = "Patrice Br{\'e}mond-Gr{\'e}goire and Choi, {Jin Young} and Insup Lee",
year = "1997",
month = "11",
day = "1",
language = "English",
volume = "138",
pages = "124--159",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "2",

}

TY - JOUR

T1 - A Complete Axiomatization of Finite-state ACSR Processes

AU - Brémond-Grégoire, Patrice

AU - Choi, Jin Young

AU - Lee, Insup

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

UR - http://www.scopus.com/inward/citedby.url?scp=0347936128&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0347936128

VL - 138

SP - 124

EP - 159

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -