4 papers · 2 filters
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…
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…
Model Checking Probabilistic Operator Precedence Automata
Francesco Pontiggia, Ezio Bartocci, Michele Chiari
We address the problem of model checking context-free specifications for probabilistic pushdown automata, which has relevant applications in the verification of recursive probabili…