-
Simplicial Models for the Epistemic Logic of Faulty Agents
Authors:
Eric Goubault,
Roman Kniazev,
Jeremy Ledent,
Sergio Rajsbaum
Abstract:
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 remov…
▽ More
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.
△ Less
Submitted 14 November, 2023; v1 submitted 2 November, 2023;
originally announced November 2023.
-
Guaranteed approximations of arbitrarily quantified reachability problems
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
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 demonstrat…
▽ More
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.
△ Less
Submitted 14 September, 2023;
originally announced September 2023.
-
Estimating the Coverage Measure and the Area Explored by a Line-Sweep Sensor on the Plane
Authors:
Maria Costa Vianna,
Eric Goubault,
Luc Jaulin,
Sylvie Putot
Abstract:
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 map**, surveillance, and coverage optimization. The proposed method leverages the concept of coverage measure of the environment and its relation to the to…
▽ More
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 map**, 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.
△ Less
Submitted 7 September, 2023;
originally announced September 2023.
-
A many-sorted epistemic logic for chromatic hypergraphs
Authors:
Eric Goubault,
Roman Kniazev,
Jérémy Ledent
Abstract:
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…
▽ More
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.
△ Less
Submitted 1 August, 2023;
originally announced August 2023.
-
Persistent homology of directed spaces
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos
Abstract:
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 appro…
▽ More
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.
△ Less
Submitted 3 May, 2024; v1 submitted 5 May, 2023;
originally announced May 2023.
-
Semi-simplicial Set Models for Distributed Knowledge
Authors:
Eric Goubault,
Roman Kniazev,
Jérémy Ledent,
Sergio Rajsbaum
Abstract:
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…
▽ More
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.
△ Less
Submitted 26 April, 2023; v1 submitted 27 March, 2023;
originally announced March 2023.
-
A semi-abelian approach to directed homology
Authors:
Eric Goubault
Abstract:
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…
▽ More
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.
△ Less
Submitted 28 April, 2023; v1 submitted 16 January, 2023;
originally announced January 2023.
-
Taylor-Lagrange Neural Ordinary Differential Equations: Toward Fast Training and Evaluation of Neural ODEs
Authors:
Franck Djeumou,
Cyrus Neary,
Eric Goubault,
Sylvie Putot,
Ufuk Topcu
Abstract:
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 expensi…
▽ More
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.
△ Less
Submitted 28 December, 2022; v1 submitted 14 January, 2022;
originally announced January 2022.
-
Solving N-player dynamic routing games with congestion: a mean field approach
Authors:
Theophile Cabannes,
Mathieu Lauriere,
Julien Perolat,
Raphael Marinier,
Sertan Girgin,
Sarah Perrin,
Olivier Pietquin,
Alexandre M. Bayen,
Eric Goubault,
Romuald Elie
Abstract:
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 rep…
▽ More
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.
△ Less
Submitted 27 October, 2021; v1 submitted 22 October, 2021;
originally announced October 2021.
-
Neural Networks with Physics-Informed Architectures and Constraints for Dynamical Systems Modeling
Authors:
Franck Djeumou,
Cyrus Neary,
Eric Goubault,
Sylvie Putot,
Ufuk Topcu
Abstract:
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 l…
▽ More
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.
△ Less
Submitted 12 December, 2022; v1 submitted 13 September, 2021;
originally announced September 2021.
-
A Simplicial Model for $KB4_n$: Epistemic Logic with Agents that May Die
Authors:
Éric Goubault,
Jérémy Ledent,
Sergio Rajsbaum
Abstract:
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 encomp…
▽ More
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.
△ Less
Submitted 9 November, 2022; v1 submitted 23 August, 2021;
originally announced August 2021.
-
Static analysis of ReLU neural networks with tropical polyhedra
Authors:
Eric Goubault,
Sébastien Palumby,
Sylvie Putot,
Louis Rustenholz,
Sriram Sankaranarayanan
Abstract:
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 derivat…
▽ More
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 co** 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.
△ Less
Submitted 23 August, 2021; v1 submitted 30 July, 2021;
originally announced August 2021.
-
Neural Network Based Model Predictive Control for an Autonomous Vehicle
Authors:
Maria Luiza Costa Vianna,
Eric Goubault,
Sylvie Putot
Abstract:
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 a…
▽ More
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.
△ Less
Submitted 30 July, 2021;
originally announced July 2021.
-
Reinforcement Learning with Formal Performance Metrics for Quadcopter Attitude Control under Non-nominal Contexts
Authors:
Nicola Bernini,
Mikhail Bessa,
Rémi Delmas,
Arthur Gold,
Eric Goubault,
Romain Pennec,
Sylvie Putot,
François Sillion
Abstract:
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 temp…
▽ More
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.
△ Less
Submitted 27 July, 2021;
originally announced July 2021.
-
Algebraic coherent confluence and higher globular Kleene algebras
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos,
Georg Struth
Abstract:
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 ins…
▽ More
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.
△ Less
Submitted 24 November, 2022; v1 submitted 29 June, 2020;
originally announced June 2020.
-
Knowledge and simplicial complexes
Authors:
Hans van Ditmarsch,
Eric Goubault,
Jeremy Ledent,
Sergio Rajsbaum
Abstract:
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 model…
▽ More
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.
△ Less
Submitted 20 February, 2020;
originally announced February 2020.
-
A dynamic epistemic logic analysis of the equality negation task
Authors:
Eric Goubault,
Marijana Lazic,
Jeremy Ledent,
Sergio Rajsbaum
Abstract:
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…
▽ More
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.
△ Less
Submitted 7 September, 2019;
originally announced September 2019.
-
Directed Homotopy in Non-Positively Curved Spaces
Authors:
Eric Goubault,
Samuel Mimram
Abstract:
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-pos…
▽ More
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.
△ Less
Submitted 10 July, 2020; v1 submitted 19 August, 2019;
originally announced August 2019.
-
Time-reversal homotopical properties of concurrent systems
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos
Abstract:
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…
▽ More
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.
△ Less
Submitted 12 December, 2018;
originally announced December 2018.
-
A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability
Authors:
Éric Goubault,
Jérémy Ledent,
Sergio Rajsbaum
Abstract:
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 mode…
▽ More
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.
△ Less
Submitted 9 September, 2018;
originally announced September 2018.
-
On directed homotopy equivalences and a notion of directed topological complexity
Authors:
Eric Goubault
Abstract:
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 topo…
▽ More
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.
△ Less
Submitted 9 October, 2017; v1 submitted 17 September, 2017;
originally announced September 2017.
-
Formal Verification of Station Kee** Maneuvers for a Planar Autonomous Hybrid System
Authors:
Benjamin Martin,
Khalil Ghorbal,
Eric Goubault,
Sylvie Putot
Abstract:
We formally verify a hybrid control law designed to perform a station kee** 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 i…
▽ More
We formally verify a hybrid control law designed to perform a station kee** 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.
△ Less
Submitted 8 September, 2017;
originally announced September 2017.
-
Models of fault-tolerant distributed computation via dynamic epistemic logic
Authors:
Eric Goubault,
Sergio Rajsbaum
Abstract:
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…
▽ More
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.
△ Less
Submitted 25 April, 2017;
originally announced April 2017.
-
A simplicial complex model of dynamic epistemic logic for fault-tolerant distributed computing
Authors:
Eric Goubault,
Sergio Rajsbaum
Abstract:
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.…
▽ More
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.
△ Less
Submitted 4 April, 2017; v1 submitted 31 March, 2017;
originally announced March 2017.
-
Robustness analysis of finite precision implementations
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
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 i…
▽ More
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.
△ Less
Submitted 16 September, 2013;
originally announced September 2013.
-
Trace Spaces: an Efficient New Technique for State-Space Reduction
Authors:
Lisbeth Fajstrup,
Eric Goubault,
Emmanuel Haucourt,
Samuel Mimram,
Martin Raussen
Abstract:
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…
▽ More
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.
△ Less
Submitted 2 April, 2012;
originally announced April 2012.
-
Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
Authors:
Assalé Adjé,
Stéphane Gaubert,
Eric Goubault
Abstract:
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 semant…
▽ More
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).
△ Less
Submitted 18 January, 2012; v1 submitted 22 November, 2011;
originally announced November 2011.
-
Formal Relationships Between Geometrical and Classical Models for Concurrency
Authors:
Eric Goubault,
Samuel Mimram
Abstract:
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…
▽ More
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.
△ Less
Submitted 11 June, 2012; v1 submitted 16 April, 2010;
originally announced April 2010.
-
A Logical Product Approach to Zonotope Intersection
Authors:
Khalil Ghorbal,
Eric Goubault,
Sylvie Putot
Abstract:
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 d…
▽ More
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.
△ Less
Submitted 26 March, 2010; v1 submitted 10 February, 2010;
originally announced February 2010.
-
The tropical double description method
Authors:
Xavier Allamigeon,
Stephane Gaubert,
Eric Goubault
Abstract:
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 poin…
▽ More
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.
△ Less
Submitted 3 February, 2010; v1 submitted 22 January, 2010;
originally announced January 2010.
-
A zonotopic framework for functional abstractions
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
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.
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.
△ Less
Submitted 9 October, 2009;
originally announced October 2009.
-
Perturbed affine arithmetic for invariant computation in numerical program analysis
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
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 betw…
▽ More
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.
△ Less
Submitted 18 July, 2008;
originally announced July 2008.
