Real-time logics: Complexity and expressiveness (Q689093)

The authors consider the theory of timed state sequences which combines classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. This is suitable for reasoning about real-time temporal systems. They showed to be able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and they present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.