Motivated by issues in temporal databases and in the verification of infinite-state systems, this talk considers the problem of representing periodic dense time information. Doing so requires handling a theory that combines discrete and continuous variables, since discrete variables are essential for representing periodicity. An automata-based approach for dealing with such a combined theory is thus introduced. This approach uses the fact that real numbers can be represented by infinite sequences of digits and hence that sets of real numbers can be viewed as infinite-word languages, which can be recognized by infinite-word finite automata. Since these automata can represent all linear constraints, can express intergerhood, and are closed under the first-order constructs, the presented approach can handle the full first-order theory of linear constraints over the reals and integers. One problem with using infinite-word automata is that the algorithms for complementing them are especially complicated and difficult to implement effectively. Fortunately, with the help of topological arguments it can be shown that a very restricted and much more tractable class of infinite-word automata are sufficient for the purpose on hand. Background information on the topics presented in this talk can be found in [1, 2, 3, 4].
展开▼
