In the modeling space, various level of abstractions have been introduced to facilitate readability and improve correctness (by minimizing details). For example, a flat transition system may be encoded hierarchically. Although these systems differ structurally, it is expected that they behave similarly.
To certify equivalence of these models, a formal (or mathematically sound) method is required to prove this. While theorem proving may be applicable, though difficult to apply, a fully automated approach (i.e., model checking) should surface to realize our goal.
Are you aware of any model checking approach that can answer the equivalence question by a button press?
usually you have to define an equivalence relation that specifies what does it mean for two models to be equivalent. To do so, you have to map both models into the same semantic domain, say an LTS or whatever suits you. Then you have to formalize, as I mentioned before, what it means for two models to be behaviorally equivalent. This thing is application-dependent. In concurrency theory, you usually define a notion of bisimulation which generally states that two models are equivalent if they can mimic each other in terms of observations. The point here is that you look at your models as black boxes and if one of them can do a move, the other one should be able to mimic this move and vise versa.
The point that I want to stress is that you have to somehow translate your models into a common framework, whether it is another language with a well-understood semantics or into a mathematical domain. After that you define your notion of equivalence and there are plenty of algorithms to compute equivalence relations. For instance if your semantic domain is an LTS and you have a notion of bisimulation then you can use that standard Paige-Tarjan algorithm for partition refinement.
As for a tool that can compute bisimulation with a click, take a look at TAPAs
https://link.springer.com/chapter/10.1007%2F978-3-540-89287-8_4
It is only for process algebra.
Note: if your models are sequential in nature, then the equivalence checking would be much easier as you can rely on denotational semantics. For operational models where concurrency is involved, the situation is more complicated with respect to sequential models. In sequential models, a program generally can be defined as function with input and output and you don't care what happens in between (assuming there are no side-effects), but in concurrency, program executions interleave and you have to take care about what happens in between.
Hope that would be of help to you
Yehia
P.S. this is called equivalence checking not model checking.
https://link.springer.com/chapter/10.1007%2F978-3-540-89287-8_4
Formal checking equivalence between two models is quite general, i think. We also proposed an approach to checking equivalence of two models in software refactoring.
https://link.springer.com/article/10.1007/s11036-017-0807-z
Hope this helps,
Anh Le
Thanks all, for your contributions.
To guarantee that we are all on the same page, I would like to make the following clarifications and/or re-emphasize some points. I consider them important after reading the comments made.
1. The notion of model checking comes from the fact that I want exhaustive exploration of the state-space and want it done automatically (i.e., a push-button approach). That's what I meant by how to model-check tow models for equivalence. Thanks for recommending appropriate terminology.
2. I already have my models translated to SMV representation, the input language of nuXmv model checker. At this junction, my expectation is suggestions of various algorithms (and/or steps) to actualize the task.
3. My understanding of syntax and semantics equivalence is pertinent to the language of implementation. I am not particular about this. For instance, our model may be implemented in any variant(s) of UML (e.g., Umple) and translated to an input language of a model checker (e.g., SMV). In this case, the structure may differ and semantics will be based on the language as well. Therefore, my concern is to check the equivalence, behavior-wise.
4. The model being considered in this context are mainly state machines.