October 2022 - Annonce

Paper published in Information & Computation
by Uli Fahrenberg 05 Mar '23

05 Mar '23

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 2

Soutenance de thèse de Michaël Roynard
by Michaël Roynard 26 Oct '22

26 Oct '22

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

1 0

Spot 2.11.1 released
by Alexandre Duret-Lutz 10 Oct '22

10 Oct '22

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

1 0