A decidable temporal logic with repeating values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Renormalization group invariants and sum rules in the deflected mirage mediation supersymmetry breaking

We examine the deflected mirage mediation supersymmetry breaking (DMMSB) scenario, which combines three supersymmetry breaking scenarios, namely anomaly mediation, gravity mediation and gauge mediation using the one-loop renormalization group invariants (RGIs). We examine the effects on the RGIs at the threshold where the gauge messengers emerge, and derive the supersymmetry breaking parameters in terms of the RGIs. We further discuss whether the supersymmetry breaking mediation mechanism can be determined using a limited set of invariants, and derive sum rules valid for DMMSB below the gauge messenger scale. In addition we examine the implications of the measured Higgs mass for the DMMSB spectrum.