Model Synthesis from Partial Model with partial labelling

Sophie Paillocher (1)

1 IBISC - Informatique, BioInformatique, Systèmes Complexes

We consider the following generic scenario: an abstract model M of some ‘real’ system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in BML or LTL. Our question is, "does any extension of the partial model satisfying the specification exist ?" In that purpose, we propose an algorithm that returns all the admissible extensions for the case where only the interpretation function is partially known.

Domains: Data Structures and Algorithms [cs.DS]; Logic in Computer Science [cs.LO]; Symbolic Computation [cs.SC]

Sophie Paillocher. Model Synthesis from Partial Model with partial labelling. [Research Report] Université Paris-Saclay, Université d'Evry Val-d'Essonne. 2021, pp.35. ⟨hal-03284114⟩