Hur valet av specifikationsspråk påverkar körtiden för en algoritm som verifierar refinement för probabilistiska kontrakt

This thesis investigates how the choice of specification language impacts the performance of an algorithm for verifying refinement of probabilistic contracts. Different specification languages are capable of expressing different requirements, and some specification languages have more costly operations associated with them. The goal of this thesis is therefore to investigate how practical the algorithm for verifying refinement is when it is instantiated with two different specification languages, where one of the languages (MLTL) is significantly more challenging to work with compared to the other specification language (LTL). The specification languages under consideration are the temporal logics LTL and a variation of its real-time extension, MTL, called MLTL. A benchmarking of the algorithm was conducted with (1) fully randomly generated refinement problems, (2) randomly generated refinement problems that resemble common specifications found in both literature and industry, and (3) a simple manually constructed refinement problem based on a real world example, where the number of components were higher than in the randomly generated refinement problems. The results show that when LTL is used, the algorithm was capable of verifying refinement within a one minute timeout on all smaller test cases where the LTL formulas were allowed to use up to 500 operators, and it was capable of verifying refinement within a 10-minute timeout on all larger test cases where the LTL formulas were allowed to use up to 10000 operators. When MLTL was used, verifying refinement proved to be significantly more challenging in general, only capable of solving around 24% of the fully randomly generated refinement problems within a 1-minute timeout, where MLTL formulas were allowed to use up to 50 operators. Still, the algorithm performed well on the randomly generated refinement problems based on common specification patterns where it managed to solve around 90% of the refinement problems within a 1-minute timeout. On the manually written refinement problem that was based on a real world example the algorithm had similar performance for both LTL and MLTL specifications.