Verification Series

Symbolic Limited Lookahead Control for Best-effort Dynamic Computing Resource Management

14th December 2017, 14:00 add to calender
Nicholas Berthier

Abstract

I will discuss the problem of enforcing best-effort control on symbolic logico-numerical systems. The latter involve state and input variables defined on infinite domains (e.g, Integers), thereby no exact algorithm exist even for safety control. Yet, relaxed versions of such control objectives are still of interest for a number of non-critical applications. I will thus present the notion of limited lookahead, and associated best-effort control objectives targeting safety and optimization on a sliding window for a number of steps ahead. I will describe new symbolic algorithms, and illustrate their application on a case study for dynamic resource management.
add to calender (including abstract)