Annonce

annonce@lrde.epita.fr

564 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

2 years

Paper accepted at FM 2023: Energy Problems in Finite and Timed Automata with Büchi Conditions

by Uli Fahrenberg

We are happy to announce that the following article has been accepted at the he 25th International Symposium on Formal Methods (FM 2023) to be held in Lübeck in March 2023: Energy Problems in Finite and Timed Automata with Büchi Conditions Sven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier Abstract: We show how to efficiently solve energy Büchi problems in finite weighted Büchi automata and in one-clock weighted timed Büchi automata; all our algorithms are implemented in a pipeline based on TChecker and Spot. Solving the latter problem is done by using the corner-point abstraction; the former problem is handled by a modified version of Bellman-Ford interleaved with Couvreur's algorithm. The paper is available at https://arxiv.org/abs/2205.04392

2 years

[CfP] 16th European Lisp Symposium, April 24-25, Amsterdam

by Didier Verna

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 16th European Lisp Symposium Call for Papers April 24-25, 2023 Startup Village, Amsterdam, Nederlands https://www.european-lisp-symposium.org/2023 Sponsored by EPITA, DIRO, MLPrograms, Franz Inc., and SISCOG ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Recent News ~~~~~~~~~~~ First keynote speaker announced: Gerald Jay Sussman, MIT, MA, USA Important Dates ~~~~~~~~~~~~~~~ - Submission deadline: February 26, 2023 - Author notification: March 26, 2023 - Final papers due: April 9, 2023 - Symposium: April 24-25, 2023 Scope ~~~~~ The European Lisp Symposium is a premier forum for the discussion and dissemination of all aspects of design, implementation, and application of any of the Lisp dialects, including Common Lisp, Scheme, Emacs Lisp, Clojure, Racket, ACL2, AutoLisp, ISLISP, Dylan, SKILL, Hy, Shen, Carp, Janet, uLisp, Picolisp, Gamelisp, TXR, and so on. We encourage everyone interested in Lisp to participate. The European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications, and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - context-, aspect-, domain-oriented and generative programming - macro-, reflective-, meta- and/or rule-based development approaches - language design and implementation - language integration, inter-operation, and deployment - development methodologies, support, and environments - educational approaches and perspectives - experience reports and case studies Technical Program ~~~~~~~~~~~~~~~~~ We invite submissions in the following forms. * Papers: technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. * Experience reports: papers of up to 6 pages describing a successful use of a Lisp dialect and/or analyzing obstacles that have kept it from working in practice. * Tutorials: abstracts of up to 4 pages for in-depth presentations about topics of special interest. * Demonstrations: abstracts of up to 4 pages for demonstrations of tools, libraries, and applications. All submissions should be formatted following the ACM SIGS guidelines and include ACM Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following link http://www.easychair.org/conferences/?conf=els2023. Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Programme Chair ~~~~~~~~~~~~~~~ Stefan Monnier, DIRO, Université de Montréal, Canada Programme Committee ~~~~~~~~~~~~~~~~~~~ Stefan Monnier, Université de Montréal, Canada Mark Evenson, RavenPack Marco Heisig, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Ioanna Dimitriou, Igalia S.L., Spain, Germany Robert Smith Mattias Engdegård Marc Feeley, Université de Montréal, Canada Marc Battyani, FractalConcept Alan Ruttenberg, National Center for Ontological Research, USA Nick Levine, Ravenbrook Ltd, UK Ludovic Courtès, Inria, France Matthew Flatt, University of Utah, USA Irène Durand, Université Bordeaux 1, France Jay McCarthy, Brigham Young University, USA Ambrose Bonnaire-Sergeant, Cisco Christopher League, Long Island University, NY, USA Local Chair ~~~~~~~~~~~ Breanndán Ó Nualláin, Machine Learning Programs, Nederlands -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

2 years, 1 month

LITES Journal Special Issue on Distributed Hybrid Systems

