- 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

PhD Defense/Soutenance
by Jim Newton 14 Nov '18

14 Nov '18

Bonjour, It is my great pleasure to announce that my PhD defense will be held on Tuesday 20 November at EPITA at 10h00 in room KB 604. Everyone is welcome and invited as long as space is available in the room. Also please join the reception (pot) afterwards (12h30) to take place in room IP 12a. https://www.lrde.epita.fr/wiki/Affiche-these-JN <https://www.lrde.epita.fr/wiki/Affiche-these-JN> If you’d like to take a look at the thesis itself, it is available here temporarily until it reaches its final resting place. https://drive.google.com/drive/folders/14L7kFNNyIOv3e-apqDTynCRPPWwoY2bw <https://drive.google.com/drive/folders/14L7kFNNyIOv3e-apqDTynCRPPWwoY2bw> Representing and Computing with Types in Dynamically Typed Languages Extending Dynamic Language Expressivity to Accommodate Rationally Typed Sequences Abstract: We present code generation techniques related to run-time type checking of heterogeneous sequences. Traditional regular expressions can be used to recognize well defined sets of character strings called rational languages or sometimes regular languages. Newton et.al. present an extension whereby a dynamic language may recognize a well defined set of heterogeneous sequences, such as lists and vectors. As with the analogous string matching regular expression theory, matching these regular type expressions can also be achieved by using a finite state machine (deterministic finite automata, DFA). Constructing such a DFA can be time consuming. The approach we chose, uses meta-programming to intervene at compile-time, generating efficient functions specific to each DFA, and allowing the compiler to further optimize the functions if possible. The functions are made available for use at run-time. Without this use of meta-programming, the program might otherwise be forced to construct the DFA at run-time. The excessively high cost of such a construction would likely far outweigh the time needed to match a string against the expression. Our technique involves hooking into the Common Lisp type system via the deftype macro. The first time the compiler encounters a relevant type specifier, the appropriate DFA is created, which may be a exponential complexity operation, from which specific low-level code is generated to match that specific expression. Thereafter, when the type specifier is encountered again, the same pre-generated function can be used. The code generated is of linear complexity at run-time. A complication of this approach, which we explain in this report, is that to build the DFA we must calculate a disjoint type decomposition which is time consuming, and also leads to sub-optimal use of typecase in machine generated code. To handle this complication, we use our own macro optimized-typecase in our machine generated code. Uses of this macro are also implicitly expanded at compile time. Our macro expansion uses BDDs (Binary Decision Diagrams) to optimize the optimized-typecase into low level code, maintaining the typecasesemantics but eliminating redundant type checks. In the report we also describe an extension of BDDs to accomodate subtyping in the Common Lisp type system as well as an in-depth analysis of worst-case sizes of BDDs. Kind regards (soon to be Dr) Jim NEWTON

1 0

[CfP] 12th European Lisp Symposium, April 1-2 2019, Genova, Italy
by Didier Verna 31 Oct '18

31 Oct '18

ELS'19 - 12th European Lisp Symposium Hotel Bristol Palace Genova, Italy April 1-2 2019 In co-location with <Programming> 2019 Sponsored by EPITA http://www.european-lisp-symposium.org/2019/ The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. The 12th 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 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 2 pages for demonstrations of tools, libraries, and applications. Tutorials: Abstracts of up to 4 pages for in-depth presentations about topics of special interest for at least 90 minutes and up to 180 minutes. The symposium will also provide slots for lightning talks, to be registered on-site every day. 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 address: https://www.easychair.org/conferences/?conf=els2019 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. Important dates: - 01 Feb 2019 Submission deadline - 01 Mar 2019 Notification of acceptance - 18 Mar 2019 Final papers due - 01-02 Apr 2019 Symposium Programme chair: Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Programme committee: tba Search Keywords: #els2019, ELS 2019, ELS '19, European Lisp Symposium 2019, European Lisp Symposium '19, 12th ELS, 12th European Lisp Symposium, European Lisp Conference 2019, European Lisp Conference '19 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

