?. Abs, . Sp-), M. Let, ?. Abs, and . Sp-), By Cor. 3, M |= ? ?, and hence M ? Mod ? (SP ) For this direction, assume M ? Mod (SP ). Hence, M ? Abs ? (SP ) By assumption Mod ? (SP ) = Abs ? (SP ) and hence M ? Mod ? (SP ). Finally we want to discuss the relationship of observational semantics with abstractor semantics in the context of fully abstract models. An A-model M is fully abstract if the observational equality ? M coincides with the set-theoretic equality of states, The fully abstract semantics of a specification SP = (A, ?) in D ? is given by the class of its fully abstract models Mod fa (SP ) = {M ? Mod (SP ) | M is fully abstract}

. Proof, The proof of the inclusion " ? " is the same as for part 1 in Thm. 8 taking into account that M/? is fully abstract. It remains to show Abs fa

?. Mod and . Sp-), Let M ? Abs fa ? (SP ) Then M ? N for some N ? Mod fa (SP ) Since N |= ? and N is fully abstract, we have N |= ? ?. Since M ? N we get, by Cor

R. 1. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba, Reactive Systems: Modelling, Specification and Verification, 2007.
DOI : 10.1017/CBO9780511814105

M. Bidoit and R. Hennicker, Constructor-based observational logic, The Journal of Logic and Algebraic Programming, vol.67, issue.1-2, pp.3-51, 2006.
DOI : 10.1016/j.jlap.2005.09.002

M. Bidoit, R. Hennicker, and M. Wirsing, Behavioural and abstractor specifications, Science of Computer Programming, vol.25, issue.2-3, pp.149-186, 1995.
DOI : 10.1016/0167-6423(95)00014-3

T. Bräuner, Hybrid Logic and its Proof?Theory. App. Logic Series, 2010.

J. A. Goguen and G. Malcolm, A hidden agenda, Theoretical Computer Science, vol.245, issue.1, pp.55-101, 2000.
DOI : 10.1016/S0304-3975(99)00275-3

D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic, 2000.

A. Madeira, L. S. Barbosa, R. Hennicker, and M. A. Martins, Dynamic Logic with Binders and Its Application to the Development of Reactive Systems, Theoretical Aspects of Computing -ICTAC 2016, pp.422-440, 2016.
DOI : 10.1007/978-3-642-17336-3

R. Milner, Communication and concurrency. PHI Series in computer science, 1989.

D. Sannella and A. Tarlecki, Foundations of Algebraic Specification and Formal Software Development. Monographs on TCS, an EATCS Series, 2012.