Person. José Luiz Vargas de Mendonça

Papers

A General Framework for Robust Quantitative Semantics of Signal Temporal Logic chen-2026-a

Quantitative semantics of Signal Temporal Logic (STL) play an important role in both the falsification and control synthesis for dynamical systems by assigning numerical quantities to truth values. Recently, several different quantitative semantics have been proposed, offering better performance in many cases. Yet a general, systematic understanding of the structure and properties of quantitative semantics is missing. In this paper, we develop a general framework to model quantitative semantics. We focus mainly on soundness, which requires that the quantitative semantics of a statement is positive when the statement is true, and negative when the statement is false. This ensures that counterexamples will not be missed during verification. We derive simple, necessary conditions in our framework for soundness. We show how several recently proposed quantitative semantics fit in our framework, and how others do not, typically because they do not strictly satisfy soundness. We implement various quantitative semantics, including existing semantics from literature, in our framework and compare their effectiveness as objective functions for optimization-based falsification on both novel and existing benchmarks.
DOI

Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation chen-2022-synchronous

DOI

Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic jeannin-2022-work

DOI
joseluizvargasdemendonca person entries/rolodex/joseluizvargasdemendonca.hel