Annonce September 2022

annonce@lrde.epita.fr

3 participants
4 discussions

Paper published in Information & Computation

by Uli Fahrenberg

The following paper has been published in Information & Computation: Posets With Interfaces as a Model for Concurrency Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternativelytaking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures. https://www.lrde.epita.fr/wiki/Publications/fahrenberg.22.iandc

1 year, 10 months

Soutenance de thèse de Florian Renkin

by Florian Renkin

Bonjour, J'ai le plaisir de vous inviter à la soutenance (en français) de ma thèse intitulée : "Transformations d'ω-automates pour la synthèse de contrôleurs réactifs". Vous êtes également cordialement invité au pot qui suivra. Version web : https://www.lrde.epita.fr/~frenkin/thesis.php Date Vendredi 7 octobre, 9h30 Lieu Amphi 401, 14-16 rue Voltaire, Le Kremlin-Bicêtre 94270 Jury _Rapporteurs_ * Olivier Carton, Université Paris Cité * Nicolas Markey, Université de Rennes _Examinateurs_ * Hanna Klaudel, Université d'Évry * Laure Petrucci, Université Sorbonne Paris Nord * Nathalie Sznajder : Sorbonne Université _Encadrants_ * Alexandre Duret-Lutz, EPITA * Adrien Pommellet, EPITA Résumé Le travail de cette thèse s'inscrit dans le cadre de la création de manière automatique de systèmes corrects à partir de spécifications, ce que l'on appelle "synthèse". Ce besoin de création automatique vient d'une part de la complexité de plus en plus importante des systèmes que l'on crée mais aussi de la difficulté de vérifier si un système est correct. Pour que la synthèse soit utilisable en pratique, y compris dans l'industrie, il faut être capable de produire des solutions pour des problèmes plus ou moins complexes en un temps raisonnable. De plus, on peut chercher à optimiser les systèmes produits afin qu'ils soient les plus simples possibles. Pour décrire les contraintes que le système doit respecter, nous utiliserons des formules de logique linéaire temporelle (LTL) qui ajoutent aux opérateurs Booléens traditionnels une notion de temps discret afin d'exprimer des contraintes telles que "il existera un instant où la variable sera vraie". Dans notre cas, il s'agira de produire un contrôleur réactif, c'est-à-dire associant à une suite d'assignations de variables Booléennes d'entrées une suite d'assignations de variables Booléennes de sorties. L'approche de la synthèse LTL que nous allons décrire consiste à : (1) Traduire la spécification LTL en un jeu de parité où un joueur contrôle l'environnement alors que le second représente les actions que peut faire le contrôleur. (2) Rechercher dans ce jeu s'il existe une stratégie gagnante pour le second joueur. (3) Cette stratégie indique les actions que doit faire le contrôleur pour respecter les spécifications et il reste alors à l'encoder sous la forme voulue (circuit, programme, …). Une partie de la première étape est une procédure dite de paritisation consistant à obtenir à partir d'un automate quelconque un automate de parité. Une contribution majeure de cette thèse consiste en l'amélioration de cette procédure. Dans cette optique, nous proposons et comparons divers algorithmes de paritisation. La première méthode est une combinaison d'algorithmes existants auxquels ont été associées des heuristiques mais aussi de nouveaux algorithmes. La seconde est l'adaptation d'une méthode introduite en 2021 par Casares _et al._ assurant une forme d'optimalité sur la taille de l'automate de parité obtenu. Dans les deux cas, ces algorithmes ont à la fois pour objectif de réduire le temps nécessaire pour une telle transformation mais aussi de limiter la taille de l'automate créé. Une autre contribution consiste à proposer des techniques de simplification du contrôleur. En particulier, nous tirerons parti des libertés offertes par la spécification. Par exemple, si l'on souhaite un système allumant une ampoule lorsqu'une présence est détectée, alors ce qu'il faut faire lorsque personne n'est détecté n'a pas d'importance. Pour obtenir un système simple, on peut décider de toujours allumer l'ampoule et le système n'a alors plus besoin d'un capteur. Deux types de simplifications seront décrites. La première est inspirée d'un outil existant (MeMin) et utilise un SAT-solver pour obtenir une solution minimale. La complexité de la recherche d'optimalité (NP-complet) nous incite également à nous tourner vers une seconde méthode basée sur les BDD visant à fournir un système réduit plus rapidement mais sans garantie d'optimalité. Ces deux contributions majeures ont été intégrées à l'outil ltlsynt distribué avec la bibliothèque Spot et ont été accompagnées de plusieurs améliorations que nous évaluons : une décomposition du problème permettant de créer des contrôleurs pour des sous-parties de la spécification mais aussi une méthode permettant de s'affranchir de la construction d'un jeu pour une certaine classe de formules. Ces travaux ont fait l'objet de publications dans les conférences ATVA'19 (première méthode de paritisation), TACAS'22 (seconde méthode de paritisation), FORTE'22 (simplification de contrôleur), CAV'22 (présentation des évolutions de Spot) ainsi que d'une présentation de ltlsynt lors de la conférence SYNT'21. L'outil ltlsynt a par ailleurs participé aux éditions 2020, 2021 et 2022 de la Syntcomp. A bientôt, Florian Renkin

