3 papers
cs.LO2025
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…
cs.LO2025
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…
cs.LO2025
Decentralized Planning Using Probabilistic Hyperproperties
Francesco Pontiggia, Filip Macák, Roman Andriushchenko +2
Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected rewar…