Abstract
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.
Cite
CITATION STYLE
Iliasov, A., & Bryans, J. (2015). A proof-based method for modelling timed systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8974, pp. 161–176). Springer Verlag. https://doi.org/10.1007/978-3-662-46823-4_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
