May 2022 - Annonce

Conférence GETCO
by Uli Fahrenberg 26 May '22

26 May '22

Bonjour, École polytechnique, LRDE and EPITA are organizing a scientific conference next week, "GETCO: Geometric and Topological Methods in Computer Science". See https://www.lix.polytechnique.fr/~smimram/getco22/ for program etc. Most talks will take place in Amphi 0, except for some parallel sessions in the afternoons which will be in KB404. Even if you are not registered, you're welcome to come and join us for some of the talks. Bien cordialement, for the organisers, Uli Fahrenberg, LRDE

1 0

Paper accepted at FORTE'22: LTL under reductions with weaker conditions than stutter invariance
by Renault Etienne 16 May '22

16 May '22

We are happy to announce that the following article has been accepted to the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22), one of the three conference of the 17th International Federated Conference on Distributed Computing Techniques (DisCoTec'22) to be held on June 13-17 in Lucca, Italy. (Philipp will go there to present the paper.) ====================================================================== LTL under reductions with weaker conditions than stutter invariance Emmanuel Paviot-Adet (1)(2), Denis Poitrenaud (1)(2), Etienne Renault (3), Yann Thierry-Mieg (1) (1) SorbonneUniversité,CNRS,LIP6,F-75005Paris,France (2) Université de Paris,F-75006Paris,France (3) LRDE, EPITA, France Verification of properties expressed as 𝜔-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. https://www.lrde.epita.fr/wiki/Publications/paviot.22.forte <https://www.lrde.epita.fr/wiki/Publications/paviot.22.forte>

1 0

Paper accepted at FORTE'22: Effective Reductions of Mealy Machines
by Alexandre Duret-Lutz 02 May '22

02 May '22

We are happy to announce that the following article has been accepted to the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22), one of the three conference of the 17th International Federated Conference on Distributed Computing Techniques (DisCoTec'22) to be held on June 13-17 in Lucca, Italy. (Philipp will go there to present the paper.) ====================================================================== Effective Reductions of Mealy Machines Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet LRDE, EPITA, France We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MeMin on a large collection of test cases made of well-known instances as well as new ones. https://www.lrde.epita.fr/wiki/Publications/renkin.22.forte ======================================================================

1 0