We are happy to announce the release of Spot 2.7
This release contains contributions by Maximilien Colange, Etienne
Renault, and myself. See below for a detailed list of new features.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.7 (2018-12-11)
Command-line tools:
- ltlsynt now has three algorithms for synthesis:
--algo=sd is the historical one. The automaton of the formula
is split to separate inputs and outputs, then
determinized (with Safra construction).
--algo=ds the automaton of the formula is determinized (Safra),
then split to separate inputs and outputs.
--algo=lar translate the formula to a deterministic automaton
with an arbitrary acceptance condition, then turn it
into a parity automaton using LAR, and split it.
In all three cases, the obtained parity game is solved using
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
been dropped as it was not used.
- ltlfilt learned --liveness to match formulas representing liveness
properties.
- the --stats= option of tools producing automata learned how to
tell if an automaton uses universal branching (%u), or more
precisely how many states (%[s]u) or edges (%[e]u) use universal
branching.
Python:
- spot.translate() and spot.postprocess() now take an xargs=
argument similar to the -x option of ltl2tgba and autfilt, making
it easier to fine tune these operations. For instance
ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0
would be written in Python as
spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
(Note: those extra options are documented in the spot-x(7) man page.)
- spot.is_generalized_rabin() and spot.is_generalized_streett() now return
a tuple (b, v) where b is a Boolean, and v is the vector of the sizes
of each generalized pair. This is a backward incompatible change.
Library:
- The LTL parser learned syntactic sugar for nested ranges of X
using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These
correspond to the next!, next_e!, and next_a! operators of PSL,
but we do not support those under these names currently.)
X[6]a = XXXXXXa
F[2:4]a = XX(a | X(a | Xa))
G[2:4]a = XX(a & X(a & Xa))
The corresponding constructors (for C++ and Python) are
formula::X(unsigned, formula)
formula::F(unsigned, unsigned, formula)
formula::G(unsigned, unsigned, formula)
- spot::unabbreviate(), used to rewrite away operators such as M or
W, learned to use some shorter rewritings when an argument (e) is
a pure eventuality or (u) is purely universal:
Fe = e
Gu = u
f R u = u
f M e = F(f & e)
f W u = G(f | u)
- The twa_graph class has a new dump_storage_as_dot() method
to show its data structure. This is more conveniently used
as aut.show_storage() in a Jupyter notebook. See
https://spot.lrde.epita.fr/ipynb/twagraph-internals.html
- spot::generic_emptiness_check() is a new function that performs
emptiness checks of twa_graph_ptr (i.e., automata not built
on-the-fly) with an *arbitrary* acceptance condition. Its sister
spot::generic_emptiness_check_scc() can be used to decide the
emptiness of an SCC. This is now used by
twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and
scc_info::determine_unknown_acceptance().
- The new function spot::to_parity() translates an automaton with
arbitrary acceptance condition into a parity automaton, based on a
last-appearance record (LAR) construction. (It is used by ltlsynt
but not yet by autfilt or ltl2tgba.)
- The new function is_liveness() and is_liveness_automaton() can be
used to check whether a formula or an automaton represents a
liveness property.
- Two new functions count_univbranch_states() and
count_univbranch_edges() can help measuring the amount of
universal branching in alternating automata.
Bugs fixed:
- translate() would incorrectly mark as stutter-invariant
some automata produced from formulas of the form X(f...)
where f... is syntactically stutter-invariant.
- acc_cond::is_generalized_rabin() and
acc_cond::is_generalized_streett() did not recognize the cases
were a single generalized pair is used.
- The pair of acc_cond::mark_t returned by
acc_code::used_inf_fin_sets(), and the pair (bool,
vector_rs_pairs) by acc_cond::is_rabin_like() and
acc_cond::is_streett_like() were not usable in Python.
- Many object types had __repr__() methods that would return the
same string as __str__(), contrary to Python usage where repr(x)
should try to show how to rebuild x. The following types have
been changed to follow this convention:
spot.acc_code
spot.acc_cond
spot.atomic_prop_set
spot.formula
spot.mark_t
spot.twa_run (__repr__ shows type and address)
spot.twa_word (likewise, but _repr_latex_ used in notebooks)
Note that this you were relying on the fact that Jupyter calls
repr() to display returned values, you may want to call print()
explicitely if you prefer the old representation.
- Fix compilation under Cygwin and Alpine Linux, both choking
on undefined secure_getenv().
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Vendredi 14 décembre 2018 (11h--12h), Amphi IP12A.
Vous trouverez sur le site du séminaire [1] les prochaines séances,
les résumés, captations vidéos et planches des exposés précédents [2],
le détail de cette séance [3] ainsi que le plan d'accès [4].
[1] http://seminaire.lrde.epita.fr
[2] http://seminaire.lrde.epita.fr/Archives
[3] http://seminaire.lrde.epita.fr/2018-12-14
[4] http://www.lrde.epita.fr/wiki/Contact
Au programme du Vendredi 14 décembre 2018 :
* 11h--12h: Toward myocardium perfusion from X-ray CT
-- Clara Jaquet (ESIEE Marne-la-Vallée)
Recent advances in medical image computing have resulted in automated
systems that closely assist physicians in patient therapy. Computational
and personalized patient models benefit diagnosis, prognosis and
treatment planning, with a decreased risk for the patient, as well as
potentially lower cost. HeartFlow Inc. is a successful example of a
company providing such a service in the cardiovascular context. Based on
patient-specific vascular model extracted from X-ray CT images, they
identify functionally significant disease in large coronary arteries.
Their combined anatomical and functional analysis is nonetheless limited
by the image resolution. At the downstream scale, a functional exam
called Myocardium Perfusion Imaging (MPI) highlights myocardium regions
with blood flow deficit. However, MPI does not functionally relate
perfusion to the upstream coronary disease. The goal of our project is
to build the functional bridge between coronary and myocardium. To this
aim we propose an anatomical and functional extrapolation. We produce an
innovative vascular network generation method extending the coronary
model down to the microvasculature. In the resulting vascular model, we
compute a functional analysis pipeline to simulate flow from large
coronaries to the myocardium, and to enable comparison with MPI
ground-truth data.
-- After completing a technological university degree in biology at
Creteil, Clara Jaquet obtained the diploma of biomedical engineer from
ISBS (Bio-Sciences Institute) in 2015. She worked for one year at
HeartFlow Inc, California, before starting a PhD at ESIEE, Université
Paris-Est, within the LIGM laboratory, on a research project jointly
with the same company.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible. N'hésitez pas à nous faire
parvenir vos suggestions d'orateurs.
--
Edwin Carlinet
Laboratoire R&D de l'EPITA (LRDE)
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/seminaire
Bonjour à tous,
J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée
``Prise en compte d'informations d'inclusion et d'adjacence dans les
représentations morphologiques hiérarchiques, avec application à
l'extraction de texte en images naturelles et vidéos.’’
Celle-ci aura lieu le jeudi 13 décembre 2018 à 10h00 en salle KB 604 à
l'EPITA
La soutenance sera suivie d'un pot.
https://www.lrde.epita.fr/wiki/Affiche-these-DH
Manuscrit de thèse
------------------
https://1drv.ms/b/s!AmbdUYjEYP52i8BOYRqHLImi0oykfQ
Composition du jury de thèse
----------------------------
Rapporteurs :
Beatriz MARCOTEGUI, Pr., MINES ParisTech, CMM
Hugues TALBOT, Pr., CentraleSupelec, CVC
Examinateurs :
Isabelle BLOCH, Pr., Telecom ParisTech, LTCI
Laurent NAJMAN , Pr., l'Université Paris-Est, LIGM
Camille KURTZ, MdC, Université Paris Descartes, LIPADE
Directeurs de thèse :
Thierry GÉRAUD, Pr., EPITA, LRDE
Yongchao XU, MdC, HUST, Chine, MCLab
Résumé de la thèse
------------------
With the rising need for a higher understanding of images, the
pixel-based representation is not enough. To answer this, the
mathematical morphology framework provides several multi-scale,
region-based image representations which include the hierarchies of
segmentation (e.g., alpha-tree, BPT) and trees based on the threshold
decomposition (Min/Max-trees and Tree of Shapes). Because objects in the
real world rarely appear in isolation but a typical context with other
related objects, we should consider the spatial relationships between
image regions.
We are interested in two type of relationship, namely the inclusion and
adjacency (in the sense of ``being nearby) since they usually carry
contextual information. The adjacency between regions gives us a sense
of how regions are arranged in images and have been widely used. On the
other hand, while fitting the human's perception of the
object-background relationship: the objects are included in their
background, the inclusion relationship is usually not taken into
account. Both these drastic information opens up possibilities for image
analysis. In this thesis, we take advantage of both inclusion and
adjacency information in morphological hierarchical representations for
computer vision applications.
We introduce the spatial alignment graph w.r.t inclusion (SAG) that is
constructed from both inclusion and spatial arrangement of regions in
the tree-based image representations.
For simple scenes, we introduce the Tree of Shapes of Laplacian sign. It
encodes the inclusion of 0-crossing of a Morphological Laplacian map and
performs well even in the case of uneven illumination. The ToSoL is
computed in linear time w.r.t the number of pixels thanks to an
optimization that mimics well-composedness. In this representation, the
spatial alignment graph is reduced to a disconnected graph where each
connected component is a semantic group of objects.
For higher detail representation, the spatial alignment graph becomes
more complex. To address this issue, we expand the idea of the shape
spaces morphology. Our expansion has two primary results: 1) It allows
the manipulation of any graph of shapes that encode different
information, which encompasses the SAG. 2) It allows any tree filtering
strategy proposed by the connected operators frameworks. Within this
expansion, the SAG could be analyzed with an alpha-tree.
We demonstrated the application aspect of our method in text detection.
The experiment results show the efficiency and effectiveness of our
methods, which robust to noise, blur, or uneven illumination. These
features are appealing to mobile applications.