ACM Transactions on Computational Logic
by Jim Newton 28 Aug '18

28 Aug '18

We are pleased to announce that we have had an article entitled Intuitive Analysis of Certain Binary Decision Diagrams accepted in ACM Transactions on Computational Logic. A link to the paper and abstract are given below. We’ll be happy to discuss the article if anyone is interested. Kind Regards Jim https://www.lrde.epita.fr/dload/papers/newton.18.tocl.pdf Abstract: Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean expressions, integrated circuit design, type inferencers, model checkers, and many other applications. Although the ROBDD is a lightweight data structure to implement, the behavior, in terms of memory allocation, may not be obvious to the program architect. We explore experimentally, numerically, and theoretically the typical and worst-case ROBDD sizes in terms of number of nodes and residual compression ratios, as compared to unreduced BDDs. While our theoretical results are not surprising, as they are in keeping with previously known results, we believe our method contributes to the current body of research by our experimental and statistical treatment of ROBDD sizes. In addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code.

1 0

Quickref open-sourced
by Didier Verna 07 Aug '18

07 Aug '18

Dear all, I'm happy to announce the first public release of Quickref, a global documentation project for Common Lisp. Quickref automatically builds a website[1] containing reference manuals for Quicklisp libraries (either those already installed or all of them). The reference manuals are generated by Declt[2] (probably the most complete documentation system for Lisp today) in Texinfo format, and then processed by makeinfo. Because Declt works by introspection, this whole process is non-intrusive: library authors do not need to do anything to support them being documented. The official Quickref website is kept up-to-date with Quicklisp, and currently documents 1588 libraries successfully. This work is the result of a collaboration with Antoine Martin, as part of an internship at LRDE. The project is still evolving: a new student will arrive in September to work on parallelization. The source code is available here: https://gitlab.common-lisp.net/quickref/quickref The resulting website may also be regenerated locally with this Docker 2-liner: docker run --name quickref quickref/quickref docker cp quickref:/home/quickref/quickref . Footnotes: [1] http://quickref.common-lisp.net [2] https://www.lrde.epita.fr/~didier/software/lisp/misc.php#declt -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Spot 2.6 released
by Alexandre Duret-Lutz 04 Jul '18

04 Jul '18

