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.
Additional information:
Dieser Eintrag ist Teil der Universitätsbibliographie.
Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.
![[img]](https://madoc.bib.uni-mannheim.de/style/images/fileicons/application_pdf.png)
Search Authors in