scholarly journals ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures

2021 ◽  
pp. 99-122
Author(s):  
Lorenz Leutgeb ◽  
Georg Moser ◽  
Florian Zuleger
Keyword(s):  
Potential Function ◽  
Data Structures ◽  
Recent Progress ◽  
Complexity Analysis ◽  
Target Function ◽  
Linear Constraint ◽  
Potential Functions ◽  
Resource Analysis ◽  
Constraint System ◽  
Scalable Analysis

AbstractBeing able to argue about the performance of self-adjusting data structures such as splay trees has been a main objective, when Sleator and Tarjan introduced the notion of amortised complexity.Analysing these data structures requires sophisticated potential functions, which typically contain logarithmic expressions. Possibly for these reasons, and despite the recent progress in automated resource analysis, they have so far eluded automation. In this paper, we report on the first fully-automated amortised complexity analysis of self-adjusting data structures. Following earlier work, our analysis is based on potential function templates with unknown coefficients.We make the following contributions: 1) We encode the search for concrete potential function coefficients as an optimisation problem over a suitable constraint system. Our target function steers the search towards coefficients that minimise the inferred amortised complexity. 2) Automation is achieved by using a linear constraint system in conjunction with suitable lemmata schemes that encapsulate the required non-linear facts about the logarithm. We discuss our choices that achieve a scalable analysis. 3) We present our tool $$\mathsf {ATLAS}$$ ATLAS and report on experimental results for splay trees, splay heaps and pairing heaps. We completely automatically infer complexity estimates that match previous results (obtained by sophisticated pen-and-paper proofs), and in some cases even infer better complexity estimates than previously published.

scholarly journals Exponential Automatic Amortized Resource Analysis

2020 ◽  
pp. 359-380
Author(s):  
David M. Kahn ◽  
Jan Hoffmann
Keyword(s):  
Stirling Numbers ◽  
Linear Constraint ◽  
Potential Functions ◽  
Binomial Coefficients ◽  
Combined System ◽  
Resource Analysis ◽  
Asymptotic Bounds ◽  
Exponential Bounds ◽  
Efficient Type ◽  
Cost Semantics

AbstractAutomatic amortized resource analysis (AARA) is a type-based technique for inferring concrete (non-asymptotic) bounds on a program’s resource usage. Existing work on AARA has focused on bounds that are polynomial in the sizes of the inputs. This paper presents and extension of AARA to exponential bounds that preserves the benefits of the technique, such as compositionality and efficient type inference based on linear constraint solving. A key idea is the use of the Stirling numbers of the second kind as the basis of potential functions, which play the same role as the binomial coefficients in polynomial AARA. To formalize the similarities with the existing analyses, the paper presents a general methodology for AARA that is instantiated to the polynomial version, the exponential version, and a combined system with potential functions that are formed by products of Stirling numbers and binomial coefficients. The soundness of exponential AARA is proved with respect to an operational cost semantics and the analysis of representative example programs demonstrates the effectiveness of the new analysis.

scholarly journals Type-based analysis of logarithmic amortised complexity

2021 ◽  
pp. 1-33
Author(s):  
Martin Hofmann ◽  
Lorenz Leutgeb ◽  
David Obwaller ◽  
Georg Moser ◽  
Florian Zuleger
Keyword(s):  
Data Structures ◽  
Type System ◽  
Automated Analysis ◽  
Logarithmic Potential ◽  
Potential Functions ◽  
Resource Analysis

Abstract We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist’s method of amortised analysis and is potentialbased. The type system makes use of logarithmic potential functions and is the first such system to exhibit logarithmic amortised complexity. With our approach, we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of splaying, once the type annotations are fixed.

The derivation of the rotational potential function from atom–atom potentials. III. Borohydride compounds

1988 ◽  
Vol 66 (4) ◽  
pp. 791-793 ◽  
Author(s):  
David Smith
Keyword(s):  
Transition Temperature ◽  
Experimental Method ◽  
Potential Function ◽  
Ground Level ◽  
Potential Functions ◽  
The Difference ◽  
Level Degeneracy ◽  
Entropy Of Transition ◽  
Good Agreement

The rotational potential functions for the borohydride ion embedded in potassium and rubidium halides are derived from atom–atom potentials of the Buckingham (exp-6) type. The librational frequencies computed from the potential functions are in good agreement with the observed frequencies. The potential functions for rubidium and potassium borohydrides derived from the atom–atom potentials yield librational frequencies that are about 10% higher than the observed values. Since the entropy of transition for potassium and rubidium borohydrides is less than expected, there is a possibility that there is some ordering of the borohydride ions above the transition temperature. An experimental method is presented for studying the ordering of the borohydride ions based on the difference in the ground level degeneracy of a tetrahedral ion in ordered and disordered states.

