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} ,
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 ,
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 ,
Reactive Systems: Modelling, Specification and Verification, 2007. ,
DOI : 10.1017/CBO9780511814105
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
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
Hybrid Logic and its Proof?Theory. App. Logic Series, 2010. ,
A hidden agenda, Theoretical Computer Science, vol.245, issue.1, pp.55-101, 2000. ,
DOI : 10.1016/S0304-3975(99)00275-3
Dynamic Logic, 2000. ,
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
Communication and concurrency. PHI Series in computer science, 1989. ,
Foundations of Algebraic Specification and Formal Software Development. Monographs on TCS, an EATCS Series, 2012. ,