8 citations · 18 across the 5 of their papers we have counts for
5 papers
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
Céline Bellanger, Pierre-Loïc Garoche, Matthieu Martel +1
Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a…
Fixed Points of the Set-Based Bellman Operator
Sarah H. Q. Li, Assalé Adjé, Pierre-Loïc Garoche +1
Motivated by uncertain parameters encountered in Markov decision processes (MDPs), we study the effect of parameter uncertainty on Bellman operator-based methods. Specifically, we…
Hierarchical State Machines as Modular Horn Clauses
Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
In model based development, embedded systems are modeled using a mix of dataflow formalism, that capture the flow of computation, and hierarchical state machines, that capture the…
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characte…
Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics
Assalé Adjé, Pierre-Loïc Garoche, Alexis Werey
Affine forms are a common way to represent convex sets of using a base of error terms . Quadratic forms are an extension of affine forms enabling the u…