Abstract When dealing with unrealizable specifications in reactive synthesis, finding the weakest environment assumptions that ensure realizability is often considered a desirable property. However, little effort has been dedicated to defining or evaluating the notion of weakness of assumptions formally. The question of whether one assumption is weaker than another is commonly interpreted by considering the implication relationship between the two or, equivalently, their language inclusion. This interpretation fails to provide any insight into the weakness of the assumptions when implication (or language inclusion) does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it cannot distinguish the weakness of assumptions expressed as fairness properties. In this paper, we propose a refined measure of weakness based on combining entropy with Hausdorff dimension, a concept that captures the notion of size of the ω -language satisfying a linear temporal logic formula. We focus on a special subset of linear temporal logic formulae which is of particular interest in reactive synthesis, called GR(1). We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae, and propose a refined measure to cover cases when two formulae are strictly ordered by implication but have the same entropy and Hausdorff dimension. We prove the consistency between our weakness measure and logical implication, that is, if one formula implies another, the latter is weaker than the former according to our measure. We evaluate our proposed weakness measure in two contexts. The first is in computing GR(1) assumption refinements where our weakness measure is used as a heuristic to drive the refinement search towards weaker solutions. The second is in the context of quantitative model checking where it is used to measure the size of the language of a model violating a linear temporal logic formula.

We investigate the dependence of software failure reproducibility on the environment in which the software is executed. The existence of such dependence is ascertained in literature, but so far it is not fully characterized. In this paper we pinpoint some of the environmental components that can affect the reproducibility of a failure and show this influence through an experimental campaign conducted on the My SQL Server software system. The set of failures of interest is drawn from My SQL's failure reports database and an experiment is designed for each of these failures. The experiments expose the influence of disk usage and level of concurrency on My SQL failure reproducibility. Furthermore, the results show that high levels of usage of these factors increase the probabilities of failure reproducibility.