We are happy to announce the release of Spot 2.6. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). This release contains code contributed by Maximilien Colange, Antoine Martin, and myself. A detailed list of new features in this new release is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that the unstable Debian packages and stable RPM packages should be available within 24h. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.6 (2018-07-04) Command-line tools: - autfilt learned --is-colored to filter automata that use exactly one acceptance set per mark or transition. - autfilt learned --has-univ-branching and --has-exist-branching to keep automata that have universal branching, or that make non-deterministic choices. - autcross' tool specifications now have %M replaced by the name of the input automaton. - autcross now aborts if there is any parser diagnostic for the input automata (previous versions would use the input automaton whenever the parser would manage to read something). - ltlcross, ltldo, and autcross learned shorthands to call delag, ltl2dra, ltl2dgra, and nba2dpa. - When autfilt is asked to build a Büchi automaton from of a chain of many products, as in "autfilt -B --product 1.hoa ... --product n.hoa in.hoa" then it will automatically degeneralize the intermediate products to avoid exceeding the number of supported acceptance sets. - genltl learned to generate six new families of LTL formulas: --gf-equiv-xn=RANGE GF(a <-> X^n(a)) --gf-implies-xn=RANGE GF(a -> X^n(a)) --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j))) --sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn) --sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn) --sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] paper (range should be included in 1..3) - genltl --ms-example can now take a two-range argument, (as --sejk-f above). Build: - ./configure --enable-max-accsets=N let you specify a maximum number of acceptance sets that Spot should support. The default is still 32, but this limit is no longer hardcoded. Larger values will cost additional memory and time. - We know distribute RPM packages for Fedora 28. See file:///home/adl/git/spot/doc/userdoc/install.html#Fedora Library: - The PSL/LTL simplification routine learned the following: q R Xf = X(q R f) if q is suspendable q U Xf = X(q U f) if q is suspendable {SERE;1} = {1} if {SERE} accepts [*0] {SERE;1} = {SERE} if {SERE} does not accept [*0] - gf_guarantee_to_ba() is a specialized construction for translating formulas of the form GF(guarantee) to BA or DBA, and fg_safety_to_dca() is a specialized construction for translating formulas of the form FG(safety) to DCA. These are generalizations of some constructions proposed by J. Esparza, J. Křentínský, and S. Sickert (LICS'18). These are now used by the main translation routine, and can be disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, here are the size of deterministic transition-based generalized Büchi automata constructed from four GF(guarantee) formulas with two versions of Spot, and converted to other types of deterministic automata by other tools distributed with Owl 18.06. "x(y)" means x states and y acceptance sets. ltl2tgba -D delag ltl2dra 2.5 2.6 18.06 18.06 ------------------------- ----------- ------------- GF(a <-> XXa) 9(1) 4(1) 4(2) 9(4) GF(a <-> XXXa) 27(1) 8(1) 8(2) 25(4) GF(((a & Xb) | XXc) & Xd) 6(1) 4(1) 16(1) 5(2) GF((b | Fa) & (b R Xb)) 6(2) 2(1) 3(4) 3(4) Note that in the above the automata produced by 'ltl2tgba -D' in version 2.5 were not deterministic (because -D is only a preference). They are deterministic in 2.6 and other tools. - spot::product() and spot::product_or() learned to produce an automaton with a simpler acceptance condition if one of the argument is a weak automaton. In this case the resulting acceptance condition is (usually) that of the other argument. - spot::product_susp() and spot::product_or_susp() are new functions for building products between an automaton A and a "suspendable" automaton B. They are also optimized for the case that A is weak. - When 'generic' acceptance is enabled, the translation routine will split the input formula on Boolean operators into components that are syntactically 'obligation', 'suspendable', or 'something else'. Those will be translated separately and combined with product()/product_susp(). This is inspired by the ways things are done in ltl2dstar or delag, and can be disabled by passing option -xltl-split=0, as in ltl2tgba -G -D -xltl-split=0. Here are the sizes of deterministic automata (except for ltl3tela which produces non-deterministic automata) produced with generic acceptance using two versions of ltl2tgba and other tools for reference. ltl2tgba -DG delag ltl3tela 2.5 2.6 18.06 1.1.2 ------------ ------- -------- FGa0&GFb0 2(2) 1(2) 1(2) 1(2) (FGa1&GFb1)|FGa0|GFb0 16(6) 1(4) 1(4) 1(9) (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 29(8) 1(6) 1(6) 3(11) FGa0|GFb0 5(4) 1(2) 1(2) 1(5) (FGa1|GFb1)&FGa0&GFb0 8(4) 1(4) 1(4) 1(7) (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 497(14) 1(6) 1(6) 1(14) GFa1 <-> GFz 4(6) 1(3) 1(4) 1(7) (GFa1 & GFa2) <-> GFz 8(4) 1(3) 1(6) 3(10) (GFa1 & GFa2 & GFa3) <-> GFz 21(4) 1(4) 1(8) 3(13) GFa1 -> GFz 5(4) 1(2) 1(2) 1(5) (GFa1 & GFa2) -> GFz 12(4) 1(3) 1(3) 1(6) (GFa1 & GFa2 & GFa3) -> GFz 41(4) 1(4) 1(4) 1(7) FG(a|b)|FG(!a|Xb) 4(2) 2(2) 2(2) 2(3) FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21(2) 4(3) 4(3) 4(4) FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170(2) 8(4) 8(4) 8(5) - For 'parity' output, the 'ltl-split' optimization just separates obligation subformulas from the rest, where a determinization is still performed. ltl2tgba -DP ltl3dra ltl2dpa 2.5 2.6 0.2.3 18.06 -------------- ------- ------- FGp0 & (Gp1 | XFp2) 6(2) 4(1) 4(1) 4(2) G!p0 | F(p0 & (!p1 W p2)) 5(2) 4(2) n/a 5(2) (p0 W XXGp0) & GFp1 & FGp2 6(2) 5(2) n/a 6(3) (The above just show a few cases that were improved. There are many cases where ltl2dpa still produces smaller automata.) - The automaton postprocessor will now simplify acceptance conditions more aggressively, calling spot::simplify_acceptance() or spot::cleanup_acceptance() depending on the optimization level. - print_dot(), used to print automata in GraphViz's format, underwent several changes: * option "a", for printing the acceptance condition, is now enabled by default. Option "A", introduced in Spot 2.4, can be used to hide the acceptance condition in case you do not want it. This change of course affects the --dot option of all the command-line tools, as well as the various way to display automata using the Python bindings. * when option "1" is used to hide state names and force the display of state numbers, the actual state names is now moved to the "tooltip" field of the state. The SVG files produced by "dot -Tsvg" will show those as popups. This is also done for state labels of Kripke structures. * the output digraph is now named using the name of the automaton if available, or the empty string otherwise. (Previous versions used to call all digraphs "G".) This name appears as a tooltip in SVG figures when the mouse is over the acceptance condition. * a new option "u" hides "true states" behind "exiting transitions". This can be used to display alternating automata in a way many people expect. * a new option "K" cancels the effect of "k" (which uses state labels whenever possible). This is most useful when one want to force transition-labeling of a Kripke structure, where "k" is usually the default. - spot::twa_graph::merge_states() is a new method that merges states with the exact same outgoing edges. As it performs no reordering of the edges, it is better to call it when you know that the edges in the twa_graph are sorted (e.g. after a call to merge_edges()). - spot::twa_graph::purge_unreachable_states() now takes a function which is called with the new numbering of states. This is useful to update an external structure that references states of the twa that we want to purge. - spot::scc_filter() now automatically turns automata marked as inherently-weak into weak automata with state-based acceptance. The acceptance condition is set to Büchi unless the input had co-Büchi or t acceptance. spot::scc_filter_states() will pass inherently-weak automata to spot::scc_filter(). - spot::cleanup_parity() and spot::cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. - spot::contains() and spot::are_equivalent() can be used to check language containement between two automata or formulas. They are most welcome in Python, since we used to redefine them every now and them. Some examples are shown in https://spot.lrde.epita.fr/ipynb/contains.html - aut1->exclusive_word(aut2) is a new method that returns a word accepted by aut1 or aut2 but not both. The exclusive_run() variant will return. This is useful when comparing automata and looking for differences. See also https://spot.lrde.epita.fr/ipynb/contains.html - spot::complement_semidet(aut) is a new function that returns the complement of aut, where aut is a semideterministic automaton. The function uses the NCSB complementation algorithm proposed by F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). - spot::remove_alternation() was slightly improved on very-weak alternating automata: the labeling of the outgoing transitions in the resulting TGBA makes it more likely that simulation-based reductions will reduce it. - When applied to automata that are not WDBA-realizable, spot::minimize_wdba() was changed to produce an automaton recognizing a language that includes the original one. As a consequence spot::minimize_obligation() and spot::is_wdba_realizable() now only need one containement check instead of two. - Slightly improved log output for the SAT-based minimization functions. The CSV log files now include an additional column with the size of the reference automaton, and they now have a header line. These log files give more details and are more accurate in the case of incremental SAT-solving. Python: - New spot.jupyter package. This currently contains a function for displaying several arguments side by side in a Jupyter notebook. See https://spot.lrde.epita.fr/ipynb/alternation.html for some examples. - Strings are now implicitely converted into formulas when passed as arguments to functions that expect formulas. Previously this was done only for a few functions. - The Python bindings for sat_minimize() now have display_log and return_log options; these are demonstrated on the new https://spot.lrde.epita.fr/ipynb/satmin.html page. Bugs fixed: - Python *.py and *.so files are now always installed into the same directory. This was an issue on systems like Fedora that separate plateform-specific packages from non-plateform-specific ones. - print_dot() will correctly escape strings containing \n in HTML mode. - The HOA parser will now accept Alias: declarations that occur before AP:. - The option --allow-dups of randltl now works properly. - Converting generalized-co-Büchi to Streett using dnf_to_nca() could produce bogus automata if the input had rejecting SCCs. Deprecation notices: - The type spot::acc_cond::mark_t has been overhauled and uses a custom bit-vector to represent acceptance sets instead of storing everything in a "unsigned int". This change is to accomodate configure's --enable-max-accsets=N option and has several effect: * The following shortcuts are deprecated: acc_cond::mark_t m1 = 0U; acc_cond::mark_t m2 = -1U; instead, use: acc_cond::mark_t m1 = {}; acc_cond::mark_t m2 = acc_cond::mark_t::all(); * acc_cond::mark_t::value_t is deprecated. It is now only defined when --enable-max-accsets=32 (the default) and equal to "unsigned" for backward compatibility reasons. Backward incompatibilities: - Functions spot::parity_product() and spot::parity_product_or() were removed. The code was unused, hard to maintain, and bogus. - The output of print_dot() now include the acceptance condition. Add option "A" (supported since version 2.4) to cancel that. - Because genltl now supports LTL pattern with two argumens, using --format=%L may output two comma-separated integer. This is an issue if you used to produce CSV files using for instance: genltl --format='%F,%L,%f' ... Make sure to quote %L to protect the potential commas: genltl --format='%F,"%L",%f' ... - In Spot 2.5 and prior running "ltl2tgba --generic --det" on some formula would attempt to translate it as deterministic TGBA or determinize it into an automaton with parity acceptance. Version 2.5 introduced --parity to force parity acceptance on the output. This version finally gives --generic some more natural semantics: any acceptance condition can be used. -- Alexandre Duret-Lutz

1 0

[Seminaire-LRDE] Séminaire du LRDE le mercredi 4 juillet 2018: Jean-Michel Morel (École Normale Supérieure Paris-Saclay)
by Guillaume Tochon 27 Jun '18

27 Jun '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 Mercredi 4 juillet 2018 (11h--12h), Amphi IP11. 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-07-04 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 4 juillet 2018 : * 11h--12h: Y a-t-il une théorie de la détection des anomalies dans les images digitales? -- Jean-Michel Morel (École Normale Supérieure Paris-Saclay) https://sites.google.com/site/jeanmichelmorelcmlaenscachan/ Dans ce travail en collaboration avec Axel Davy, Mauricio Delbracio et Thibaud Ehret, je passerai en revue les classes d'algorithmes dont le but est de détecter des anomalies dans les images digitales. Ces détecteurs répondent au difficile problème de trouver automatiquement des exceptions dans des images de fond, qui peuvent être aussi diverses qu'un tissu ou une mammographie. Des méthodes de détection ont été proposées par milliers car chaque problème nécessite un modèle de fond différent. En analysant les approches existantes, nous montrerons que le problème peut être réduit à la détection d'anomalies dans les images résiduelles (extraites de l'image cible) dans lesquelles prédominent le bruit et les anomalies. Ainsi, le problème général et impossible de la modélisation d'un fond arbitraire est remplacé par celui de modèliser un bruit. Or un modèle de bruit permet le calcul de seuils de détection rigoureux. L'approche au problème peut donc être non supervisée et fonctionner sur des images arbitraires. Nous illustrerons l'usage de la théorie de détection dite a contrario, qui évite la sur-détection en fixant des seuils de détection prenant en compte la multiplicité des tests. -- Mathématicien de formation, docteur de l'Université Pierre et Marie Curie, Assistant à Marseille-Luminy, maître de conférences et professeur à l'Université Paris-Dauphine puis à l'ENS Cachan, JMM a fait ses premiers travaux sur les équations aux dérivées partielles non-linéaires et les méthodes variationnelles. Il s'est ensuite consacré au développement d'outils mathématiques pour le traitement et l'analyse d'images et la modélisation de la perception visuelle. 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. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

Séminaire des étudiants chercheurs : Mardi 3 juillet 2018 - Amphi 4
by Daniela Becker 22 Jun '18

22 Jun '18

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mardi 3 juillet 2018 à partir de 10h00 en Amphi 4 (KB). Les étudiants ING1 et ING2 présenteront le résultat de leurs travaux des derniers mois. Au programme : SPOT — BIBLIOTHEQUE DE MODEL CHECKING 10h00 Recherche de chemin acceptant bi-bande dans Spot – CLÉMENT GILLARD Nous proposons un algorithme de recherche de chemin acceptant bi-bande, qui vient compléter le test de vacuité bibande présenté l’an dernier, et nous permet de l’utiliser dans des applications plus concrètes. 10h30 Création d’une bibliothèque d’antichaîne – ARTHUR REMAUD Une antichaîne est un sous-ensemble d’éléments tous deux à deux incomparables. Les antichaînes sont utilisées dans la théorie des automates comme structures de données pour stocker des ensembles d’états. De nouveaux algorithmes ont été implémentés et évalués afin d’optimiser l’insertion dans une antichaîne. 11h00 Implémentation des transitions invisibles et transparentes dans Spot – VINCENT TOURNEUR Dans le domaine de la vérification formelle, la Réduction d’Ordre Partiel (ROP) est une méthode qui permet de réduire notablement la taille des structures de données utilisées pour représenter les différentes exécutions d’un programme. Pour vérifier des formules LTL en utilisant la ROP, il faut ajouter des vérifications supplémentaires pour ne pas omettre des exécutions qui modifient les valeurs des propositions atomiques de la formule. Nous expliquons le fonctionnement de deux méthodes qui résolvent ce problème et leurs implémentations dans Spot : les méthodes des transitions invisibles et transparentes. CLIMB — TRAITEMENT D’IMAGES EN LISP 13h30 SUBTYPEP : une implémentation de l’algorithme de Baker – LEO VALAIS SUBTYPEP est un prédicat du langage Common Lisp qui indique si un type est un sous-type d’un autre. Étant donné le système de typage du langage, il n’est pas toujours possible de donner de réponse. Les implémentations de cette fonction ayant souvent tendance à ne pas répondre, même lorsque c’est possible, Baker a publié un algorithme qu’il prétend plus efficace. Nous proposons ici une implémentation partielle de son algorithme et présentons ses avantages et ses inconvénients. OLENA — TRAITEMENT D’IMAGES GÉNÉRIQUE ET PERFORMANT 14h00 Optimisation d’une bibliothèque de traitement d’images – VIRGILE HIRTZ La bibliothèque de traitement d’images Pylene n’est pas conforme aux nouveaux standards et subit des pertes de performance. Nous présentons un nouveau design résolvant ces problèmes. 14h30 Intégration d’histogrammes dans l’algorithme NL-Mean pour le débruitage d’images – ALIONA DANGLA L’objectif principal de ce projet est d’incorporer l’information liée à la distribution statistique des couleurs grâce à l’utilisation d’histogrammes dans NL-Mean. Cela permet d’effectuer toute transformation qui n’affecte pas la forme des histogrammes et ajouter des régions qui auraient pu ne pas être prises en compte dans l’algorithme originel. 15h00 Segmentation automatique du coeur – YOUNES KHOUDLI Nous proposons ici une méthode de segmentation automatique, adaptée d’une méthode développée pour la segmentation du cerveau humain. -- Daniela Becker Responsable administrative du LRDE

1 0