scholarly journals Synchronous linear constraint system games

2021 ◽  
Vol 62 (3) ◽  
pp. 032201
Author(s):  
Adina Goldberg
Keyword(s):  
Linear Constraint ◽  
Constraint System

Control of Multiple Mobile Agents Via Artificial Potential Functions and Random Motion

2007 ◽  
Author(s):  
Manish Kumar ◽  
Devendra P. Garg ◽  
Randy Zachery
Keyword(s):  
Potential Function ◽  
Mobile Agents ◽  
Formation Control ◽  
Cluster Formation ◽  
Limited Range ◽  
Random Motion ◽  
Potential Functions ◽  
Random Behavior ◽  
Artificial Potential Function ◽  
Multiple Mobile Agents

This paper investigates the effectiveness of designed random behavior in cooperative formation control of multiple mobile agents. A method based on artificial potential functions provides a framework for decentralized control of their formation. However, it implies heavy communication costs. The communication requirement can be replaced by onboard sensors. The onboard sensors have limited range and provide only local information, and may result in the formation of isolated clusters. This paper proposes to introduce a component representing random motion in the artificial potential function formulation of the formation control problem. The introduction of the random behavior component results in a better chance of global cluster formation. The paper uses an agent model that includes both position and orientation, and formulates the dynamic equations to incorporate that model in artificial potential function approach. The effectiveness of the proposed method is verified via extensive simulations performed on a group of mobile agents and leaders.

Constrained on-board attitude control using gas jet thrusters

1999 ◽  
Vol 103 (1030) ◽  
pp. 549-556 ◽  
Author(s):  
G. Radice ◽  
C. R. Mclnnes
Keyword(s):  
Potential Function ◽  
Attitude Control ◽  
Computational Effort ◽  
Potential Functions ◽  
Geometric Configuration ◽  
Gas Jet ◽  
New Approach ◽  
Safety Critical ◽  
Current Attitude ◽  
Lyapunov’S Theorem

Abstract This paper analyses a new approach utilising potential functions to autonomously control constrained attitude slew manoeuvres using gas jet thrusters. The method hinges on defining a potential function from the geometric configuration of the satellite's current attitude, the final target attitude and any pointing constraint which may be present. It will be demonstrated that complex path shaping and planning can be achieved using little computational effort. The method is mathematically validated using Lyapunov's theorem, and so can be considered for safety critical applications.

Modeling of Elastically Coupled Bodies: Part I—General Theory and Geometric Potential Function Method

1998 ◽  
Vol 120 (4) ◽  
pp. 496-500 ◽  
Author(s):  
Ernest D. Fasse ◽  
Peter C. Breedveld
Keyword(s):  
General Theory ◽  
Potential Energy ◽  
Potential Function ◽  
Geometric Modeling ◽  
Function Method ◽  
Rigid Bodies ◽  
Potential Functions ◽  
Energy Functions ◽  
Automatic Computation ◽  
Potential Energy Functions

This paper looks at spatio-geometric modeling of elastically coupled rigid bodies. Desirable properties of compliance families are defined (sufficient diversity, parsimony, frame-indifference, and port-indifference). A novel compliance family with the desired properties is defined using geometric potential energy functions. The configuration-dependent wrenches corresponding to these potential functions are derived in a form suitable for automatic computation.

On different parameterisation methods to analyse spacecraft attitude manoeuvres in the presence of attitude constraints

2007 ◽  
Vol 111 (1119) ◽  
pp. 335-342 ◽  
Author(s):  
G. Radice ◽  
M. Casasco
Keyword(s):  
Potential Function ◽  
Function Method ◽  
Potential Functions ◽  
Spacecraft Attitude ◽  
Modified Rodrigues Parameters ◽  
Current Attitude ◽  
Definition Of ◽  
Potential Function Method

Abstract This paper analyses and compares two different attitude representations, using quaternions and modified Rodrigues parameters, in the context of the potential function method applied to autonomously control constrained attitude slew manoeuvres. This method hinges on the definition of novel Lyapunov potential functions in terms of the attitude parameters representing the current attitude, the goal attitude and any pointing constraints, which may be present. It proves to be successful in forcing the satellite to achieve the desired attitude while at the same time avoiding the pointing constraints. A linearised version of the modified Rodrigues parameterisation is also introduced and analysed. Finally advantages and drawbacks of all attitude representations are discussed.

Sign in / Sign up

Export Citation Format

Share Document