by Uli Fahrenberg

I am happy to announce the appearance today of a special issue of the Leibniz Transactions on Embedded Systems dedicated to distributed hybrid systems and edited by Alessandro Abate, Martin Fränzle and myself: https://ojs.dagstuhl.de/index.php/lites/issue/view/lites-v008-i002 Foreword abstract: This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume. The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G.~Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain. The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.

2 years, 3 months

[CfP] ELS 2023, 16th European Lisp Symposium, April 24-25, Amsterdam

by Didier Verna

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 16th European Lisp Symposium Call for Papers April 24-25, 2023 Startup Village, Amsterdam, Nederlands https://www.european-lisp-symposium.org/2023 Sponsored by EPITA and DIRO ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Important Dates ~~~~~~~~~~~~~~~ - Submission deadline: February 26, 2023 - Author notification: March 26, 2023 - Final papers due: April 9, 2023 - Symposium: April 24-25, 2023 Scope ~~~~~ The European Lisp Symposium is a premier forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp dialects, including Common Lisp, Scheme, Emacs Lisp, Clojure, Racket, ACL2, AutoLisp, ISLISP, Dylan, SKILL, Hy, Shen, Carp, Janet, uLisp, Picolisp, Gamelisp, TXR, and so on. We encourage everyone interested in Lisp to participate. The European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications, and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - context-, aspect-, domain-oriented and generative programming - macro-, reflective-, meta- and/or rule-based development approaches - language design and implementation - language integration, inter-operation and deployment - development methodologies, support and environments - educational approaches and perspectives - experience reports and case studies Technical Program ~~~~~~~~~~~~~~~~~ We invite submissions in the following forms. * Papers: technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. * Demonstrations: abstracts of up to 4 pages for demonstrations of tools, libraries, and applications. * Tutorials: abstracts of up to 4 pages for in-depth presentations about topics of special interest. All submissions should be formatted following the ACM SIGS guidelines and include ACM Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following link http://www.easychair.org/conferences/?conf=els2023. Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Programme Chair ~~~~~~~~~~~~~~~ Stefan Monnier, DIRO, Université de Montréal Canada Programme Committee ~~~~~~~~~~~~~~~~~~~ TBA Local Chair ~~~~~~~~~~~ Breanndán Ó Nualláin, Machine Learning Programs, Nederlands -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

2 years, 3 months

ELS 2023 is on track!

by Didier Verna

Dear collegues, I'm happy to announce that ELS 2023, the 16th European Lisp Symposium will be held in Amsterdam (and online) on April 24-25! A preliminary call for papers will follow soon. Stay tuned for updates. Best, -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

2 years, 4 months

Papiers acceptés

by Souheib Baarir

Hi every one, I'm happy to annonce the publication of the following papers : 1) In SETTA'2022 Title : Diversifying a parallel SAT solver with Bayesian Moment Matching Authors : V. Vallade, S.Nejati, J.Sopena, V. Ganesh and S. Baarir Abstract : In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores. The key insight underpinning our method is that Bayesian reasoning is a powerful way to guide the CDCL search procedure away from fruitless parts of the search space of a satisfiable Boolean formula, and towards those regions that are likely to contain satisfying assignments. 2) In VMCAI'2023 Title : CosySEL: Improving SAT Solving Using Local Symmetries Authors : S. Saouli , S. Baarir , C. Dutheillet and J. Devriendt Abstract : Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new tool, CosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of Local symmetries. We conduct our experiments on instances issued from the last ten sat competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems See you, Souheib.

2 years, 5 months

Soutenance de thèse de Michaël Roynard

by Michaël Roynard

