Within the past decade, model checking has emerged to be a useful technique for verifying the correctness of real-time systems. Two different time semantics are commonly employed: dense or discrete. A major advantage of model checking under a dense-time model is its ability to give precise information about the behavior of a real-time system. On the other hand, model checking under a discrete-time model is simpler and a wide variety of verification methods are readily available. While a number of verification methods have been developed for these two kind of models, comparatively little effort has been invested in exploring the possibility of reducing dense-time verification problems to discrete-time verification problems....[ Read more ]

Within the past decade, model checking has emerged to be a useful technique for verifying the correctness of real-time systems. Two different time semantics are commonly employed: dense or discrete. A major advantage of model checking under a dense-time model is its ability to give precise information about the behavior of a real-time system. On the other hand, model checking under a discrete-time model is simpler and a wide variety of verification methods are readily available. While a number of verification methods have been developed for these two kind of models, comparatively little effort has been invested in exploring the possibility of reducing dense-time verification problems to discrete-time verification problems.

In 1992, T.A. Henzinger proposed a digitization technique which allows the verification of dense real-time systems to be reduced to the problem of verifying the systems under a discrete-time model. This digitization technique has been successfully applied to the verification of the linear-time temporal logic MTL. In this work, we study the possibility of applying this digitization technique to the verification of real-time distributed systems by using branching-time temporal logics. For this purpose, a number of CTL-based branching-time temporal logics are studied, These branching- time temporal logics can be divided into two groups: timed and untimed. In the timed group, the logics included are OCTL, ∀QCTL, [there exists]QCTL, and SQCTL, and in the untimed group, the logics included are CTL, ∀CTL, [there exists]CTL, and SCTL. It is found that in the timed case, only the verification of SQCTL can be reduced whose expressive power is very limited. In the untimed case, for systems that consist of single processes, the verification of CTL, ∀CTL, [there exists]CTL, and SCTL are proved to be reducible. However, for systems that consist of multiple communicating processes, even though the logics are untimed, the verification of CTL, which has the largest expressive power among the logics in the untimed group, is found to be non-reducible. The results of our study suggest that the digitization technique is not suitable to be used in the verification of CTL-based branching-time temporal logics.