2 years, 4 months

[CfP] ICCQ 2023 - 3rd International Conference on Code Quality

by Didier Verna

ICCQ 2023 https://www.iccq.ru/2023.html Sat 22 Apr 2023, St. Petersburg, Russia Due to the pandemic situation, the conference will be held in online mode: all speakers will present their work remotely over Zoom. The Third International Conference on Code Quality (ICCQ) is a one-day computer science event focused on static and dynamic analysis, program verification, programming languages design, software bug detection, and software maintenance. ICCQ is organized in cooperation with IEEE Computer Society. Program Committee ================= Andrey Terekhov (Chair), SPbU Alexandre Bergel, University of Chile Laura M. Castro, Universidade da Coruña Stephen Chang, UMass Boston Daniele Cono D’Elia, Sapienza University of Rome Pierre Donat-Bouillud, Czech Technical University Bernhard Egger, Seoul National University Sebastian Erdweg, Johannes Gutenberg University Mainz Samir Genaim, Universidad Complutense de Madrid Shachar Itzhaky, Technion Yusuke Izawa, Tokyo Institute of Technology Ranjit Jhala, University of California, San Diego Tetsuo Kamina, Oita University Christoph Kirsch, University of Salzburg Yu David Liu, Binghamton University Wolfgang de Meuter, Vrije Universiteit Brussel Antoine Miné, Sorbonne Université Guillermo Polito, CRIStAL Xuehai Qian, University of Southern California Junqiao Qiu, Michigan Technological University Yann Régis-Gianas, Nomadic Labs Yudai Tanabe, Tokyo Institute of Technology Tachio Terauchi, Waseda University Didier Verna, EPITA David West, New Mexico Highlands University Guannan Wei, Purdue University Vadim Zaytsev, University of Twente Important Dates =============== Paper/abstract submission: 18 Dec 2022 (anywhere on Earth) Author notification: 1 Mar 2023 Camera-ready submissions: 25 Mar 2023 Conference: 22 Apr 2023 Call for Papers =============== Papers will be published in the Proceedings of ICCQ and submitted for inclusion into IEEE Xplore subject to meeting their scope and quality requirements; to be indexed by Web of Science, Scopus, Google Scholar, DBLP, and others. We consider the following criteria when evaluating papers: Novelty: The paper presents new ideas and results and places them appropriately within the context established by previous research. Importance: The paper contributes to the advancement of knowledge in the field. We also welcome papers that diverge from the dominant trajectory of the field. Evidence: The paper presents sufficient evidence supporting its claims, such as proofs, implemented systems, experimental results, statistical analyses, case studies, and anecdotes. Clarity: The paper presents its contributions, methodology and results clearly. Papers will be reviewed by at least three PC members using a double-blind review process. Instructions for Authors ======================== Submissions must be in PDF, printable in black and white on US Letter sized paper. All submissions must adhere to the acmart sigplan template (two columns, 11pt font size). Compile it with this header: \documentclass[sigplan,11pt,nonacm=true]{acmart} \settopmatter{printfolios=false,printccs=false,printacmref=false} Submitted papers must be at least 4 and at most 16 pages long, including bibliographical references and appendices. Submissions that do not meet the above requirements will be rejected without review. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

2 years, 4 months

Paper accepted at CONCUR'22

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.

2 years, 4 months

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce September 2022