Compositional reasoning using intervals and time reversal

Date

2013-06-05

Advisors

Journal Title

Journal ISSN

ISSN

1012-2443
1573-7470

Volume Title

Publisher

Springer

Type

Article

Peer reviewed

Yes

Abstract

Interval Temporal Logic (ITL) is an established formalism for reasoning about time periods. We investigate some simple kinds of ITL formulas which have application to compositional reasoning and furthermore are closed under conjunction and the conventional temporal operator known both as “box” and “always”. Such closures help us modularly construct formulas from simple building blocks in a way which preserves useful compositional properties. The most important class considered here is called the 2-to-1 formulas. They offer an attractive framework for analysing sequential composition in ITL and provide the formal basis for most of the subsequent presentation. A key contribution of this work concerns a useful and apparently new and quite elementary mathematical theorem that 2-to-1 formulas are closed under “box”. We also use a natural form of time symmetry with 2-to-1 formulas. This extends known facts about such formulas by looking at them in reverse. An important example involves showing that 2-to-1 formulas are also closed under a variant of “box” for prefix subintervals rather than suffix ones. We then apply the compositional formulas obtained with time symmetry to analyse concurrent behaviour involving mutual exclusion in both Peterson’s algorithm and a new and more abstract one. At present, our study of mutual exclusion mainly serves as a kind of experimental “proof of concept” and research tool to develop and illustrate some of the logical framework’s promising features. We also discuss how time symmetry sometimes assists in reducing reasoning in ITL to conventional linear-time temporal logic.

Description

Keywords

Interval Temporal Logic, Compositional reasoning, Formal verification, Time reversal, Symmetry, Mutual exclusion, Peterson’s algorithm

Citation

Moszkowski, B.C. (2014) Compositional reasoning using intervals and time reversal. Annals of Mathematics and Artificial Intelligence, 71 (1-3), pp. 175-250

Rights

Research Institute