An effective axiomatization for real time ACP
Baeten and Bergstra added real time to ACP, and introduced the notion of integration, which expresses the possibility of an action happening within a time interval. In order to axiomatize this feature, they needed an `uncountable' axiom. This paper deals with prefix integration, and integration is parametrized by conditions, which are inequalities between linear expressions of variables. We present an axiomatization for process terms, and propose a strategy to decide bisimulation equivalence between process terms, by means of this axiomatization.
|Formal Definitions and Theory (acm D.3.1), Specifying and Verifying and Reasoning about Programs (acm F.3.1), Semantics of Programming Languages (acm F.3.2)|
|Semantics (msc 68Q55), Specification and verification (program logics, model checking, etc.) (msc 68Q60)|
|Department of Computer Science [CS]|
Fokkink, W.J, & Klusener, A.S. (1995). An effective axiomatization for real time ACP. Department of Computer Science [CS]. CWI.