Invited Speakers

---

 

Kyungmin Bae, POSTECH, South Korea

Title: Robust Model Checking for Signal Temporal Logic

Abstract: Signal Temporal Logic (STL) is a temporal logic for specifying linear-time properties of continuous signals. It is widely used in monitoring and testing hybrid systems that exhibit both discrete and continuous behavior. However, model checking for such systems has mostly focused on invariants and reachability, due to the difficulty of handling uncountably many continuously evolving signals. In this talk, I introduce a bounded model checking approach for general STL properties of hybrid systems. Our method is built on a novel logical foundation for STL, including: (i) syntactic separation, which decomposes STL formulas into parts that depend exclusively on separate signal segments; (ii) signal discretization, which abstracts continuous signals into discrete elements; and (iii) epsilon-strengthening, which reduces robust STL checking to Boolean STL checking. This foundation allows STL model checking—up to given bounds and robustness thresholds—to be reduced to the satisfiability of a first-order formula, which is decidable if the reachability of the underlying hybrid system is decidable.

 

---

 

Christoph Haase, University of Oxford, UK

Title: TBA

Abstract: TBA

 

---

 

Shunsuke Inenaga, Kyushu University, Japan

Title: TBA

Abstract: TBA

 

---

 

Dora Giammarresi, University of Rome Tor Vergata, Italy

Title: Partial Cubes and Fibonacci Dimension: Insights and Perspectives

Abstract: A partial cube is a graph \(G \) that embeds isometrically into a hypercube \( Q_k \), with minimum such \( k \) called the isometric dimension \( \operatorname{idim}(G) \) of \(G \). A Fibonacci cube \(\Gamma_k \) excludes from the vertices strings containing “11”, and any partial cube \(G \) embeds into some \( \Gamma_d \), defining the Fibonacci dimension \( \operatorname{fdim}(G) \) as the minimum such \( d \). It holds that \( \operatorname{idim}(G) \leq \operatorname{fdim}(G) \leq 2 \cdot \operatorname{idim}(G) - 1.\) While \(\operatorname{idim}(G) \) is computable in polynomial time, checking whether \( \operatorname{idim}(G) = \operatorname{fdim}(G) \) is NP-complete. We survey properties of partial cubes and generalized Fibonacci cubes, and present a new family of graphs \( G \) for which \( \operatorname{idim}(G) = \operatorname{fdim}(G). \) We conclude with some open problems.