# Formalizing “dual-time” temporal logic

I am interested in modeling a discrete temporal logic based on music, where there are two metrics of time, beat and seconds, (call them B and S). The constraints on what constitutes a syntactically valid formula is that the following conditions are satisfiable

• If B(t) = a and B(t + 1) = b, there must be some t2 and t3 such that S(t2) = a and S(t2 + t3) = b, and the value of S between t2 and t3 is a.
• Similarly, If S(t) = a and S(t + 1) = b, there must be some t2 and t3 such that B(t2) = a and B(t2 + t3) = b, and the value of B between t2 and t3 is a.
• If B(t_i - 1) = a and B(t_i..t_i + k) = b and B(t_i + k + 1) = c, there must be an interval S(t_j..t_j + m) = a such that S(t_j - 1) = a, S(t_j..t_j + m) = b, S(m + 1) = c, and (m/k) is in some range on the reals.

Intuitively, I'm trying to define a system where time doesn't always pass proportionally between "beat time" and "second time" (because the beats per second fluctuates), but where there is a constraint to how much this fluctuation can occur.

Does such a logic exist currently, or are there any ideas of how to fit existing temporal logics to this paradigm?

For instance: The values for B(0,1,2,3,4) = 0,0,1,0,1 and S(1,2,3,4,5,6) = 0,1,1,0,1,1 would constitute semantically meaningful facts at a difference threshold of 2, because it can be interpreted as an event of 0 taking two B ticks and 1 S tick, an event of 1 taking one B tick and two S ticks, an event of 0 taking one B tick and one S tick, and an event of 1 taking one B tick and two S ticks, occurring in a temporal succession. In contrast, the values for B(0,1,2) = 1,1,0 and S(0,1,2) = 0,1,0 is not a valid set of facts, because there is no way to map from B to S by shrinking or expanding the number of ticks an event takes before the successive event.