Showing 1–8 of 8 results for author: Mover, S

Reconciling Spatial and Temporal Abstractions for Goal Representation

Authors: Mehdi Zadem, Sergio Mover, Sao Mai Nguyen

Abstract: Goal representation affects the performance of Hierarchical Reinforcement Learning (HRL) algorithms by decomposing the complex learning problem into easier subtasks. Recent studies show that representations that preserve temporally abstract environment dynamics are successful in solving difficult problems and provide theoretical guarantees for optimality. These methods however cannot scale to task… ▽ More Goal representation affects the performance of Hierarchical Reinforcement Learning (HRL) algorithms by decomposing the complex learning problem into easier subtasks. Recent studies show that representations that preserve temporally abstract environment dynamics are successful in solving difficult problems and provide theoretical guarantees for optimality. These methods however cannot scale to tasks where environment dynamics increase in complexity i.e. the temporally abstract transition relations depend on larger number of variables. On the other hand, other efforts have tried to use spatial abstraction to mitigate the previous issues. Their limitations include scalability to high dimensional environments and dependency on prior knowledge. In this paper, we propose a novel three-layer HRL algorithm that introduces, at different levels of the hierarchy, both a spatial and a temporal goal abstraction. We provide a theoretical study of the regret bounds of the learned policies. We evaluate the approach on complex continuous control tasks, demonstrating the effectiveness of spatial and temporal abstractions learned by this approach. Find open-source code at https://github.com/cosynus-lix/STAR. △ Less

Submitted 30 June, 2024; v1 submitted 18 January, 2024; originally announced January 2024.

Journal ref: ICLR 2024

Goal Space Abstraction in Hierarchical Reinforcement Learning via Set-Based Reachability Analysis

Authors: Mehdi Zadem, Sergio Mover, Sao Mai Nguyen

Abstract: Open-ended learning benefits immensely from the use of symbolic methods for goal representation as they offer ways to structure knowledge for efficient and transferable learning. However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic… ▽ More Open-ended learning benefits immensely from the use of symbolic methods for goal representation as they offer ways to structure knowledge for efficient and transferable learning. However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic goal representation is that it must preserve critical information, such as the environment dynamics. In this paper, we propose a developmental mechanism for goal discovery via an emergent representation that abstracts (i.e., groups together) sets of environment states that have similar roles in the task. We introduce a Feudal HRL algorithm that concurrently learns both the goal representation and a hierarchical policy. The algorithm uses symbolic reachability analysis for neural networks to approximate the transition relation among sets of states and to refine the goal representation. We evaluate our approach on complex navigation tasks, showing the learned representation is interpretable, transferrable and results in data efficient learning. △ Less

Submitted 22 November, 2023; v1 submitted 14 September, 2023; originally announced September 2023.

ACM Class: K.3.2

Goal Space Abstraction in Hierarchical Reinforcement Learning via Reachability Analysis

Authors: Mehdi Zadem, Sergio Mover, Sao Mai Nguyen

Abstract: Open-ended learning benefits immensely from the use of symbolic methods for goal representation as they offer ways to structure knowledge for efficient and transferable learning. However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic… ▽ More Open-ended learning benefits immensely from the use of symbolic methods for goal representation as they offer ways to structure knowledge for efficient and transferable learning. However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic goal representation is that it must preserve critical information, such as the environment dynamics. In this work, we propose a developmental mechanism for subgoal discovery via an emergent representation that abstracts (i.e., groups together) sets of environment states that have similar roles in the task. We create a HRL algorithm that gradually learns this representation along with the policies and evaluate it on navigation tasks to show the learned representation is interpretable and results in data efficiency. △ Less

Submitted 12 September, 2023; originally announced September 2023.

Journal ref: Intrinsically Motivated Open-ended Learning IMOL 2023, Sep 2023, Paris, France

Historia: Refuting Callback Reachability with Message-History Logics (Extended Version)

Authors: Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang

Abstract: This paper determines if a callback can be called by an event-driven framework in an unexpected state.Event-driven programming frameworks are pervasive for creating user-interactive apps on just about every modern platform.Control flow between callbacks is determined by the framework and largely opaque to the programmer.This opacity of the callback control flow not only causes difficulty for the p… ▽ More This paper determines if a callback can be called by an event-driven framework in an unexpected state.Event-driven programming frameworks are pervasive for creating user-interactive apps on just about every modern platform.Control flow between callbacks is determined by the framework and largely opaque to the programmer.This opacity of the callback control flow not only causes difficulty for the programmer but is also difficult for those develo** static analysis.Previous static analysis techniques address this opacity either by assuming an arbitrary framework implementation or attempting to eagerly specify all possible callback control flow, but this is either too coarse or too burdensome and tricky to get right.Instead, we present a middle way where the callback control flow can be gradually refined in a targeted manner to prove assertions of interest.The key insight to get this middle way is by reasoning about the history of method invocations at the boundary between app and framework code - enabling a decoupling of the specification of callback control flow from the analysis of app code.We call the sequence of such boundary-method invocations message histories and develop message-history logics to do this reasoning.In particular, we define the notion of an application-only transition system with boundary transitions, a message-history program logic for programs with such transitions, and a temporal specification logic for capturing callback control flow in a targeted and compositional manner.Then to utilize the logics in a goal-directed verifier, we define a way to combine after-the-fact an assertion about message histories with a specification of callback control flow.We implemented a prototype message history-based verifier called Historia that enables proving the absence of multi-callback bug patterns in real-world open-source Android apps. △ Less

Submitted 11 September, 2023; v1 submitted 8 September, 2023; originally announced September 2023.

Comments: 40 pages, 8 figures, Accepted to OOPSLA 2023

MSC Class: 68Q60 ACM Class: D.3.3

Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version)

Authors: Shawn Meier, Sergio Mover, Bor-Yuh Evan Chang

Abstract: Develo** interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interfa… ▽ More Develo** interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable. △ Less

Submitted 12 June, 2019; v1 submitted 11 June, 2019; originally announced June 2019.

Comments: 26 pages, 11 figures, ECOOP 2019

DroidStar: Callback Typestates for Android Classes

Authors: Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, Pavol Černý

Abstract: Event-driven programming frameworks, such as Android, are based on components with asynchronous interfaces. The protocols for interacting with these components can often be described by finite-state machines we dub *callback typestates*. Callback typestates are akin to classical typestates, with the difference that their outputs (callbacks) are produced asynchronously. While useful, these specific… ▽ More Event-driven programming frameworks, such as Android, are based on components with asynchronous interfaces. The protocols for interacting with these components can often be described by finite-state machines we dub *callback typestates*. Callback typestates are akin to classical typestates, with the difference that their outputs (callbacks) are produced asynchronously. While useful, these specifications are not commonly available, because writing them is difficult and error-prone. Our goal is to make the task of producing callback typestates significantly easier. We present a callback typestate assistant tool, DroidStar, that requires only limited user interaction to produce a callback typestate. Our approach is based on an active learning algorithm, L*. We improved the scalability of equivalence queries (a key component of L*), thus making active learning tractable on the Android system. We use DroidStar to learn callback typestates for Android classes both for cases where one is already provided by the documentation, and for cases where the documentation is unclear. The results show that DroidStar learns callback typestates accurately and efficiently. Moreover, in several cases, the synthesized callback typestates uncovered surprising and undocumented behaviors. △ Less

Submitted 2 March, 2018; v1 submitted 26 January, 2017; originally announced January 2017.

Comments: Appearing at ICSE 2018

Abstracting Event-Driven Systems with Lifestate Rules

Authors: Shawn Meier, Aleksandar Chakarov, Maxwell Russek, Sergio Mover, Bor-Yuh Evan Chang

Abstract: We present lifestate rules--an approach for abstracting event-driven object protocols. Develo** applications against event-driven software frameworks is notoriously difficult. One reason why is that to create functioning applications, developers must know about and understand the complex protocols that abstract the internal behavior of the framework. Such protocols intertwine the proper register… ▽ More We present lifestate rules--an approach for abstracting event-driven object protocols. Develo** applications against event-driven software frameworks is notoriously difficult. One reason why is that to create functioning applications, developers must know about and understand the complex protocols that abstract the internal behavior of the framework. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application programming interface (API) calls to delegate back to it. Lifestate rules unify lifecycle and typestate constraints in one common specification language. Our primary contribution is a model of event-driven systems from which lifestate rules can be derived. We then apply specification mining techniques to learn lifestate specifications for Android framework types. In the end, our implementation is able to find several rules that characterize actual behavior of the Android framework. △ Less

Submitted 31 December, 2016; originally announced January 2017.

ACM Class: D.2.4; F.3.1

IC3 Modulo Theories via Implicit Predicate Abstraction

Authors: Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta

Abstract: We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract tran- sitions without computing explicitly the abstract system and is incremental with re… ▽ More We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract tran- sitions without computing explicitly the abstract system and is incremental with respect to the addition of predicates. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discov- ering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike current SMT gener- alizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available, and can moreover be inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improve- ment, as our experiments demonstrate. △ Less

Submitted 25 October, 2013; originally announced October 2013.

ACM Class: D.2.4; B.5.2