-
Combined Left and Right Temporal Robustness for Control under STL Specifications
Authors:
Alëna Rodionova,
Lars Lindemann,
Manfred Morari,
George J. Pappas
Abstract:
Many modern autonomous systems, particularly multi-agent systems, are time-critical and need to be robust against timing uncertainties. Previous works have studied left and right time robustness of signal temporal logic specifications by considering time shifts in the predicates that are either only to the left or only to the right. We propose a combined notion of temporal robustness which simulta…
▽ More
Many modern autonomous systems, particularly multi-agent systems, are time-critical and need to be robust against timing uncertainties. Previous works have studied left and right time robustness of signal temporal logic specifications by considering time shifts in the predicates that are either only to the left or only to the right. We propose a combined notion of temporal robustness which simultaneously considers left and right time shifts. For instance, in a scenario where a robot plans a trajectory around a pedestrian, this combined notion can now capture uncertainty of the pedestrian arriving earlier or later than anticipated. We first derive desirable properties of this new notion with respect to left and right time shifts and then design control laws for linear systems that maximize temporal robustness using mixed-integer linear programming. Finally, we present two case studies to illustrate how the proposed temporal robustness accounts for timing uncertainties.
△ Less
Submitted 8 June, 2023;
originally announced June 2023.
-
The Open corpus of the Veps and Karelian languages: overview and applications
Authors:
Tatyana Boyko,
Nina Zaitseva,
Natalia Krizhanovskaya,
Andrew Krizhanovsky,
Irina Novak,
Nataliya Pellinen,
Aleksandra Rodionova
Abstract:
A growing priority in the study of Baltic-Finnic languages of the Republic of Karelia has been the methods and tools of corpus linguistics. Since 2016, linguists, mathematicians, and programmers at the Karelian Research Centre have been working with the Open Corpus of the Veps and Karelian Languages (VepKar), which is an extension of the Veps Corpus created in 2009. The VepKar corpus comprises tex…
▽ More
A growing priority in the study of Baltic-Finnic languages of the Republic of Karelia has been the methods and tools of corpus linguistics. Since 2016, linguists, mathematicians, and programmers at the Karelian Research Centre have been working with the Open Corpus of the Veps and Karelian Languages (VepKar), which is an extension of the Veps Corpus created in 2009. The VepKar corpus comprises texts in Karelian and Veps, multifunctional dictionaries linked to them, and software with an advanced system of search using various criteria of the texts (language, genre, etc.) and numerous linguistic categories (lexical and grammatical search in texts was implemented thanks to the generator of word forms that we created earlier). A corpus of 3000 texts was compiled, texts were uploaded and marked up, the system for classifying texts into languages, dialects, types and genres was introduced, and the word-form generator was created. Future plans include develo** a speech module for working with audio recordings and a syntactic tagging module using morphological analysis outputs. Owing to continuous functional advancements in the corpus manager and ongoing VepKar enrichment with new material and text markup, users can handle a wide range of scientific and applied tasks. In creating the universal national VepKar corpus, its developers and managers strive to preserve and exhibit as fully as possible the state of the Veps and Karelian languages in the 19th-21st centuries.
△ Less
Submitted 8 June, 2022;
originally announced June 2022.
-
Neuropunk Revolution. Hacking Cognitive Systems towards Cyborgs 3.0
Authors:
Max Talanov,
Jordi Vallverdu,
Andrew Adamatzky,
Alexander Toschev,
Alina Suleimanova,
Alexey Leukhin,
Ann Posdeeva,
Yulia Mikhailova,
Alice Rodionova,
Alexey Mikhaylov,
Alexander Serb,
Sergey Shchanikov,
Svetlana Gerasimova,
Mohammad Mahdi Dehshibi,
Alexander Hramov,
Victor Kazantsev,
Tatyana Tsoy,
Evgeni Magid,
Igor Lavrov,
Victor Erokhin,
Kevin Warwick
Abstract:
This work is dedicated to the review and perspective of the new direction that we call "Neuropunk revolution" resembling the cultural phenomenon of cyberpunk. This new phenomenon has its foundations in advances in neuromorphic technologies including memristive and bio-plausible simulations, BCI, and neurointerfaces as well as unconventional approaches to AI and computing in general. We present the…
▽ More
This work is dedicated to the review and perspective of the new direction that we call "Neuropunk revolution" resembling the cultural phenomenon of cyberpunk. This new phenomenon has its foundations in advances in neuromorphic technologies including memristive and bio-plausible simulations, BCI, and neurointerfaces as well as unconventional approaches to AI and computing in general. We present the review of the current state-of-the-art and our vision of near future development of scientific approaches and future technologies. We call the "Neuropunk revolution" the set of trends that in our view provide the necessary background for the new generation of approaches technologies to integrate the cybernetic objects with biological tissues in close loop system as well as robotic systems inspired by the biological processes again integrated with biological objects. We see bio-plausible simulations implemented by digital computers or spiking networks memristive hardware as promising bridge or middleware between digital and (neuro)biological domains.
△ Less
Submitted 13 May, 2022;
originally announced May 2022.
-
Temporal Robustness of Temporal Logic Specifications: Analysis and Control Design
Authors:
Alëna Rodionova,
Lars Lindemann,
Manfred Morari,
George J. Pappas
Abstract:
We study the temporal robustness of temporal logic specifications and show how to design temporally robust control laws for time-critical control systems. This topic is of particular interest in connected systems and interleaving processes such as multi-robot and human-robot systems where uncertainty in the behavior of individual agents and humans can induce timing uncertainty. Despite the importa…
▽ More
We study the temporal robustness of temporal logic specifications and show how to design temporally robust control laws for time-critical control systems. This topic is of particular interest in connected systems and interleaving processes such as multi-robot and human-robot systems where uncertainty in the behavior of individual agents and humans can induce timing uncertainty. Despite the importance of time-critical systems, temporal robustness of temporal logic specifications has not been studied, especially from a control design point of view. We define synchronous and asynchronous temporal robustness and show that these notions quantify the robustness with respect to synchronous and asynchronous time shifts in the predicates of the temporal logic specification. It is further shown that the synchronous temporal robustness upper bounds the asynchronous temporal robustness. We then study the control design problem in which we aim to design a control law that maximizes the temporal robustness of a dynamical system. Our solution consists of a Mixed-Integer Linear Programming (MILP) encoding that can be used to obtain a sequence of optimal control inputs. While asynchronous temporal robustness is arguably more nuanced than synchronous temporal robustness, we show that control design using synchronous temporal robustness is computationally more efficient. This trade-off can be exploited by the designer depending on the particular application at hand. We conclude the paper with a variety of case studies.
△ Less
Submitted 29 March, 2022;
originally announced March 2022.
-
Temporal Robustness of Stochastic Signals
Authors:
Lars Lindemann,
Alena Rodionova,
George J. Pappas
Abstract:
We study the temporal robustness of stochastic signals. This topic is of particular interest in interleaving processes such as multi-agent systems where communication and individual agents induce timing uncertainty. For a deterministic signal and a given specification, we first introduce the synchronous and the asynchronous temporal robustness to quantify the signal's robustness with respect to sy…
▽ More
We study the temporal robustness of stochastic signals. This topic is of particular interest in interleaving processes such as multi-agent systems where communication and individual agents induce timing uncertainty. For a deterministic signal and a given specification, we first introduce the synchronous and the asynchronous temporal robustness to quantify the signal's robustness with respect to synchronous and asynchronous time shifts in its sub-signals. We then define the temporal robustness risk by investigating the temporal robustness of the realizations of a stochastic signal. This definition can be interpreted as the risk associated with a stochastic signal to not satisfy a specification robustly in time. In this definition, general forms of specifications such as signal temporal logic specifications are permitted. We show how the temporal robustness risk is estimated from data for the value-at-risk. The usefulness of the temporal robustness risk is underlined by both theoretical and empirical evidence. In particular, we provide various numerical case studies including a T-intersection scenario in autonomous driving.
△ Less
Submitted 12 March, 2022; v1 submitted 5 February, 2022;
originally announced February 2022.
-
Learning-'N-Flying: A Learning-based, Decentralized Mission Aware UAS Collision Avoidance Scheme
Authors:
Alëna Rodionova,
Yash Vardhan Pant,
Connor Kurtz,
Kuk Jang,
Houssam Abbas,
Rahul Mangharam
Abstract:
Urban Air Mobility, the scenario where hundreds of manned and Unmanned Aircraft System (UAS) carry out a wide variety of missions (e.g. moving humans and goods within the city), is gaining acceptance as a transportation solution of the future. One of the key requirements for this to happen is safely managing the air traffic in these urban airspaces. Due to the expected density of the airspace, thi…
▽ More
Urban Air Mobility, the scenario where hundreds of manned and Unmanned Aircraft System (UAS) carry out a wide variety of missions (e.g. moving humans and goods within the city), is gaining acceptance as a transportation solution of the future. One of the key requirements for this to happen is safely managing the air traffic in these urban airspaces. Due to the expected density of the airspace, this requires fast autonomous solutions that can be deployed online. We propose Learning-'N-Flying (LNF) a multi-UAS Collision Avoidance (CA) framework. It is decentralized, works on-the-fly and allows autonomous UAS managed by different operators to safely carry out complex missions, represented using Signal Temporal Logic, in a shared airspace. We initially formulate the problem of predictive collision avoidance for two UAS as a mixed-integer linear program, and show that it is intractable to solve online. Instead, we first develop Learning-to-Fly (L2F) by combining: a) learning-based decision-making, and b) decentralized convex optimization-based control. LNF extends L2F to cases where there are more than two UAS on a collision path. Through extensive simulations, we show that our method can run online (computation time in the order of milliseconds), and under certain assumptions has failure rates of less than 1% in the worst-case, improving to near 0% in more relaxed operations. We show the applicability of our scheme to a wide variety of settings through multiple case studies.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
Learning-to-Fly: Learning-based Collision Avoidance for Scalable Urban Air Mobility
Authors:
Alëna Rodionova,
Yash Vardhan Pant,
Kuk Jang,
Houssam Abbas,
Rahul Mangharam
Abstract:
With increasing urban population, there is global interest in Urban Air Mobility (UAM), where hundreds of autonomous Unmanned Aircraft Systems (UAS) execute missions in the airspace above cities. Unlike traditional human-in-the-loop air traffic management, UAM requires decentralized autonomous approaches that scale for an order of magnitude higher aircraft densities and are applicable to urban set…
▽ More
With increasing urban population, there is global interest in Urban Air Mobility (UAM), where hundreds of autonomous Unmanned Aircraft Systems (UAS) execute missions in the airspace above cities. Unlike traditional human-in-the-loop air traffic management, UAM requires decentralized autonomous approaches that scale for an order of magnitude higher aircraft densities and are applicable to urban settings. We present Learning-to-Fly (L2F), a decentralized on-demand airborne collision avoidance framework for multiple UAS that allows them to independently plan and safely execute missions with spatial, temporal and reactive objectives expressed using Signal Temporal Logic. We formulate the problem of predictively avoiding collisions between two UAS without violating mission objectives as a Mixed Integer Linear Program (MILP).This however is intractable to solve online. Instead, we develop L2F, a two-stage collision avoidance method that consists of: 1) a learning-based decision-making scheme and 2) a distributed, linear programming-based UAS control algorithm. Through extensive simulations, we show the real-time applicability of our method which is $\approx\!6000\times$ faster than the MILP approach and can resolve $100\%$ of collisions when there is ample room to maneuver, and shows graceful degradation in performance otherwise. We also compare L2F to two other methods and demonstrate an implementation on quad-rotor robots.
△ Less
Submitted 23 June, 2020;
originally announced June 2020.
-
Hybridizing the 1/5-th Success Rule with Q-Learning for Controlling the Mutation Rate of an Evolutionary Algorithm
Authors:
Arina Buzdalova,
Carola Doerr,
Anna Rodionova
Abstract:
It is well known that evolutionary algorithms (EAs) achieve peak performance only when their parameters are suitably tuned to the given problem. Even more, it is known that the best parameter values can change during the optimization process. Parameter control mechanisms are techniques developed to identify and to track these values.
Recently, a series of rigorous theoretical works confirmed the…
▽ More
It is well known that evolutionary algorithms (EAs) achieve peak performance only when their parameters are suitably tuned to the given problem. Even more, it is known that the best parameter values can change during the optimization process. Parameter control mechanisms are techniques developed to identify and to track these values.
Recently, a series of rigorous theoretical works confirmed the superiority of several parameter control techniques over EAs with best possible static parameters. Among these results are examples for controlling the mutation rate of the $(1+λ)$~EA when optimizing the OneMax problem. However, it was shown in [Rodionova et al., GECCO'19] that the quality of these techniques strongly depends on the offspring population size $λ$.
We introduce in this work a new hybrid parameter control technique, which combines the well-known one-fifth success rule with Q-learning. We demonstrate that our HQL mechanism achieves equal or superior performance to all techniques tested in [Rodionova et al., GECCO'19] and this -- in contrast to previous parameter control methods -- simultaneously for all offspring population sizes $λ$. We also show that the promising performance of HQL is not restricted to OneMax, but extends to several other benchmark problems.
△ Less
Submitted 19 June, 2020;
originally announced June 2020.
-
Offspring Population Size Matters when Comparing Evolutionary Algorithms with Self-Adjusting Mutation Rates
Authors:
Anna Rodionova,
Kirill Antonov,
Arina Buzdalova,
Carola Doerr
Abstract:
We analyze the performance of the 2-rate $(1+λ)$ Evolutionary Algorithm (EA) with self-adjusting mutation rate control, its 3-rate counterpart, and a $(1+λ)$~EA variant using multiplicative update rules on the OneMax problem. We compare their efficiency for offspring population sizes ranging up to $λ=3,200$ and problem sizes up to $n=100,000$.
Our empirical results show that the ranking of the a…
▽ More
We analyze the performance of the 2-rate $(1+λ)$ Evolutionary Algorithm (EA) with self-adjusting mutation rate control, its 3-rate counterpart, and a $(1+λ)$~EA variant using multiplicative update rules on the OneMax problem. We compare their efficiency for offspring population sizes ranging up to $λ=3,200$ and problem sizes up to $n=100,000$.
Our empirical results show that the ranking of the algorithms is very consistent across all tested dimensions, but strongly depends on the population size. While for small values of $λ$ the 2-rate EA performs best, the multiplicative updates become superior for starting for some threshold value of $λ$ between 50 and 100. Interestingly, for population sizes around 50, the $(1+λ)$~EA with static mutation rates performs on par with the best of the self-adjusting algorithms.
We also consider how the lower bound $p_{\min}$ for the mutation rate influences the efficiency of the algorithms. We observe that for the 2-rate EA and the EA with multiplicative update rules the more generous bound $p_{\min}=1/n^2$ gives better results than $p_{\min}=1/n$ when $λ$ is small. For both algorithms the situation reverses for large~$λ$.
△ Less
Submitted 18 April, 2019; v1 submitted 16 April, 2019;
originally announced April 2019.
-
Quantitative Regular Expressions for Arrhythmia Detection Algorithms
Authors:
Houssam Abbas,
Alena Rodionova,
Ezio Bartocci,
Scott A. Smolka,
Radu Grosu
Abstract:
Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak de…
▽ More
Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak detection (where a peak in a cardiac signal indicates a heartbeat) and various discriminators, each of which uses a feature of the cardiac signal to distinguish fatal from non-fatal arrhythmias. Expressing these algorithms' desired output in current temporal logics, and implementing them via monitor synthesis, is cumbersome, error-prone, computationally expensive, and sometimes infeasible.
In contrast, we show that a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today's arrhythmia-detection devices are easily expressible in QREs. The fact that one formalism (QREs) is used to describe the desired end-to-end operation of an arrhythmia detector opens the way to formal analysis and rigorous testing of these detectors' correctness and performance. Such analysis could alleviate the regulatory burden on device developers when modifying their algorithms. The performance of the peak-detection QREs is demonstrated by running them on real patient data, on which they yield results on par with those provided by a cardiologist.
△ Less
Submitted 24 September, 2017; v1 submitted 22 December, 2016;
originally announced December 2016.
-
Temporal Logic as Filtering
Authors:
Alena Rodionova,
Ezio Bartocci,
Dejan Nickovic,
Radu Grosu
Abstract:
We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) idempotent dioid. Moreover, by interpreting these operators over the field of reals (+,*,0,1), one can associate various quantitative semantics to a metric-temporal-logic formula, depending on the filter's kernel used: squ…
▽ More
We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) idempotent dioid. Moreover, by interpreting these operators over the field of reals (+,*,0,1), one can associate various quantitative semantics to a metric-temporal-logic formula, depending on the filter's kernel used: square, rounded-square, Gaussian, low-pass, band-pass, or high-pass. This remarkable connection between filtering and metric temporal logic allows us to freely navigate between the two, and to regard signal-feature detection as logical inference. To the best of our knowledge, this connection has not been established before. We prove that our qualitative, filtering semantics is identical to the classical MTL semantics. We also provide a quantitative semantics for MTL, which measures the normalized, maximum number of times a formula is satisfied within its associated kernel, by a given signal. We show that this semantics is sound, in the sense that, if its measure is 0, then the formula is not satisfied, and it is satisfied otherwise. We have implemented both of our semantics in Matlab, and illustrate their properties on various formulas and signals, by plotting their computed measures.
△ Less
Submitted 9 February, 2016; v1 submitted 27 October, 2015;
originally announced October 2015.