Bonjour, J'ai l'honneur et le plaisir de vous inviter à ma soutenance de thèse intitulée "Programmation Générique en C++ Moderne pour le traitement d'image" qui aura lieu vendredi 04 novembre à 9h30 en Amphi 0 (Bâtiment Voltaire au rdc). Vous êtes également convié à prendre un pot qui aura lieu après la soutenance (en salle apprentissage 1 dans le bâtiment Paritalie au 3ème étage). Membres du jury --------- Rapporteurs: Pr. Benjamin Perret ESIEE / LIGM / Universié Gustave Eiffel Pr. Pascale Le Gall CentraleSupélec / Université Paris Saclay Examinateurs: Pr. Hugues Talbot CentraleSupélec / Université Paris Saclay Pr. Laurent Najman ESIEE / LIGM / Universié Gustave Eiffel Dr. Camille Kurtz LIPADE / SIP Lab / Université Paris Cité Dr. Joël Falcou LRI / Universié Paris Saclay Directeur de thèse: Pr. Thierry Géraud LRE / EPITA Encadrant: Dr. Edwin Carlinet LRE / EPITA --------- Résumé: --------- C++ est un langage de programmation multiparadigme qui permet au développeur initié de mettre au point des algorithmes de traitement d'images. La force de langage se base sur plusieurs aspects. C++ est haut-niveau, cela signifie qu'il est possible de développer des abstractions puissantes mélangeant plusieurs styles de programmation pour faciliter le développement. En même temps, C++ reste bas-niveau et peut pleinement tirer partie du matériel pour fournir un maximum de performances. Il est aussi portable et très compatible ce qui lui permet de se brancher à d'autres langages de haut niveau pour le prototypage rapide tel que Python ou Matlab. Un des aspects les plus fondamentaux où le C++ brille, c'est la programmation générique. La programmation générique rend possible le développement et la réutilisation de briques logiciel comme des objets (images) de différentes natures (types) sans avoir de perte au niveau performance. Néanmoins, il n'est pas trivial de concilier les aspects de généricité, de performance et de simplicité d'utilisation. Le C++ moderne (post-2011) amène de nouvelles fonctionnalités qui le rendent plus simple et plus puissant. Dans cette thèse, nous explorons en premier un aspect particulier du C++20 : les concepts, dans le but de construire une taxonomie des types relatifs au traitement d'images. Deuxièmement, nous explorons une autre fonctionnalité ajoutée au C++20 : les ranges (et les vues). Nous appliquons ce design aux algorithmes de traitement d'images et aux types d'image, dans le but résoudre les problèmes liés, notamment, à la difficulté qu'il existe pour customiser les algorithmes de traitement d'image. Enfin, nous explorons les possibilités concernant la façon dont il est possible de construire un pont entre du code C++ générique statique (compile-time) et du code Python dynamique (runtime). Nous fournissons une solution hybride et nous mesurons ses performances. Nous discutons aussi les pistes qui peuvent être explorées dans le futur, notamment celles qui concernent les technologies JIT. Étant donné ces trois axes, nous voulons résoudre le problème concernant la conciliation des aspects de généricité, de performance et de simplicité d'utilisation. --------- Abstract: --------- C++ is a multi-paradigm language that enables the initiated programmer to set up efficient image processing algorithms. This language strength comes from several aspects. C++ is high-level, which enables developing powerful abstractions and mixing different programming styles to ease the development. At the same time, C++ is low-level and can fully take advantage of the hardware to deliver the best performance. It is also very portable and highly compatible which allows algorithms to be called from high-level, fast-prototyping languages such as Python or Matlab. One of the most fundamental aspects where C++ really shines is generic programming. Generic programming makes it possible to develop and reuse bricks of software on objects (images) of different natures (types) without performance loss. Nevertheless, conciliating the aspects of genericity, efficiency, and simplicity is not trivial. Modern C++ (post-2011) has brought new features that made the language simpler and more powerful. In this thesis, we first explore one particular C++20 aspect: the concepts, in order to build a concrete taxonomy of image related types and algorithms. Second, we explore another addition to C++20, ranges (and views), and we apply this design to image processing algorithms and image types in order to solve issues such as how hard it is to customize/tweak image processing algorithms. Finally, we explore possibilities regarding how we can offer a bridge between static (compile-time) generic C++ code and dynamic (runtime) Python code. We offer our own hybrid solution and benchmark its performance as well as discuss what can be done in the future with JIT technologies. Considering those three axes, we will address the issue regarding the way to conciliate generic programming, efficiency and ease of use. --------- En espérant vous voir nombreux. A bientôt, -- Michaël ROYNARD PhD Student EPITA/LRE

