arXiv subjects

Jiří Fejlek

Publications and source records attributed to Jiří Fejlek.

4 recordsLinked to original sources

arXiv2024

Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals

In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias in the output space. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed algorithm aims to cover all possible outputs directly. Compared to other state-of-the-art falsification tools, it also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.

eess.SY↗

arXiv2024

Computation of Feedback Control Laws Based on Switched Tracking of Demonstrations

A common approach in robotics is to learn tasks by generalizing from special cases given by a so-called demonstrator. In this paper, we apply this paradigm and present an algorithm that uses a demonstrator (typically given by a trajectory optimizer) to automatically synthesize feedback controllers for steering a system described by ordinary differential equations into a goal set. The resulting feedback control law switches between the demonstrations that it uses as reference trajectories. In comparison to the direct use of trajectory optimization as a control law, for example, in the form of model predictive control, this allows for a much simpler and more efficient implementation of the controller. The synthesis algorithm comes with rigorous convergence and optimality results, and computational experiments confirm its efficiency.

eess.SY↗

arXiv2023

LQR-trees with Sampling Based Exploration of the State Space

This paper introduces an extension of the LQR-tree algorithm, which is a feedback-motion-planning algorithm for stabilizing a system of ordinary differential equations from a bounded set of initial conditions to a goal. The constructed policies are represented by a tree of exemplary system trajectories, so called demonstrations, and linear-quadratic regulator (LQR) feedback controllers. Consequently, the crucial component of any LQR-tree algorithm is a demonstrator that provides suitable demonstrations. In previous work, such a demonstrator was given by a local trajectory optimizer. However, these require appropriate initial guesses of solutions to provide valid results, which was pointed out, but largely unresolved in previous implementations. In this paper, we augment the LQR-tree algorithm with a randomized motion-planning procedure to discover new valid demonstration candidates to initialize the demonstrator in parts of state space not yet covered by the LQR-tree. In comparison to the previous versions of the LQR-tree algorithm, the resulting exploring LQR-tree algorithm reliably synthesizes feedback control laws for a far more general set of problems.

eess.SY↗

arXiv2022

Computing Funnels Using Numerical Optimization Based Falsifiers

In this paper, we present an~algorithm that computes funnels along trajectories of systems of ordinary differential equations. A funnel is a time-varying set of states containing the given trajectory, for which the evolution from within the set at any given time stays in the funnel. Hence it generalizes the behavior of single trajectories to sets around them, which is an important task, for example, in robot motion planning. In contrast to approaches based on sum-of-squares programming, which poorly scale to high dimensions, our approach is based on falsification and tackles the funnel computation task directly, through numerical optimization. This approach computes accurate funnel estimates far more efficiently and leaves formal verification to the end, outside all funnel size optimization loops.

cs.RO↗