Correspondence:
[*]
Address for correspondence: LISCO Laboratory - Department of computer science, Badji Mokthar Annaba University, PO BOX 12, Annaba, Algeria.
Abstract: Probabilistic models play an important role in many fields such as distributed systems and simulations. Like non-probabilistic systems, they can be synthesized using classical refinement-based techniques, but they also require identifying the probability distributions to be used and their parameters. Since a fully automated and blind refinement is generally undecidable, many works tried to synthesize them by looking for the parameters of the distributions. Syntax-guided synthesizing approaches are more powerful, they try to synthesize models structurally by using context-free grammars. However, many problems arise like huge search space, the complexity of generated models, and the limitation of context-free grammars to define constraints over the structure. In this paper, we propose a multi-step refinement approach, based on meta-models, offering several abstraction levels to reduce the size of the search space. More specifically, each refinement step is divided into two stages in which the desired shape of models is first described by context-sensitive constraints. In the second stage, model templates are instantiated by using global optimization techniques. We use our approach to a synthesize a set of optimal probabilistic models and show that context-sensitive constraints coupled with the multi-level abilities of the approach make the synthesis task more effective.
Keywords: model synthesis, refinement, search-based software engineering, constraint satisfaction, probabilistic model checking