2 years, 5 months

Spot 2.11.1 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.11.1 Spot is a C++17 library for handling of linear-time temporal logic formulas and omega automata. It comes with a set of command-line utilities (to automate various tasks) and Python binding for easy prototyping. Some applications are model-checking and reactive synthesis. Spot 2.11 is a major release containing new features and improvements implemented over the last 11 months by Florian Rankin, Philipp Schlehuber-Caissier, Antoine Martin, and myself. A detailled list of changes is appended to this email. Spot 2.11.1 fixes a couple of build issues discovered before I had time to announce 2.11... You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) had been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). The removal of "development", is nothing to worry about: we are still continuing to develop Spot as part of our research. However a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.1 (2022-10-10) Bugs fixed: - Fix a build issue preventing the update of website (issue #516). - Fix a compilation error with clang-14 on FreeBSD (issue #515). New in spot 2.11 (2022-10-08) Build: - configure will now diagnose situations where Python bindings will be installed in a directory that is not part of Python's search path. A new configure option --with-pythondir can be used to modify this installation path. (Issue #512) - A new configure option --enable-pthread enables the compilation of Spot with -pthread, and render available the parallel version of some algorithms. If Spot is compiled with -pthread enabled, any user linking with Spot should also link with the pthread library. In order to not break existing build setups using Spot, this option is currently disabled by default in this release. We plan to turn it on by default in some future release. Third-party project using Spot may want to start linking with -pthread in prevision for this change. Command-line tools: - autfilt has a new options --aliases=drop|keep to specify if the HOA printer should attempt to preserve aliases present in the HOA input. This defaults to "keep". - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html - ltlfilt has a new --sonf option to produce a formula's Suffix Operator Normal Form, described in [cimatti.06.fmcad]. The associated option --sonf-aps allows listing the newly introduced atomic propositions. - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). - ltlsynt has a new option --tlsf that takes the filename of a TLSF specification and calls syfco (which must be installed) to convert it into an LTL formula. - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. - ltlsynt has a new option --hide-status to hide the REALIZABLE or UNREALIZABLE output expected by SYNTCOMP. (This line is superfluous, because the exit status of ltlsynt already indicate whether the formula is realizable or not.) - ltlsynt has a new option --dot to request GraphViz output instead of most output. This works for displaying Mealy machines, games, or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for examples. - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba options. Those are used to generate pairs of automata that should include each other, and are used to show a regression (in speed) present in Spot 2.10.x and fixed in 2.11. - genltl learned --eil-gsi to generate a familly a function whose translation and simplification used to be very slow. In particular genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba was reported as taking 9 days. This is now instantaneous. Library: - The new function suffix_operator_normal_form() implements transformation of formulas to Suffix Operator Normal Form, described in [cimatti.06.fmcad]. - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected to recognize the same language. The "original-states" should be prefered property when that integer correspond to some actual state. - tgba_determinize() learned to fill the "original-classes" property. States of the determinized automaton that correspond to the same subset of states of the original automaton belong to the same class. Filling this property is only done on demand as it inccurs a small overhead. - sbacc() learned to take the "original-classes" property into account and to preserve it. - The HOA parser and printer learned to map the synthesis-outputs property of Spot to the controllable-AP header for the Extended HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 - The automaton parser learned to parse games in the PGSolver format. See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for an example. - "aliases" is a new named property that is filled by the HOA parser using the list of aliases declared in the HOA file, and then used by the HOA printer on a best-effort basis. Aliases can be used to make HOA files more compact or more readable. But another possible application is to use aliases to name letters of a 2^AP alphabet, in applications where using atomic propositions is inconvenient. - print_dot() learned option "@" to display aliases, as discussed above. - to_finite() is a new function that help interpreting automata build from LTLf formula using the from_ltlf() function. It replace the previously suggested method of removing and atomic proposition and simpifying automata, that failed to deal with states without successors. See updated https://spot.lrde.epita.fr/tut12.html - the HOA parser learned to not ignore self-loops labeled with [f] and to turn any state that have colors but no outgoing transitions into a state with a [f] self-loop. This helps dealing with automata containing states without successors, as in the output of to_finite(). - purge_dead_states() will now also remove edges labeled by false (except self-loops). - When parsing formulas with a huge number of operands for an n-ary operator (for instance 'p1 | p2 | ... | p1000') the LTL parser would construct that formula two operand at a time, and the formula constructor for that operator would be responsible for inlining, sorting, deduplicating, ... all operands at each step. This resulted in a worst-than-quadratic slowdown. This is now averted in the parser by delaying the construction of such n-ary nodes until all children are known. - complement() used to always turn tautological acceptance conditions into Büchi. It now only does that if the automaton is modified. - The zielonka_tree construction was optimized using the same memoization trick that is used in ACD. Additionally it can now be run with additional options to abort when the tree as an unwanted shape, or to turn the tree into a DAG. - contains() can now take a twa as a second argument, not just a twa_graph. This allows for instance to do contains(ltl, kripke) to obtain a simple model checker (that returns true or false, without counterexample). - degeneralize() and degeneralize_tba() learned to work on generalized-co-Büchi as well. - product() learned that the product of two co-Büchi automata is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. - spot::postprocessor has a new extra option "merge-states-min" that indicates above how many states twa_graph::merge_states() (which perform a very cheap pass to fuse states with identicall succesors) should be called before running simulation-based reductions. - A new function delay_branching_here(aut) can be used to simplify some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂) and (q₁,ℓ,M,q₃) differ only by their destination state, and are the only incoming transitions of their destination states, then q₂ and q₃ can be merged (taking the union of their outgoing transitions). This is cheap function is automatically called by spot::translate() after translation of a formula to GBA, before further simplification. This was introduced to help with automata produced from formulas output by "genltl --eil-gsi" (see above). - spot::postprocessor has new configuration variable branch-post that can be used to control the use of branching-postponement (disabled by default) or delayed-branching (see above, enabled by default). See the spot-x(7) man page for details. - spot::postprocessor is now using acd_transform() by default when building parity automata. Setting option "acd=0" will revert to using "to_parity()" instead. - to_parity() has been almost entirely rewritten and is a bit faster. - When asked to build parity automata, spot::translator is now more aggressively using LTL decomposition, as done in the Generic acceptance case before paritizing the result. This results in much smaller automata in many cases. - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only twa_graph::merge_states() supports it. Python bindings: - The to_str() method of automata can now export a parity game into the PG-Solver format by passing option 'pg'. See https://spot.lrde.epita.fr/ipynb/games.html for an example. Deprectation notice: - spot::pg_print() has been deprecated in favor of spot::print_pg() for consistency with the rest of the API. Bugs fixed: - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could produce unexpected result if begin and end where already pointing into the universal edge vector, since the later can be reallocated during that process. - Printing an alternating automaton with print_dot() using 'u' to hide true state could produce some incorrect GraphViz output if the automaton as a true state as part of a universal group. - Due to an optimization introduces in 2.10 to parse HOA label more efficiently, the automaton parser could crash when parsing random input (not HOA) containing '[' (issue #509).

2 years, 5 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, 6 months

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce