Bisimulation for reactive frames

Reactive frames are those whose structure is not fi xed but can vary according to the path chosen. This kind of frame has been study and both a logic and an axiomatization for it were already developed. In this paper we take this study further and de fine a notion of bisimulation for reactive models...

Full description

Bibliographic Details
Main Author: Figueiredo, Daniel (author)
Other Authors: Martins, Manuel António (author)
Format: conferenceObject
Language:eng
Published: 2018
Subjects:
Online Access:http://hdl.handle.net/10773/21327
Country:Portugal
Oai:oai:ria.ua.pt:10773/21327
Description
Summary:Reactive frames are those whose structure is not fi xed but can vary according to the path chosen. This kind of frame has been study and both a logic and an axiomatization for it were already developed. In this paper we take this study further and de fine a notion of bisimulation for reactive models. We show that the logic introduced by Marcelino for these frames is invariant under our notion of bisimulation. Finally, we proof the Hennessy-Milner theorem for a class of reactive models.