Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Towards a Set-based Signal Temporal Logic

Abstract : Abstract model-checking methods are efficient to prove properties on systems with infinite state-space dimension. When considering continuoustime dynamical systems, adequate temporal logic has to be used to express specifications of systems. In this short paper, we present our current work on designing a subset of signal temporal logic (STL) amenable to bounded abstract model-checking methods. The proposed approach uses set-based operations as atomic proposition of STL. Set-based approach is more suitable to applied abstract model-checking methods as it allows to consider set of system trajectories instead of only one trajectory of the system. Interval analysis methods are used to give a computable counterpart version of this set-based STL and to compute sets of trajectories of dynamical systems. The correctness of the presented framework is asserted using an abstract interpretation framework.
Complete list of metadatas
Contributor : Alexandre Chapoutot <>
Submitted on : Monday, December 21, 2020 - 12:13:23 PM
Last modification on : Tuesday, January 5, 2021 - 3:40:41 AM


Files produced by the author(s)


  • HAL Id : hal-03084701, version 1


Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Pierre-Loïc Garoche. Towards a Set-based Signal Temporal Logic. 2020. ⟨hal-03084701⟩



Record views


Files downloads