December 2018 - Annonce

Spot 2.7 released
by Alexandre Duret-Lutz 11 Dec '18

11 Dec '18

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

1 0

[Seminaire-LRDE] Vendredi 14 décembre 2018: Clara Jaquet (ESIEE Marne-la-Vallée)
by Edwin Carlinet 10 Dec '18

10 Dec '18

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

1 0

Soutenance de ma thèse
by dhuynh 04 Dec '18

04 Dec '18

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.

1 0