A verifiable model of a minimal market operating sequentially, with price and time discrete - Žunić, Dragiša (Journal of Computer and Forensic Sciences, 2023)
This research presents a minimal computational market model, i.e.,a model of a trading venue, with sequential order matching, in a declarative style, and proceeds to demonstrate how some fundamental properties can be formally proved. It is a challenging task to formally certify properties for a fundamental system in any realm of human endeavor, especially for systems with infinite state space. With the recent development of theoretical frameworks based on formal logic, it is now possible (albeit very difficult) to both formalize and reason about an object system in the same language. This research derives from the previous research presented in [1], and represents a simplification to obtain a minimal model. The computational model of a minimal market, presented here in a declarative style, is of importance from the perspective of both market design and verification.
Keywords: formal logic; market design; financial exchanges; automated reasoning; logical frameworks; computational models