Symbolic Abstractions with Guarantees: A Data-Driven Divide-and-Conquer Strategy

TL;DR

This paper presents a data-driven divide-and-conquer method to create symbolic abstractions of interconnected control networks with unknown models, enabling formal verification and control synthesis with probabilistic guarantees.

Contribution

It introduces a novel data-driven framework using alternating pseudo-bisimulation functions and compositional techniques to construct symbolic abstractions for unknown interconnected systems.

Findings

Successfully applied to a 100-room temperature network

Constructed symbolic abstractions from data with probabilistic guarantees

Synthesized controllers to regulate temperature within safe zones

Abstract

This article is concerned with a data-driven divide-and-conquer strategy to construct symbolic abstractions for interconnected control networks with unknown mathematical models. We employ a notion of alternating bisimulation functions (ABF) to quantify the closeness between state trajectories of an interconnected network and its symbolic abstraction. Consequently, the constructed symbolic abstraction can be leveraged as a beneficial substitute for the formal verification and controller synthesis over the interconnected network. In our data-driven framework, we first establish a relation between each unknown subsystem and its data-driven symbolic abstraction, so-called alternating pseudo-bisimulation function (APBF), with a guaranteed probabilistic confidence. We then provide compositional conditions based on max-type small-gain techniques to construct an ABF for an unknown interconnected network using APBF of its individual subsystems, constructed from data. We demonstrate the efficacy of our data-driven approach over a room temperature network composing 100 rooms with unknown models. We construct a symbolic abstraction from data for each room as an appropriate substitute of original system and compositionally synthesize controllers regulating the temperature of each room within a safe zone with some guaranteed probabilistic confidence.