The usual semantics of multi-agent epistemic logic is based on Kripke models, defined in terms of binary relations on a set of possible worlds. Recently, there has been a growing interest in using simplicial complexes rather than graphs, as models for multi-agent epistemic logic. This approach uses agents' views as the fundamental object instead of worlds. A set of views by different agents about a world forms a simplex, and a set of simplexes defines a simplicial complex, that can serve as a model for multi-agent epistemic logic. This new approach reveals topological information that is implicit in Kripke models, because the binary indistinguishability relations are more clearly seen as n-ary relations in the simplicial complex. This paper, written for an economics audience, introduces simplicial models to non-experts and connects distributed computing, epistemic logic and topology. Our focus is on distributed knowledge and its fixed point, common distributed knowledge. These concepts arise when considering the knowledge that a group of agents would acquire, if they could communicate their local knowledge perfectly. While common knowledge has been shown to be related to consensus, we illustrate how distributed knowledge is related to a task weaker to consensus, called majority consensus. We describe three models of communication, some well-known (immediate snapshot), and others less studied (related to broadcast and test-and-set). When majority consensus is solvable, we describe the distributed knowledge that is used to solve it. When it is not solvable, we present a logical obstruction, a formula that should always be known according to the task specification, but which the players cannot know.

Quantitative verification of neural networks requires reasoning about probabilities under substantial uncertainty in both input distributions and their dependence structure. In realistic settings, this information is often only partially specified, and assuming precise probabilistic models can lead to unreliable results. We propose a sound framework for quantitative verification under imprecise probabilistic information, combining interval belief structures to represent marginal uncertainty with imprecise copulas to model uncertain dependence. We develop a propagation method for imprecisely coupled interval belief structures through feed-forward neural networks. Using mixed imprecise copula volumes, we derive sound push-forward constructions through affine transformations and activation functions. The resulting output can provide guaranteed lower and upper bounds on probabilistic safety properties, valid for all probability models compatible with the specified imprecise inputs.

We introduce abelian framed bicategories, which are particular framed bicategories that are locally abelian, and show that they are suitable for developing homology and cohomology theories for directed structures. This means in particular that similar exact sequences as the relative homology and Mayer-Vietoris long exact sequences can be shown to hold. Also, for closed monoidal abelian framed bicategories, Künneth theorem holds as well. Finally, we prove embedding theorems similar to the Gabriel and Freyd-Mitchell theorems, for particular abelian framed bicategories, allowing to see those as bicategories of bimodules over algebras. This naturally links to the original motivation of this work, which was to generalize directed homology developed in the abelian framed bicategory of bimodules over (path) algebras.

We propose an approach for computing inner and outer-approximations of the sets of values that satisfy constraints expressed as arbitrarily quantified formulas. Such formulas arise for example when specifying important problems in control such as robustness, motion planning and controller comparison. We propose an interval-based method which allows for tight but tractable approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation. Finally, we develop higher-order methods, particularly tractable order one methods which provide even tighter results.

In this article, we show that the now classical protocol complex approach to distributed task solvability of Herlihy et al. can be understood in standard categorical terms. First, protocol complexes are functors, from chromatic (semi-) simplicial sets to chromatic simplicial sets, that naturally give rise to algebras. These algebras describe the next state operator for the corresponding distributed systems. This is constructed for semi-synchronous distributed systems with general patterns of communication for which we show that these functors are always Yoneda extensions of simpler functors, implying a number of interesting properties. Furthermore, for these protocol complex functors, we prove the existence of a free algebra on any initial chromatic simplicial complex, modeling iterated protocol complexes. Under this categorical formalization, protocol complexes are seen as transition systems, where states are structured as chromatic simplicial sets. We exploit the epistemic interpretation of chromatic simplicial sets and the underlying transition system (or algebra) structure to introduce a temporal-epistemic logic and its semantics on all free algebras on chromatic simplicial sets. We end up by giving hints on how to extend this framework to more general dynamic network graphs and state-dependent protocols, and give example in fault-tolerant distributed systems and mobile robotics.

In probabilistic neural network verification, a well-chosen representation of input uncertainty ensures that theoretical analyses accurately reflect real input perturbations. A recent approach based on probability boxes (p-boxes) [9] is introduced in [10] and unifies setbased and probabilistic information on the inputs. The method allows for obtaining guaranteed probabilistic bounds for property satisfaction on feedforward ReLU networks. However, it suffers from conservatism due to employing set-based propagation methods. In this work we investigate how to sample from p-boxes without loss of information. Based on that, we develop a sampling-based approach for propagating p-boxes through feedforward ReLU networks. We prove that with dense enough coverings of the input p-boxes, the propagated samples accurately represent the output uncertainty and provide error bounds. Additionally, we show how to create coverings for arbitrary p-boxes with various distributions. On the ACAS Xu benchmark we demonstrate that our approach is applicable in practice, both as a standalone verifier and as a way to partially assess the conservatism of the set-based approach of [10].

Split conformal prediction is a statistical method known for its finite-sample coverage guarantees, simplicity, and low computational cost. As such, it is suitable for predicting uncertainty regions in time series forecasting. However, in the context of multi-horizon forecasting, the current literature lacks conformal methods that produce efficient intervals and have low computational cost. Building on the foundation of split conformal prediction and one of its most prominent extensions to multi-horizon time series forecasting (CF-RNN), we introduce ConForME, a method that leverages the time dependence within time series to construct efficient multi-horizon prediction intervals with probabilistic joint coverage guarantees. We prove its validity and support our claims with experiments on both synthetic and real-world data. Across all instances, our method outperforms CF-RNN in terms of mean, min, and max interval sizes over the entire prediction horizon, achieving improvements of up to 52%. The experiments also suggest that these improvements can be further increased by extending the prediction horizon and through hyperparameter optimization.

In this note, we give a self-contained account on a construction for a directed homology theory based on modules over algebras, linking it to both persistence homology and natural homology. We study its first properties, among which some exact sequences.

We explore the reinforcement learning approach to designing controllers by extensively discussing the case of a quadcopter attitude controller. We provide all details allowing to reproduce our approach, starting with a model of the dynamics of a crazyflie 2.0 under various nominal and non-nominal conditions, including partial motor failures and wind gusts. We develop a robust form of a signal temporal logic to quantitatively evaluate the vehicle's behavior and measure the performance of controllers. The paper thoroughly describes the choices in training algorithms, neural net architecture, hyperparameters, observation space in view of the different performance metrics we have introduced. We discuss the robustness of the obtained controllers, both to partial loss of power for one rotor and to wind gusts and finish by drawing conclusions on practical controller design by reinforcement learning.

We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.

This paper presents a method for determining the area explored by a line-sweep sensor during an area-covering mission in a two-dimensional plane. Accurate knowledge of the explored area is crucial for various applications in robotics, such as mapping, surveillance, and coverage optimization. The proposed method leverages the concept of coverage measure of the environment and its relation to the topological degree in the plane, to estimate the extent of the explored region. In addition, we extend the approach to uncertain coverage measure values using interval analysis. This last contribution allows for a guaranteed characterization of the explored area, essential considering the often critical character of area-covering missions. Finally, this paper also proposes a novel algorithm for computing the topological degree in the 2-dimensional plane, for all the points inside an area of interest, which differs from existing solutions that compute the topological degree for single points. The applicability of the method is evaluated through a real-world experiment.

We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.

In this article, we develop data-driven algorithms for reachability analysis and control of systems with a priori unknown nonlinear dynamics. The resulting algorithms not only are suitable for settings with real-time requirements but also provide provable performance guarantees. To this end, they merge noisy data from only a single finite-horizon trajectory and, if available, various forms of side information. Such side information may include knowledge of the regularity of the dynamics, algebraic constraints on the states, monotonicity, or decoupling in the dynamics between the states. Specifically, we develop two algorithms, DaTaReach and DaTaControl, to overapproximate the reachable set and design control signals for the system on the fly. DaTaReach constructs a differential inclusion that contains the unknown dynamics. Then, in a discrete-time setting, it overapproximates the reachable set through interval Taylor-based methods applied to systems with dynamics described as differential inclusions. We provide a bound on the time step size that ensures the correctness and termination of DaTaReach. DaTaControl enables convex-optimization-based control using the computed overapproximation and the receding-horizon control framework. Besides, DaTaControl achieves near-optimal control and is suitable for real-time control of such systems. We establish a bound on its suboptimality and the number of primitive operations it requires to compute control values. Then, we theoretically show that DaTaControl achieves tighter suboptimality bounds with an increasing amount of data and richer side information. Finally, experiments on a unicycle, quadrotor, and aircraft systems demonstrate the efficacy of both algorithms over existing approaches.

Neural ordinary differential equations (NODEs) -- parametrizations of differential equations using neural networks -- have shown tremendous promise in learning models of unknown continuous-time dynamical systems from data. However, every forward evaluation of a NODE requires numerical integration of the neural network used to capture the system dynamics, making their training prohibitively expensive. Existing works rely on off-the-shelf adaptive step-size numerical integration schemes, which often require an excessive number of evaluations of the underlying dynamics network to obtain sufficient accuracy for training. By contrast, we accelerate the evaluation and the training of NODEs by proposing a data-driven approach to their numerical integration. The proposed Taylor-Lagrange NODEs (TL-NODEs) use a fixed-order Taylor expansion for numerical integration, while also learning to estimate the expansion's approximation error. As a result, the proposed approach achieves the same accuracy as adaptive step-size schemes while employing only low-order Taylor expansions, thus greatly reducing the computational cost necessary to integrate the NODE. A suite of numerical experiments, including modeling dynamical systems, image classification, and density estimation, demonstrate that TL-NODEs can be trained more than an order of magnitude faster than state-of-the-art approaches, without any loss in performance.

We present a unified approach, implemented in the RINO tool, for the computation of inner and outer-approximations of reachable sets of discrete-time and continuous-time dynamical systems, possibly controlled by neural networks with differentiable activation functions. RINO combines a zonotopic set representation with generalized mean-value AE extensions to compute under and over-approximations of the robust range of differentiable functions, and applies these techniques to the particular case of learning-enabled dynamical systems. The AE extensions require an efficient and accurate evaluation of the function and its Jacobian with respect to the inputs and initial conditions. For continuous-time systems, possibly controlled by neural networks, the function to evaluate is the solution of the dynamical system. It is over-approximated in RINO using Taylor methods in time coupled with a set-based evaluation with zonotopes. We demonstrate the good performances of RINO compared to state-of-the art tools Verisig 2.0 and ReachNN* on a set of classical benchmark examples of neural network controlled closed loop systems. For generally comparable precision to Verisig 2.0 and higher precision than ReachNN*, RINO is always at least one order of magnitude faster, while also computing the more involved inner-approximations that the other tools do not compute.

This letter presents an approach to over-approximate the reachable set of states of a system whose uncertainties are arbitrarily time-varying. Most approaches generally assume piecewise continuity or sometimes Riemann-integrability of the uncertainties. In this letter we go one step further, only assuming Lebesgue measurability, which is the weakest meaningful hypothesis. We develop our new technique, based on a decomposition of components as a difference of positive functions, for separable systems, a generalization of control-affine systems. We compare the over-approximation produced by our method with the ones obtained using the tools Flow* and CORA on simple examples, and show that correct outer-approximations of the reachable sets are computable with a high degree of precision even for these general forms of uncertainties.

The recent emergence of navigational tools has changed traffic patterns and has now enabled new types of congestion-aware routing control like dynamic road pricing. Using the fundamental diagram of traffic flows - applied in macroscopic and mesoscopic traffic modeling - the article introduces a new N-player dynamic routing game with explicit congestion dynamics. The model is well-posed and can reproduce heterogeneous departure times and congestion spill back phenomena. However, as Nash equilibrium computations are PPAD-complete, solving the game becomes intractable for large but realistic numbers of vehicles N. Therefore, the corresponding mean field game is also introduced. Experiments were performed on several classical benchmark networks of the traffic community: the Pigou, Braess, and Sioux Falls networks with heterogeneous origin, destination and departure time tuples. The Pigou and the Braess examples reveal that the mean field approximation is generally very accurate and computationally efficient as soon as the number of vehicles exceeds a few dozen. On the Sioux Falls network (76 links, 100 time steps), this approach enables learning traffic dynamics with more than 14,000 vehicles.

Full coverage of an area of interest is a common task for a robot in the underwater environment. Estimating the area explored by the robot is indeed essential for determining if path-planning algorithms lead to complete coverage. In this work, we propose a method for estimating the area explored by a Side-Scan Sonar. The proposed method is able to determine how many times each portion of the space has been sensed by the sonar using a novel approach based on the topological properties of the environment that has been scanned, and more precisely on an estimation of certain winding numbers. This property is useful for localization inside homogeneous environments, e.g. the underwater environment, and assessment for potential revisiting missions.