Seminari
Da febbraio 2019, l’Istituto del Software ha iniziato una serie di seminari. Ogni giovedì pomeriggio, un ricercatore dell’Istituto terrà un breve discorso su un argomento di ingegneria del software a sua scelta, come ad esempio articoli interessanti pubblicati di recente, articoli seminali nel proprio campo di ricerca, discussioni su idee preliminari, tutorial e piccoli esperimenti.
Sulla nostra playlist YouTube potete riguardare alcuni dei seminari precedenti. Di seguito trovate ulteriori dettagli sul prossimo seminario, su quelli a venire e un archivio dei relatori precedenti.
Tutti sono invitati a partecipare ai seminari organizzati dall’Istituto del Software.
Prossimo Relatore: Andrea Manini
Many real-time systems involve a controller interacting with an unpredictable environment, such as a robot whose chosen action may succeed or fail based on the behavior of external human operators. A natural way to reason about such systems involve games, played over time, between controller and environment, also known as Timed Games. However, classical Timed Games formulations struggle with a common interaction pattern: the controller first commits to an action, and only afterwards does the environment resolve how that action is effectively performed. Capturing this pattern in standard Timed Games formulations is either unsuitable or requires substantial modeling effort.
In this talk, I will present Timed CLTLoc Games (TCGs), a variant of Timed Games designed to model these patterns naturally. TCGs differ from the classical formulations in two ways. First, control is assigned to locations rather than transitions, so the player who moves is determined by where the system is. Second, controller objectives are expressed in Constraint LTL over clocks, a linear temporal logic with constraints over clocks. I will then turn to the algorithmic side, showing how to solve TCGs for objectives such as reachability and safety. Interestingly, for reachability objectives, the synthesized strategies ensure that the goal is reached using the minimum number of moves.
Andrea Manini is a PhD student in the Department of Electronics, Information and Bioengineering at Politecnico di Milano, currently in a visiting period at the Università della Svizzera Italiana in Lugano. His research focuses on formal methods for software engineering and real-time systems, with a particular emphasis on model checking techniques for Timed Automata and Timed Games. He is a core developer of Tarzan, a region-based C++ library for Timed Automata verification and Timed Game solving.
Programma
-
Alexander Lercher12 Novembre 2026
-
19 Novembre 2026
-
26 Novembre 2026