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
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
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
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.
