A proof rule for control loops
Plants are often controlled by looping programs that repeatedly cycle through a fixed set of production steps or alternate between a sensing phase and a correction phase. To ensure that a control program is safe we must verify a certain inequation. The contribution of this article is a calculational rule for proving such inequations. Its formal statement and proof is given in temporal algebra, which is an algebraic calculus encompassing logics such as CTL, linear temporal logic, interval logic and the duration calculus. The first part of this paper (Sec. 2-4) gives a short introduction to temporal algebra. In Sec. 5 we state the proof rule and establish its correctness. The next two sections extend the basic calculus with measures and durations. In Sec. 8 we give two examples that illustrate the use of our proof rule. The paper is concluded in Sec. 9 with a meta-theorem that reduces the verification of infinite loops to the verification of finite ones. For the entire collection see [Zbl 0891.00027].
This page was built for publication: A proof rule for control loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4213375)
