Action refinement is a useful methodology for the development of concurrent processes in a stepwise manner. We are here interested in establishing a connection between syntactic action refinement and logic. In the syntactic approach to action refinement, reduction functions are used to remove the refinement operators from process-algebraic expressions thereby providing semantics for them. We incorporate a syntactic action refinement operator to the Hennessy-Milner-Logic and define a logical reduction function for this extended logic. This provides a possibility to refine a process expression and a formula simultaneously on the syntactic level, while preserving their satisfaction relation. It turns out that the assertion P ≠ φ ⇔ P[a ⇔ Q] ≠ φ[a ⇔ Q] where .(a ⇔ Q] denotes the refinement operator both, on process terms and formulas holds in the considered framework under weak and reasonable restrictions.
Dieser Eintrag ist Teil der Universitätsbibliographie.
Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.
Search Authors in