Model Synthesis from Partial Model with partial labelling
Sophie Paillocher · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
We consider the following generic scenario: an abstract model M of some ‘real’ systemis only partially presented, or partially known to us, and we have to ensure that theactual system satisfies a given specification, formalised in BML or LTL. Our questionis, "does any extension of the partial model satisfying the specification exist ?" In thatpurpose, we propose an algorithm that returns all the admissible extensions for the casewhere only the interpretation function is partially known.