We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.
|Title of host publication||International Andrei Ershov Memorial Conference on Perspectives of System Informatics|
|Place of Publication||Berlin|
|Number of pages||16|
|Publication status||E-pub ahead of print - 19 Apr 2015|