TY - CONF
AB - We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.
AU - Geretti, Luca
AU - Alexandre Dit Sandretto, Julien
AU - Althoff, Matthias
AU - Benet, Luis
AU - Chapoutot, Alexandre
AU - Chen, Xin
AU - Collins, Pieter
AU - Forets, Marcelo
AU - Freire, Daniel
AU - Immler, Fabian
AU - Kochdumper, Niklas
AU - Sanders, David
AU - Schilling, Christian
ID - 8571
T2 - EPiC Series in Computing
TI - ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics
VL - 74
ER -
TY - CONF
AB - We present the results of the ARCH 2020 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fourth edition, eight tools have been applied to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.
AU - Althoff, Matthias
AU - Bak, Stanley
AU - Bao, Zongnan
AU - Forets, Marcelo
AU - Frehse, Goran
AU - Freire, Daniel
AU - Kochdumper, Niklas
AU - Li, Yangge
AU - Mitra, Sayan
AU - Ray, Rajarshi
AU - Schilling, Christian
AU - Schupp, Stefan
AU - Wetzlinger, Mark
ID - 8572
T2 - EPiC Series in Computing
TI - ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics
VL - 74
ER -
TY - CONF
AB - A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
AU - Avni, Guy
AU - Henzinger, Thomas A
ID - 8599
SN - 18688969
T2 - 31st International Conference on Concurrency Theory
TI - A survey of bidding games on graphs
VL - 171
ER -
TY - CONF
AB - A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 8600
SN - 18688969
T2 - 31st International Conference on Concurrency Theory
TI - Multi-dimensional long-run average problems for vector addition systems with states
VL - 171
ER -
TY - CONF
AB - We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers.
AU - Henzinger, Thomas A
AU - Sarac, Naci E
ID - 8623
SN - 0302-9743
T2 - Runtime Verification
TI - Monitorability under assumptions
VL - 12399
ER -
TY - JOUR
AB - A central goal of artificial intelligence in high-stakes decision-making applications is to design a single algorithm that simultaneously expresses generalizability by learning coherent representations of their world and interpretable explanations of its dynamics. Here, we combine brain-inspired neural computation principles and scalable deep learning architectures to design compact neural controllers for task-specific compartments of a full-stack autonomous vehicle control system. We discover that a single algorithm with 19 control neurons, connecting 32 encapsulated input features to outputs by 253 synapses, learns to map high-dimensional inputs into steering commands. This system shows superior generalizability, interpretability and robustness compared with orders-of-magnitude larger black-box learning systems. The obtained neural agents enable high-fidelity autonomy for task-specific parts of a complex autonomous system.
AU - Lechner, Mathias
AU - Hasani, Ramin
AU - Amini, Alexander
AU - Henzinger, Thomas A
AU - Rus, Daniela
AU - Grosu, Radu
ID - 8679
JF - Nature Machine Intelligence
TI - Neural circuit policies enabling auditable autonomy
VL - 2
ER -
TY - CONF
AB - Traditional robotic control suits require profound task-specific knowledge for designing, building and testing control software. The rise of Deep Learning has enabled end-to-end solutions to be learned entirely from data, requiring minimal knowledge about the application area. We design a learning scheme to train end-to-end linear dynamical systems (LDS)s by gradient descent in imitation learning robotic domains. We introduce a new regularization loss component together with a learning algorithm that improves the stability of the learned autonomous system, by forcing the eigenvalues of the internal state updates of an LDS to be negative reals. We evaluate our approach on a series of real-life and simulated robotic experiments, in comparison to linear and nonlinear Recurrent Neural Network (RNN) architectures. Our results show that our stabilizing method significantly improves test performance of LDS, enabling such linear models to match the performance of contemporary nonlinear RNN architectures. A video of the obstacle avoidance performance of our method on a mobile robot, in unseen environments, compared to other methods can be viewed at https://youtu.be/mhEsCoNao5E.
AU - Lechner, Mathias
AU - Hasani, Ramin
AU - Rus, Daniela
AU - Grosu, Radu
ID - 8704
SN - 10504729
T2 - Proceedings - IEEE International Conference on Robotics and Automation
TI - Gershgorin loss stabilizes the recurrent neural network compartment of an end-to-end robot learning scheme
ER -
TY - JOUR
AB - Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.
AU - Bogomolov, Sergiy
AU - Forets, Marcelo
AU - Frehse, Goran
AU - Potomkin, Kostiantyn
AU - Schilling, Christian
ID - 8790
IS - 11
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
SN - 02780070
TI - Reachability analysis of linear hybrid systems via block decomposition
VL - 39
ER -
TY - CONF
AB - The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence.
AU - Ferrere, Thomas
AU - Henzinger, Thomas A
AU - Kragl, Bernhard
ID - 7348
SN - 1868-8969
T2 - 28th EACSL Annual Conference on Computer Science Logic
TI - Monitoring event frequencies
VL - 152
ER -
TY - JOUR
AB - This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.
AU - Garcia Soto, Miriam
AU - Prabhakar, Pavithra
ID - 7426
IS - 5
JF - Nonlinear Analysis: Hybrid Systems
SN - 1751570X
TI - Abstraction based verification of stability of polyhedral switched systems
VL - 36
ER -