In this short note, we are concerned with the fairness condition "A and B hold almost equally often", which is important for specifying and verifying the correctness of non-terminating processes and protocols. We introduce the logic of temporal domination, in which the above condition can be expressed. We present syntax and semantics of our logic and show that it is a proper extension of linear time temporal logic. In order to obtain this result, we rely on the corresponding result for k-counting automata.

翻译：在这篇短文中，我们关注公平性条件“A和B几乎同等频繁成立”，该条件对于非终止进程与协议的规约和正确性验证至关重要。我们提出时间支配逻辑，该逻辑能够表达上述条件。我们给出了所提逻辑的语法和语义，并证明它是对线性时序逻辑的真扩展。为获得这一结果，我们依赖于k-计数自动机的相应结论。