arXiv subjects

Omar Inverso

Publications and source records attributed to Omar Inverso.

6 recordsLinked to original sources

arXiv2026

Emergent Behaviour in Financial Markets

Some properties of so-called complex or collective systems can be observed to emerge from the interactions of elementary agents. This phenomenon, known as emergent behaviour, has long since been studied in the most diverse disciplines, with recent growing awareness from the formal methods community about the opportunity of opening up to seemingly distant disciplines with appropriate technology for computer-aided reasoning. Different peculiar elements of complexity make automated reasoning on these systems particularly challenging. We consider electronic financial markets to drive our discussion. We identify and structure the sources of complexity to tackle in order to provide computational support for the analysis of emergent phenomena. We refrain from evaluating the suitability of specific technical solutions or frameworks of preference, which would as usual require simplifying assumptions and divert from the actual phenomenon of interest. Rather, we elaborate on possible alternatives to handle some of the main technical aspects involved in automated analysis, while retaining a solid and concrete interpretation of the domain, and in doing so outline a more systematic research program for the formal specification and analysis of market mechanisms.

cs.MA↗

arXiv2026

Fundamental market design as a layer of AI-agent alignment

This paper argues that AI-agent alignment in markets should not be understood only as a property of agents, but also as a property of the interaction infrastructure in which agents act. In financial markets, this infrastructure is the market core: the rule system that determines how orders enter, interact, match, persist, and stabilize. If this fundamental interaction layer allows or rewards undesired behaviour, then higher-level alignment of agents may be insufficient. We propose to view fundamental market design as a layer of AI-agent alignment. Alongside the important work of computational economics in modelling agents, strategies, and learning, we focus on a complementary but more fundamental layer: the formal modelling of the market core itself. Market design, especially at the level of the core mechanism, can benefit from a rigour characteristic of theoretical computer science. This gives a transparent-box model of the market, whose core properties can be formally specified and reasoned about. It also lets us treat the trading venue not as a static order book, but as a computational process combining resident orders with incoming order flow, and ask which computational model, perhaps yet unknown, naturally lies at its core. This perspective is especially relevant for markets populated by adaptive or AI agents. Such agents may learn what the mechanism rewards, including speed, delay, liquidity provision, or manipulation. These behaviours are not only properties of individual agents, but may emerge from the agent-mechanism system. We therefore argue that transparent formal models of market cores can support incentive-oriented analysis and the design of mechanisms in which desirable behaviours are structurally favoured and undesirable behaviours are harder to sustain.

cs.GT↗

arXiv2023

Certification of the proximal gradient method under fixed-point arithmetic for box-constrained QP problems

In safety-critical applications that rely on the solution of an optimization problem, the certification of the optimization algorithm is of vital importance. Certification and suboptimality results are available for a wide range of optimization algorithms. However, a typical underlying assumption is that the operations performed by the algorithm are exact, i.e., that there is no numerical error during the mathematical operations, which is hardly a valid assumption in a real hardware implementation. This is particularly true in the case of fixed-point hardware, where computational inaccuracies are not uncommon. This article presents a certification procedure for the proximal gradient method for box-constrained QP problems implemented in fixed-point arithmetic. The procedure provides a method to select the minimal fractional precision required to obtain a certain suboptimality bound, indicating the maximum number of iterations of the optimization method required to obtain it. The procedure makes use of formal verification methods to provide arbitrarily tight bounds on the suboptimality guarantee. We apply the proposed certification procedure on the implementation of a non-trivial model predictive controller on 32-bit fixed-point hardware.

math.OC↗

arXiv2020

Probabilistic Analysis of Binary Sessions

We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.

cs.LO↗

arXiv2018

Towards formal models and languages for verifiable Multi-Robot Systems

Incorrect operations of a Multi-Robot System (MRS) may not only lead to unsatisfactory results, but can also cause economic losses and threats to safety. These threats may not always be apparent, since they may arise as unforeseen consequences of the interactions between elements of the system. This call for tools and techniques that can help in providing guarantees about MRSs behaviour. We think that, whenever possible, these guarantees should be backed up by formal proofs to complement traditional approaches based on testing and simulation. We believe that tailored linguistic support to specify MRSs is a major step towards this goal. In particular, reducing the gap between typical features of an MRS and the level of abstraction of the linguistic primitives would simplify both the specification of these systems and the verification of their properties. In this work, we review different agent-oriented languages and their features; we then consider a selection of case studies of interest and implement them useing the surveyed languages. We also evaluate and compare effectiveness of the proposed solution, considering, in particular, easiness of expressing non-trivial behaviour.

cs.PL↗

arXiv2014

On the Path-Width of Integer Linear Programming

We consider the feasibility problem of integer linear programming (ILP). We show that solutions of any ILP instance can be naturally represented by an FO-definable class of graphs. For each solution there may be many graphs representing it. However, one of these graphs is of path-width at most 2n, where n is the number of variables in the instance. Since FO is decidable on graphs of bounded path- width, we obtain an alternative decidability result for ILP. The technique we use underlines a common principle to prove decidability which has previously been employed for automata with auxiliary storage. We also show how this new result links to automata theory and program verification.

cs.LO↗