Lookup NU author(s): Dr Alexei Iliasov,
Dr Jeremy Bryans
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
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.
Author(s): Iliasov A, Bryans J
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Perspectives of System Informatics
Year of Conference: 2015
Print publication date: 01/01/2015
Acceptance date: 01/01/1900
Publisher: Springer Berlin Heidelberg
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science