Sampling semantics of Duration Calculus

Abstract

In the paper, the problem of discretization of continuous time in Duration Calculus (DC) is addressed. For a DC formula D, for a sampling step h, a sampling semantics [D]_h is defined to express the properties of discrete observations of its models, while original semantics [D] expresses the properties of the models. In practice, only sampling semantics is implemented. So, an implementation D of a system specified by S, where both are written in DC, is correct iff $[[D]]_h \subseteq [[S]]$. Some rules for proving the correctness of an implementation are given. The problem of digitization is also considered in the paper. Some forms of digitizable DC formulas are shown. Then we apply the obtained results to a non-trivial example, namely, a Biphase Mark Protocol introduced in [11]. That protocol uses 18-cycle cell for one bit of message. A cell is formed by 5-cycle mark subcell followed by 13-cycle code subcell. We adopt the same assumptions about physical environment as in [11]. However, we are able to show a stronger property than in [11]: The protocol works correctly provided the ratio of the writer's and reader's clock is within 30%.

On leave from the Institute of Information Technology, Nghia Do, Tu Liem, Hanoi, Vietnam.