Model Counting Results

To automatically compute the semantic distance between the original unrealizable specification and the candidate repairs we use LTL Model Counting.

It is well-known that the fitness function is frequently evaluated during the evolution process, so we need an efficient model counting approach to evaluate the semantic distance. Due to the exact model counting approaches quickly reach their scalability limits, and sicne we want to compute the behaviours that some refinements preserve and remove from the original specification, we need model counting analyses to scale to relatively large values of the bound. For this reason, we implemented an efficient Automata-Based Model Counting approach.

To evaluate our approach, we considered two related approaches. On the one hand, we re-implemented an exact model counting approach (basically, we translate LTL formulas as propositional formulas, and then use a Propositional Model Counter), and on the other hand, we considered an approach based on regular expressions.

To carry out this evaluation, we took 10 sets of 50 random LTL formulas each, taken from a well-established benchmark. For each formula in each set, we computed the number of models by using the exact model counting, the regex approach, and our approximate model counting. We computed this for values of the bound k from 6 to 10. Then, we elaborate an ascending ranking for the values obtained with each technique, and then compare these rankings to verify if the exact ranking is preserved by the other techniques.

You can download the results of our experimental evaluation from this link: Results.zip. 

The following tables summarize all our study, where: MC, Exact MC and RE MC, refers to our approach, the exact model counting approach, and the regex approach, respectively.

Column Diff(Exact-MC) represents the number of formulas incorrectly ranked by our approach; while column Diff(Exact-RE) represents the number of formulas incorrectly ranked by RE approach.

K = 6:

K = 7:

K = 8:

K = 9:

K = 10:

Running the experiments:

To reproduce the experiments shown above, we provide the next script:

• run-modelcounting-evaluation.sh K This script runs the model counter evaluation with each set. Notice that, the bound K must be indicated,and by default, the script will run the exact model counter, therefore it is necessary to edit it by adding the flag -re to run the regex approach and the flag -auto to run our model counting approach.