Curriculum
Computer Science for Societal Challenges and Innovation, XLI series
Grant sponsor
UNIPD
Supervisor
Davide Bresolin
Co-supervisor
to be defined
Contact
roberto.borelli@phd.unipd.it
Project description
Formal verification techniques (such as model checking or monitoring) are essential tools for ensuring that the behaviour of a system satisfies a given specification, typically expressed in Linear Temporal Logic (LTL). These methodologies play a crucial role in the analysis of safety-critical systems, and more broadly in guaranteeing the trustworthiness and reliability of complex computational infrastructures. In this context, the theoretical foundations of LTL still present several open questions, many of which have a direct impact on verification procedures. My research aims to contribute to these theoretical foundations through the study of cascades of automata. A starting point for this approach is the Krohn–Rhodes theorem, a celebrated result in semiautomata theory and semigroup algebra. It implies that every behaviour definable in LTL can be represented by a cascade of extremely simple computational units, namely two-state reset automata. By exploiting the simple structure of reset automata, more efficient verification and synthesis algorithms can be developed. Beyond the relevance of cascades of automata to logic and verification, there are also deep connections to other areas of computer science. In particular, the theory may offer insights into the study of modern neural architectures such as the Transformer.