mercredi 17 décembre 2025

par BUTEL Nathalie

Nicolas Mazzocchi (STU Bratislava, Slovaquie) invité au laboratoire en fin d'année dans le pôle COMRED, donnera un séminaire le mercredi 17 décembre 2025 à 11 h dans la salle 007 (algorithmes).

 

 Title : Safety and liveness of quantitative properties and automata

 

Abstract :

Safety and liveness are fundamental concepts in computer-aided verification. The safety-liveness classification of Boolean properties determines whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). This talk extends the safety-liveness framework to quantitative properties, defined as arbitrary functions from infinite words to partially ordered domains. This framework will be instantiated with the classes of quantitative properties expressed by automata, which map infinite words to real numbers. Then, procedures for deciding whether a given automaton defines a safe or live property will be presented, together with a decomposition into safe and live automata.