Search

In recent years, several authors have been investigating simplicial models, a model of epistemic logic based on higher-dimensional structures called simplicial complexes. In the original formulation, simplicial models were always assumed to be pure, meaning that all worlds have the same dimension. This is equivalent to the standard S5n semantics of epistemic logic, based on Kripke models. By removing the assumption that models must be pure, we can go beyond the usual Kripke semantics and study epistemic logics where the number of agents participating in a world can vary. This approach has been developed in a number of papers, with applications in fault-tolerant distributed computing where processes may crash during the execution of a system. A difficulty that arises is that subtle design choices in the definition of impure simplicial models can result in different axioms of the resulting logic. In this paper, we classify those design choices systematically, and axiomatize the corresponding logics. We illustrate them via distributed computing examples of synchronous systems where processes may crash.

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 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.

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 a many-sorted modal logic for reasoning about knowledge in multi-agent systems. Our logic introduces a clear distinction between participating agents and the environment. This allows to express local properties of agents and global properties of worlds in a uniform way, as well as to talk about the presence or absence of agents in a world. The logic subsumes the standard epistemic logic and is a conservative extension of it. The semantics is given in chromatic hypergraphs, a generalization of chromatic simplicial complexes, which were recently used to model knowledge in distributed systems. We show that the logic is sound and complete with respect to the intended semantics. We also show a further connection of chromatic hypergraphs with neighborhood frames.

In this work, we explore links between natural homology and persistent homology for the classification of directed spaces. The former is an algebraic invariant of directed spaces, a semantic model of concurrent programs. The latter was developed in the context of topological data analysis, in which topological properties of point-cloud data sets are extracted while eliminating noise. In both approaches, the evolution homological properties are tracked through a sequence of inclusions of usual topological spaces. Exploiting this similarity, we show that natural homology may be considered a persistence object, and may be calculated as a colimit of uni-dimensional persistent homologies along traces. Finally, we suggest further links and avenues of future work in this direction.

In recent years, a new class of models for multi-agent epistemic logic has emerged, based on simplicial complexes. Since then, many variants of these simplicial models have been investigated, giving rise to different logics and axiomatizations. In this paper, we present a further generalization, where a group of agents may distinguish two worlds, even though each individual agent in the group is unable to distinguish them. For that purpose, we generalize beyond simplicial complexes and consider instead simplicial sets. By doing so, we define a new semantics for epistemic logic with distributed knowledge. As it turns out, these models are the geometric counterpart of a generalization of Kripke models, called "pseudo-models". We identify various interesting sub-classes of these models, encompassing all previously studied variants of simplicial models; and give a sound and complete axiomatization for each of them.

We develop a homology theory for directed spaces, based on the semi-abelian category of (non-unital) associative algebras. The major ingredient is a simplicial algebra constructed from convolution algebras of certain trace categories of a directed space. We show that this directed homology HA is invariant under directed homeomorphisms, and is computable as a simple algebra quotient for $HA_1$. We also show that the algebra structure for $HA_n$, $n\geq 2$ is degenerate, through a Eckmann-Hilton argument. We hint at some relationships between this homology theory and natural homology, another homology theory designed for directed spaces. Finally we pave the way towards some interesting long exact sequences.

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., Comment: Final submission IJCAI 2022

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.

Effective inclusion of physics-based knowledge into deep neural network models of dynamical systems can greatly improve data efficiency and generalization. Such a-priori knowledge might arise from physical principles (e.g., conservation laws) or from the system's design (e.g., the Jacobian matrix of a robot), even if large portions of the system dynamics remain unknown. We develop a framework to learn dynamics models from trajectory data while incorporating a-priori system knowledge as inductive bias. More specifically, the proposed framework uses physics-based side information to inform the structure of the neural network itself, and to place constraints on the values of the outputs and the internal states of the model. It represents the system's vector field as a composition of known and unknown functions, the latter of which are parametrized by neural networks. The physics-informed constraints are enforced via the augmented Lagrangian method during the model's training. We experimentally demonstrate the benefits of the proposed approach on a variety of dynamical systems -- including a benchmark suite of robotics environments featuring large state spaces, non-linear dynamics, external forces, contact forces, and control inputs. By exploiting a-priori system knowledge during training, the proposed approach learns to predict the system dynamics two orders of magnitude more accurately than a baseline approach that does not include prior knowledge, given the same training dataset., Comment: Published as a conference paper at L4DC 2022

