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