idSTLPy: A Python Toolbox for Active Perception and Control

TL;DR

idSTLPy is a Python toolbox that enables active perception and control synthesis for switched linear systems with probabilistic specifications, integrating model checking, optimization, and motion planning techniques.

Contribution

It introduces a novel Python toolbox combining counterexample-guided synthesis, Bounded Model Checking, linear programming, and sampling-based planning for probabilistic signal temporal logic.

Findings

Successfully applied to vehicle motion planning with noisy localization

Demonstrates effective synthesis of control strategies under uncertainty

Provides accessible open-source implementation

Abstract

This paper describes a Python toolbox for active perception and control synthesis of probabilistic signal temporal logic (PrSTL) formulas of switched linear systems with additive Gaussian disturbances and measurement noises. We implement a counterexample-guided synthesis strategy that combines Bounded Model Checking, linear programming, and sampling-based motion planning techniques. We illustrate our approach and the toolbox throughout the paper with a motion planning example for a vehicle with noisy localization. The code is available at \url{https://codeocean.com/capsule/0013534/tree}.