The standard semantics of multi-agent epistemic logic S5 is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that we formalized as pure simplicial models in a previous work (Information and Computation, 2021). Here we extend the theory to encompass simplicial models that are not necessarily pure. The corresponding class of Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. Such models correspond to the epistemic logic KB4 . Impure simplicial models arise in situations where two possible worlds may not have the same set of agents. We illustrate it with distributed computing examples of synchronous systems where processes may crash.

This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks.

We study learning based controllers as a replacement for model predictive controllers (MPC) for the control of autonomous vehicles. We concentrate for the experiments on the simple yet representative bicycle model. We compare training by supervised learning and by reinforcement learning. We also discuss the neural net architectures so as to obtain small nets with the best performances. This work aims at producing controllers that can both be embedded on real-time platforms and amenable to verification by formal methods techniques.

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 consider the problem of under and over-approximating the image of general vector-valued functions over bounded sets, and apply the proposed solution to the estimation of reachable sets of uncertain non-linear discrete-time dynamical systems. Such a combination of under and over-approximations is very valuable for the verification of properties of embedded and cyber-physical controlled systems. Over-approximations prove properties correct, while under-approximations can be used for falsification. Coupled, they provide a measure of the conservatism of the analysis. This work introduces a general framework relying on computations of robust ranges of vector-valued functions. This framework allows us to extend for under-approximation many precision refinements that are classically used for over-approximations, such as affine approximations, Taylor models, quadrature formulae and preconditioning methods. We end by evaluating the efficiency and precision of our approach, focusing on the application to the analysis of discrete-time dynamical systems with inputs and disturbances, on different examples from the literature., Comment: 8 pages, 4 figures

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, $\texttt{DaTaReach}$ and $\texttt{DaTaControl}$, to over-approximate the reachable set and design control signals for the system on the fly. $\texttt{DaTaReach}$ constructs a differential inclusion that contains the unknown dynamics. Then, in a discrete-time setting, it over-approximates 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 $\texttt{DaTaReach}$. $\texttt{DaTaControl}$ enables convex-optimization-based control using the computed over-approximation and the receding-horizon control framework. Besides, $\texttt{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 $\texttt{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., Comment: Extended version of the initial submission to IEEE TAC. arXiv admin note: substantial text overlap with arXiv:2009.12733

We investigate the problem of data-driven, on-the-fly control of systems with unknown nonlinear dynamics where data from only a single finite-horizon trajectory and possibly side information on the dynamics are available. Such side information may include knowledge of the regularity of the dynamics, monotonicity of the states, or decoupling in the dynamics between the states. Specifically, we develop two algorithms, $\texttt{DaTaReach}$ and $\texttt{DaTaControl}$, to over-approximate the reachable set and design control signals for the system on the fly. $\texttt{DaTaReach}$ constructs a differential inclusion that contains the unknown vector field. Then, it computes an over-approximation of the reachable set based on interval Taylor-based methods applied to systems with dynamics described as differential inclusions. $\texttt{DaTaControl}$ enables convex-optimization-based, near-optimal control using the computed over-approximation and the receding-horizon control framework. We provide a bound on its suboptimality and show that more data and side information enable $\texttt{DaTaControl}$ to achieve tighter suboptimality bounds. Finally, we demonstrate the efficacy of $\texttt{DaTaControl}$ over existing approaches on the problems of controlling a unicycle and quadrotor systems., Comment: Extended version of the final submission to the American Control Conference (ACC) 2021

We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.

Simplicial complexes are a versatile and convenient paradigm on which to build all the tools and techniques of the logic of knowledge, on the assumption that initial epistemic models can be described in a distributed fashion. Thus, we can define: knowledge, belief, bisimulation, the group notions of mutual, distributed and common knowledge, and also dynamics in the shape of simplicial action models. We give a survey on how to interpret all such notions on simplicial complexes, building upon the foundations laid in prior work by Goubault and others.

In this paper we study the solvability of the equality negation task in a simple wait-free model where processes communicate by reading and writing shared variables or exchanging messages. In this task, two processes start with a private input value in the set {0,1,2}, and after communicating, each one must decide a binary output value, so that the outputs of the processes are the same if and only if the input values of the processes are different. This task is already known to be unsolvable; our goal here is to prove this result using the dynamic epistemic logic (DEL) approach introduced by Goubault, Ledent and Rajsbaum in GandALF 2018. We show that in fact, there is no epistemic logic formula that explains why the task is unsolvable. We fix this issue by extending the language of our DEL framework, which allows us to construct such a formula, and discuss its utility.

A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have non-positive curvature, a notion that we introduce and study here for precubical sets, and can be thought of as an algebraic analogue of the well-known one for metric spaces. Using this it, as well as categorical rewriting techniques, we are then able to show that directed and non-directed homotopy coincide for directed paths in these precubical sets. Finally, we study the geometric realization of precubical sets in metric spaces, to show that our conditions on precubical sets actually coincide with those for metric spaces. Since the category of metric spaces is not cocomplete, we are lead to work with generalized metric spaces and study some of their properties.

It has been observed that the very important motion planning problem of robotics mathematically speaking boils down to the problem of finding a section to the path-space fibration, raising the notion of topological complexity, as introduced by M. Farber. The above notion fits the motion planning problem of robotics when there are no constraints on the actual control that can be applied to the physical apparatus. In many applications, however, a physical apparatus may have constrained controls, leading to constraints on its potential future dynamics. In this paper we adapt the notion of topological complexity to the case of directed topological spaces, which encompass such controlled systems, and also systems which appear in concurrency theory. We study its first properties, make calculations for some interesting classes of spaces, and show applications to a form of directed homotopy equivalence.

Directed topology was introduced as a model of concurrent programs, where the flow of time is described by distinguishing certain paths in the topological space representing such a program. Algebraic invariants which respect this directedness have been introduced to classify directed spaces. In this work we study the properties of such invariants with respect to the reversal of the flow of time in directed spaces. Known invariants, natural homotopy and homology, have been shown to be unchanged under this time-reversal. We show that these can be equipped with additional algebraic structure witnessing this reversal. Specifically, when applied to a directed space and to its reversal, we show that these refined invariants yield dual objects. We further refine natural homotopy by introducing a notion of relative directed homotopy and showing the existence of a long exact sequence of natural homotopy systems.

The usual epistemic model S5n for a multi-agent system is based on a Kripke frame, which is a graph whose edges are labeled with agents that do not distinguish between two states. We propose to uncover the higher dimensional information implicit in this structure, by considering a dual, simplicial complex model. We use dynamic epistemic logic (DEL) to study how an epistemic simplicial complex model changes after a set of agents communicate with each other. We concentrate on an action model that represents the so called immediate snapshot communication patterns of asynchronous agents, because it is central to distributed computability (but our setting works for other communication patterns). There are topological invariants preserved from the initial epistemic complex to the one after the action model is applied, which determine the knowledge that the agents gain after communication. Finally, we describe how a distributed task specification can be modeled as a DEL action model, and show that the topological invariants determine whether the task is solvable. We thus provide a bridge between DEL and the topological theory of distributed computability, which studies task solvability in a shared memory or message passing architecture., Comment: In Proceedings GandALF 2018, arXiv:1809.02416

This short note introduces a notion of directed homotopy equivalence and of "directed" topological complexity (which elaborates on the notion that can be found in e.g. Farber's book) which have a number of desirable joint properties. In particular, being dihomotopically equivalent implies having bisimilar natural homologies (defined in Dubut et al. 2015). Also, under mild conditions, directed topological complexity is an invariant of our directed homotopy equivalence and having a directed topological complexity equal to one is (under these conditions) equivalent to being dihomotopy equivalent to a point (i.e., to being "dicontractible", as in the undirected case). It still remains to compare this notion with the notion introduced in Dubut et al. 2016, which has lots of good properties as well. For now, it seems that for reasonable spaces, this new proposal of directed homotopy equivalence identifies more spaces than the one of Dubut et al. 2016., Comment: Some typos corrected (version 2)

We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the theorem prover Keymaera X to discharge some of the generated proof obligations., Comment: In Proceedings FVAV 2017, arXiv:1709.02126

The computability power of a distributed computing model is determined by the communication media available to the processes, the timing assumptions about processes and communication, and the nature of failures that processes can suffer. In a companion paper we showed how dynamic epistemic logic can be used to give a formal semantics to a given distributed computing model, to capture precisely the knowledge needed to solve a distributed task, such as consensus. Furthermore, by moving to a dual model of epistemic logic defined by simplicial complexes, topological invariants are exposed, which determine task solvability. In this paper we show how to extend the setting above to include in the knowledge of the processes, knowledge about the model of computation itself. The extension describes the knowledge processes gain about the current execution, in problems where processes have no input values at all., Comment: arXiv admin note: text overlap with arXiv:1703.11005

The usual epistemic S5 model for multi-agent systems is a Kripke graph, whose edges are labeled with the agents that do not distinguish between two states. We propose to uncover the higher dimensional information implicit in the Kripke graph, by using as a model its dual, a chromatic simplicial complex. For each state of the Kripke model there is a facet in the complex, with one vertex per agent. If an edge (u,v) is labeled with a set of agents S, the facets corresponding to u and v intersect in a simplex consisting of one vertex for each agent of S. Then we use dynamic epistemic logic to study how the simplicial complex epistemic model changes after the agents communicate with each other. We show that there are topological invariants preserved from the initial epistemic complex to the epistemic complex after an action model is applied, that depend on how reliable the communication is. In turn these topological properties determine the knowledge that the agents may gain after the communication happens.

This paper addresses the problem of evaluating a subset of the range of a vector-valued function. It is based on a work by Gold- sztejn and Jaulin which provides methods based on interval analysis to address this problem when the dimension of the domain and co-domain of the function are equal. This paper extends this result to vector-valued functions with domain and co-domain of different dimensions. This ex- tension requires the knowledge of the rank of the Jacobian function on the whole domain. This leads to the sub-problem of extracting an in- terval sub-matrix of maximum rank from a given interval matrix. Three different techniques leading to approximate solutions of this extraction are proposed and compared., Comment: 26 pages, 17 figures

A desirable property of control systems is to be robust to inputs, that is small perturbations of the inputs of a system will cause only small perturbations on its outputs. But it is not clear whether this property is maintained at the implementation level, when two close inputs can lead to very different execution paths. The problem becomes particularly crucial when considering finite precision implementations, where any elementary computation can be affected by a small error. In this context, almost every test is potentially unstable, that is, for a given input, the computed (finite precision) path may differ from the ideal (same computation in real numbers) path. Still, state-of-the-art error analyses do not consider this possibility and rely on the stable test hypothesis, that control flows are identical. If there is a discontinuity between the treatments in the two branches, that is the conditional block is not robust to uncertainties, the error bounds can be unsound. We propose here a new abstract-interpretation based error analysis of finite precision implementations, which is sound in presence of unstable tests. It automatically bounds the discontinuity error coming from the difference between the float and real values when there is a path divergence, and introduces a new error term labeled by the test that introduced this potential discontinuity. This gives a tractable error analysis, implemented in our static analyzer FLUCTUAT: we present results on representative extracts of control programs., Comment: 16 pages, extended version of APLAS 2013 paper

State-space reduction techniques, used primarily in model-checkers, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not necessary to consider all execution paths in the interleaving semantics of a concurrent program, but rather some equivalence classes. The purpose of this paper is to describe a new algorithm to compute such equivalence classes, and a representative per class, which is based on ideas originating in algebraic topology. We introduce a geometric semantics of concurrent languages, where programs are interpreted as directed topological spaces, and study its properties in order to devise an algorithm for computing dihomotopy classes of execution paths. In particular, our algorithm is able to compute a control-flow graph for concurrent programs, possibly containing loops, which is "as reduced as possible" in the sense that it generates traces modulo equivalence. A preliminary implementation was achieved, showing promising results towards efficient methods to analyze concurrent programs, with very promising results compared to partial-order reduction techniques.

We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, generalizes the domain of linear "templates" introduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic templates, we use Shor's semi-definite relaxation to derive computable yet precise abstractions of semantic functionals, and we show that the abstract fixpoint equation can be solved accurately by coupling policy iteration and semi-definite programming. We demonstrate the interest of our approach on a series of examples (filters, integration schemes) including a degenerate one (symplectic scheme)., Comment: 32 pages, 9 figures, preliminary version appeared in ESOP (European Symposium On Programming) 2010; LMCS 8 (1:1) 2012

A wide variety of models for concurrent programs has been proposed during the past decades, each one focusing on various aspects of computations: trace equivalence, causality between events, conflicts and schedules due to resource accesses, etc. More recently, models with a geometrical flavor have been introduced, based on the notion of cubical set. These models are very rich and expressive since they can represent commutation between any bunch of events, thus generalizing the principle of true concurrency. While they seem to be very promising - because they make possible the use of techniques from algebraic topology in order to study concurrent computations - they have not yet been precisely related to the previous models, and the purpose of this paper is to fill this gap. In particular, we describe an adjunction between Petri nets and cubical sets which extends the previously known adjunction between Petri nets and asynchronous transition systems by Nielsen and Winskel.

We define and study a new abstract domain which is a fine-grained combination of zonotopes with polyhedric domains such as the interval, octagon, linear templates or polyhedron domain. While abstract transfer functions are still rather inexpensive and accurate even for interpreting non-linear computations, we are able to also interpret tests (i.e. intersections) efficiently. This fixes a known drawback of zonotopic methods, as used for reachability analysis for hybrid sys- tems as well as for invariant generation in abstract interpretation: intersection of zonotopes are not always zonotopes, and there is not even a best zonotopic over-approximation of the intersection. We describe some examples and an im- plementation of our method in the APRON library, and discuss some further in- teresting combinations of zonotopes with non-linear or non-convex domains such as quadratic templates and maxplus polyhedra.

We develop a tropical analogue of the classical double description method allowing one to compute an internal representation (in terms of vertices) of a polyhedron defined externally (by inequalities). The heart of the tropical algorithm is a characterization of the extreme points of a polyhedron in terms of a system of constraints which define it. We show that checking the extremality of a point reduces to checking whether there is only one minimal strongly connected component in an hypergraph. The latter problem can be solved in almost linear time, which allows us to eliminate quickly redundant generators. We report extensive tests (including benchmarks from an application to static analysis) showing that the method outperforms experimentally the previous ones by orders of magnitude. The present tools also lead to worst case bounds which improve the ones provided by previous methods., Comment: 12 pages, prepared for the Proceedings of the Symposium on Theoretical Aspects of Computer Science, 2010, Nancy, France

This article formalizes an abstraction of input/output relations, based on parameterized zonotopes, which we call affine sets. We describe the abstract transfer functions and prove their correctness, which allows the generation of accurate numerical invariants. Other applications range from compositional reasoning to proofs of user-defined complex invariants and test case generation., Comment: 23 pages

We establish a characterization of the vertices of a tropical polyhedron defined as the intersection of finitely many half-spaces. We show that a point is a vertex if, and only if, a directed hypergraph, constructed from the subdifferentials of the active constraints at this point, admits a unique strongly connected component that is maximal with respect to the reachability relation (all the other strongly connected components have access to it). This property can be checked in almost linear-time. This allows us to develop a tropical analogue of the classical double description method, which computes a minimal internal representation (in terms of vertices) of a polyhedron defined externally (by half-spaces or hyperplanes). We provide theoretical worst case complexity bounds and report extensive experimental tests performed using the library TPLib, showing that this method outperforms the other existing approaches., Comment: 29 pages (A4), 10 figures, 1 table; v2: Improved algorithm in section 5 (using directed hypergraphs), detailed appendix; v3: major revision of the article (adding tropical hyperplanes, alternative method by arrangements, etc); v4: minor revision

The state space of a machine admits the structure of time. For example, the geometric realization of a precubical set, a generalization of an unlabeled asynchronous transition system, admits a "local preorder" encoding control flow. In the case where time does not loop, the "locally preordered" state space splits into causally distinct components. The set of such components often gives a computable invariant of machine behavior. In the general case, no such meaningful partition could exist. However, as we show in this note, the locally preordered geometric realization of a precubical set admits a "locally monotone" covering from a state space in which time does not loop. Thus we hope to extend geometric techniques in static program analysis to looping processes., Comment: 14 pages, 2 figures, results partially presented at ATMCS III 2008; deleted false Lem 2.2; corrected proof of Lem 3.7; deleted wrong formula for \lambda(\theta,d_{-1}\theta) on p10; deleted Prop 2.20 and all mention of op-fibration (confusing); generalized Lem 3.6; weakened claim of Eg. 2.2 b/c homotopies need not lift; added defs and fixed typos throughout; main results unchanged

We completely describe a new domain for abstract interpretation of numerical programs. Fixpoint iteration in this domain is proved to converge to finite precise invariants for (at least) the class of stable linear recursive filters of any order. Good evidence shows it behaves well also for some non-linear schemes. The result, and the structure of the domain, rely on an interesting interplay between order and topology., Comment: 12 pages in two-column style

The problem of computing the smallest fixed point of an order-preserving map arises in the study of zero-sum positive stochastic games. It also arises in static analysis of programs by abstract interpretation. In this context, the discount rate may be negative. We characterize the minimality of a fixed point in terms of the nonlinear spectral radius of a certain semidifferential. We apply this characterization to design a policy iteration algorithm, which applies to the case of finite state and action spaces. The algorithm returns a locally minimal fixed point, which turns out to be globally minimal when the discount rate is nonnegative., Comment: 26 pages, 3 figures. We add new results, improvements and two examples of positive stochastic games. Note that an initial version of the paper has appeared in the proceedings of the Eighteenth International Symposium on Mathematical Theory of Networks and Systems (MTNS2008), Blacksburg, Virginia, July 2008

A local po-space is a gluing of topological spaces which are equipped with a closed partial ordering representing the time flow. They are used as a formalization of higher dimensional automata which model concurrent systems in computer science. It is known that there are two distinct notions of deformation of higher dimensional automata, ``spatial'' and ``temporal'', leaving invariant computer scientific properties like presence or absence of deadlocks. Unfortunately, the formalization of these notions is still unknown in the general case of local po-spaces. We introduce here a particular kind of local po-space, the ``globular CW-complexes'', for which we formalize these notions of deformations and which are sufficient to formalize higher dimensional automata. After localizing the category of globular CW-complexes by spatial and temporal deformations, we get a category (the category of dihomotopy types) whose objects up to isomorphism represent exactly the higher dimensional automata up to deformation. Thus globular CW-complexes provide a rigorous mathematical foundation to study from an algebraic topology point of view higher dimensional automata and concurrent computations., Comment: 43 pages ; LaTeX2e ; 12 postscript figures ; final version to appear in Homology, Homotopy and Applications