Annonce

annonce@lrde.epita.fr

543 discussions

by Uli Fahrenberg

The following paper has been accepted at the 33rd International Conference on Concurrency Theory (CONCUR 2022), to be held in Warsaw next week: A Kleene Theorem for Higher-Dimensional Automata Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański (LR(D)E, NTNU Gjøvik, U of Sheffield, Warsaw U) We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

1 year, 7 months

article accepted: The 34th Symposium on Implementation and Application of Functional Languages

by Jim Newton (lrde)

Hi, I’m pleased to announce I’ve had a paper accepted for presentation at The 34th Symposium on Implementation and Application of Functional Languages (https://ifl22.github.io <https://ifl22.github.io/>). The paper is entitled: How to fold and color a map: Comparing Use-Cases of Tree-Fold vs Fold-Left. You may view the article here https://drive.google.com/file/d/1-65beERt9UylSmxgsWe-gcl3Hz8JvjzC/view?usp=… as it is not yet available on /lrde/doc, pending an IT issue. ABSTRACT In this article we examine some consequences of computation order of two different conceptual implementations of the fold function. We explore a set of performance- and accuracy-based experiments on two implementations of this function. In particular, we contrast the traditional fold-left implementation with another approach we refer to as tree-fold. It is often implicitly supposed that the binary operation in question has constant complexity. We explore several application areas which diverge from that assumption: rational arithmetic, floating-point arithmetic, and Binary Decisions Diagram construction. These are binary operations which degrade in performance as the fold iteration progresses. We show that these types of binary operations are good candidates for tree-fold. Kind regards Jim

1 year, 8 months

Quickref 4.0b1 is out

by Didier Verna

Dear all, following the recent release of Declt 4.0, I'm happy to announce that Quickref 4.0 is on its way too, resulting in an update of the official website (https://quickref.common-lisp.net/), which now contains automatically generated documentation for 2110 Common Lisp libraries. The Docker images are up to date too. More details here: https://www.didierverna.net/blog/index.php?post/2022/05/26/Quickref-4.0-bet… -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 year, 10 months

Declt 4.0 beta 1 is released

by Didier Verna

Dear all, I'm happy to announce the release of Declt 4.0 beta 1. Although tagged as a beta version, this release is stable and constitutes the first of three steps in a major infrastructure overhaul. Declt is the rendering engine behind Quickref, a website providing automatic documentation for more than two thousand Common Lisp libraries. The long list of fixes, improvements, and new features in this release is proved here: https://www.didierverna.net/blog/index.php?post/2022/05/10/Declt-4.0-beta-1… For more information on Declt / Quickref: https://www.lrde.epita.fr/~didier/software/lisp/typesetting.php The Quickref website: https://quickref.common-lisp.net/ -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 year, 10 months

sortie de mon essai "Données, Transparence et Démocratie"

by Olivier Ricou

Bonjour, Je suis heureux de vous annoncer la sortie de mon essai Données, Transparence et Démocratie http://opendata.ricou.eu.org/ Je pars du fait que notre système politique va mal et que la confiance en nos institutions est faible. Un remède me semble être de donner à chacun les outils pour vérifier les actions de l'État et pour participer. Cela passe par la transparence, dans notre cas l'ouverture des données publiques, et par la prise en compte des retours des citoyens. L'ouverture des données publiques est inscrite dans la loi depuis 2016 mais elle a du mal à se mettre en place, pour des raisons techniques et politiques. Elle peut aussi être ralentie par le sentiment d'inutilité lorsque des données publiées ne trouvent pas leur public. Aussi le but de mon essai est de souligner l'importance de cette ouverture et de pousser chacun d'entre nous à exploiter ces données dans un but personnel ou pour le bien public. Cette ouverture offre aussi de nombreuses opportunités économiques et sociales que je présente dans ce livre. N'hésitez pas à me faire part de vos impressions ou remarques, par mail ou sur mon fil Twitter @egeopol https://twitter.com/egeopol Olivier Ricou.

1 year, 10 months

New publication: "From Spot 2.0 to Spot 2.10: What's New?" (CAV'22)

by Alexandre Duret-Lutz

We are happy to announce that the following article has been accepted to the 34th International Conference on Computer Aided Verification (CAV'22) to be held in Haifa, Israel, in August 7-10, 2022. ====================================================================== From Spot 2.0 to Spot 2.10: What's New? Alexandre Duret-Lutz¹ Étienne Renault¹ Maximilien Colange² Florian Renkin¹ Alexandre Gbaguidi Aisse² Philipp Schlehuber-Caissier¹ Thomas Medioni² Antoine Martin¹ Jérôme Dubois¹ Clément Gillard² Henrich Lauko² ¹LRDE, EPITA, France ²previously at LRDE Spot is a C++17 library for LTL and ω-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support ω-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata. https://www.lrde.epita.fr/wiki/Publications/duret.22.cav ======================================================================

1 year, 10 months

Conférence GETCO

by Uli Fahrenberg

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 year, 10 months

Paper accepted at FORTE'22: LTL under reductions with weaker conditions than stutter invariance

by Renault Etienne

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 year, 11 months

Paper accepted at FORTE'22: Effective Reductions of Mealy Machines

by Alexandre Duret-Lutz

1 year, 11 months

Paper accepted at TACAS'22: Practical Applications of the ACD

by Alexandre Duret-Lutz

We are happy to announce that the following article has been accepted to the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22) to be held in Munich in April 2022. ====================================================================== Practical Applications of the Alternating Cycle Decomposition Antonio Casares¹, Alexandre Duret-Lutz², Klara J. Meyer³, Florian Renkin², and Salomon Sickert⁴ ¹LaBRI, Universitée de Bordeaux, France ²LRDE, EPITA, France ³Independent Researcher ⁴School of Computer Science and Engineering, The Hebrew Univ., Israel In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot, and adapt it to the framework of Emerson-Lei automata, i.e., ω-automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of Emerson-Lei automata into parity automata with strong optimality guarantees: the resulting parity automaton is minimal among those automata that can be obtained by duplication of states. Our empirical results show that this transformation is usable in practice. Further, we show how the ACD can generalize many other specialized constructions such as deciding typeness of automata and degeneralization of generalized Büchi automata, providing a framework of practical algorithms for ω-automata. https://www.lrde.epita.fr/wiki/Publications/casares.22.tacas ======================================================================

2 years, 2 months

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce