Towards Efficient Exact Synthesis for Linear Hybrid Systems

TL;DR

This paper presents an efficient method for exactly synthesizing controllable regions in linear hybrid automata using polyhedral abstractions, with implementation and experimental validation on the PHAVer tool.

Contribution

It introduces optimized techniques for exact controllable region synthesis in linear hybrid systems leveraging polyhedral abstractions, enhancing computational efficiency.

Findings

Successful implementation on PHAVer demonstrating practical applicability.

Significant reduction in computation time compared to previous methods.

Effective handling of safety objectives in hybrid automata.

Abstract

We study the problem of automatically computing the controllable region of a Linear Hybrid Automaton, with respect to a safety objective. We describe the techniques that are needed to effectively and efficiently implement a recently-proposed solution procedure, based on polyhedral abstractions of the state space. Supporting experimental results are presented, based on an implementation of the proposed techniques on top of the tool PHAVer.