IRIF, 8 place Aurélie Nemours (bâtiment Sophie Germain) dans le 13ème (RER C & ligne 14 : arrêt Bibliothèque François Mitterrand; Tram T3a : arrêt Avenue de France; Bus 62 & 89 : arrêt Porte de France).
Comme l’accès à l’IRIF est badgé, je propose de vous attendre en bas du bâtiment, je serai là dès 13:40. On montera au 3ème étage ensemble vers 13:55.
Abstract : The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the interval-based semantics of MTL is strictly more expressive than the pointwise one. These results may suggest that enabling the evaluation of formulae at arbitrary time points instead of positions of timed events increases the expressive power of MTL. In this paper, we formally argue otherwise. We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable. We then propose a new mixed semantics that embeds both the pointwise and the interval-based ones.
Abstract : Joint work with Hugo Férée and Giovanni Bernardi. The must-preorder is a liveness-preserving contextual refinement, whose definition does not directly entail a general proof method. The literature presents at least ten proof methods, depending on whether communication is synchronous or asynchronous, on whether there is value-passing or not. Moreover there are three approaches to define these proof methods: à la Hennessy, De Nicola, and Hoare. This ad-hoc development of the theory suggests a lack of understanding of the properties necessary and sufficient to reason on the must-preorder, and hinders the development of tools. To abandon ad-hoc methods, this paper presents three proof methods (one for each approach) that subsume the ten results from the literature, that cover five new cases, and that let us arrive at a novel proof method for asynchronous CCS with value-passing. We achieve this generality via three techniques: an axiomatic treatment of LTSs à la Selinger, a parametric treatment of non-blocking actions, and the novel notion of label abstraction, which captures the essence of correct substitutivity w.r.t. program progress. As use cases, we apply our proof methods to prove that two forms of code-hoisting are liveness-preserving. Our proofs are constructive and entirely mechanised in Rocq.