Journal of Logic and Computation, Volume 8, Issue 5, pp. 669678: Abstract.
On the decidability of continuous time specification formalismsA Rabinovich Department of Computer Science, Tel Aviv University, Tel Aviv 69978, Israel. Email: rabino@math.tau.ac.il
We consider an interpretation of monadic secondorder logic of order in the continuous time structure of finitely variable signals and show the decidability of monadic logic in this structure. The expressive power of monadic logic is illustrated by providing a straightforward meaning preserving translation into monadic logic of three typical continuous time specification formalism: temporal logic of reals, restricted duration calculus and the propositional fragment of mean value calculus. As a byproduct of the decidability of monadic logic we obtain that the above formalisms are decidable even when extended by quantifiers. Key words: Monadic secondorder logic, temporal logic, duration calculus, decidability.
