On Syntactic Action Refinement and Logic


Majster-Cederbaum, Mila ; Salger, Frank


[img]
Vorschau
PDF
1999_07.pdf - Veröffentlichte Version

Download (1MB)

URL: http://ub-madoc.bib.uni-mannheim.de/2058
URN: urn:nbn:de:bsz:180-madoc-20584
Dokumenttyp: Arbeitspapier
Erscheinungsjahr: 1999
Sprache der Veröffentlichung: Englisch
Einrichtung: Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Sonstige - Fakultät für Mathematik und Informatik
MADOC-Schriftenreihe: Veröffentlichungen der Fakultät für Mathematik und Informatik > Institut für Informatik > Technical Reports
Fachgebiet: 004 Informatik
Normierte Schlagwörter (SWD): Prozessalgebra
Abstract: 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.
Zusätzliche Informationen:

Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.




+ Zitationsbeispiel und Export

Majster-Cederbaum, Mila und Salger, Frank (1999) On Syntactic Action Refinement and Logic. [Arbeitspapier]
[img]
Vorschau



+ Suche Autoren in

+ Download-Statistik

Downloads im letzten Jahr

Detailierte Angaben



Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail


Actions (login required)

Eintrag anzeigen Eintrag anzeigen