7 papers · 1 filter
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Beatrice Melani, Ezio Bartocci, Michele Chiari
Signal Temporal Logic (STL) is a widely recognized formal specification language to express rigorous temporal requirements on mixed analog signals produced by cyber-physical system…
Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputs
Andrey Kofnov, Daniel Kapla, Ezio Bartocci +1
We derive exact upper and lower bounds for the cumulative distribution function (cdf) of the output of a neural network (NN) over its entire support subject to noisy (stochastic) i…
POPACheck: A Model Checker for Probabilistic Pushdown Automata
Francesco Pontiggia, Ezio Bartocci, Michele Chiari
We present POPACheck, the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. POPACheck provides a user-friendly probabil…
Cumulative-Time Signal Temporal Logic
Hongkai Chen, Zeyu Zhang, Shouvik Roy +4
Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and respon…
Moment-based Density Elicitation with Applications in Probabilistic Loops
Andrey Kofnov, Ezio Bartocci, Efstathia Bura
We propose the K-series estimation approach for the recovery of unknown univariate and multivariate distributions given knowledge of a finite number of their moments. Our method is…
Rule-Guided Reinforcement Learning Policy Evaluation and Improvement
Martin Tappler, Ignacio D. Lopez-Miguel, Sebastian Tschiatschek +1
We consider the challenging problem of using domain knowledge to improve deep reinforcement learning policies. To this end, we propose LEGIBLE, a novel approach, following a multi-…