April 2013 - Annonce

Publication: Spin'13: Compositional Approach to Suspension and Other Improvements to LTL Translation
by Alexandre Duret-Lutz 28 Apr '13

28 Apr '13

We are happy to announce that the following paper has been accepted for publication at the 20th International SPIN Symposium on Model Checking of Software (SPIN'13) that will take place in Stony Brook, NY, USA on 8-9 July 2013. Compositional Approach to Suspension and Other Improvements to LTL Translation Tomáš Babiak (1), Thomas Badie (2), Alexandre Duret-Lutz (2), Mojmír Křetínský (1), and Jan Strejček (1) (1) Faculty of Informatics, Masaryk University, Brno, Czech Republic (2) LRDE, EPITA, Kremlin-Bicêtre, France http://publis.lrde.epita.fr/201307-Spin Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton. -- Alexandre Duret-Lutz

1 0

Spot 1.1 released
by Alexandre Duret-Lutz 28 Apr '13

28 Apr '13

We are pleased to announce the release of Spot 1.1. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. This release features several improvements developped with our collegues from the Mazaryk University (also authors of the ltl3ba translator) as detailed in the following paper: Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček: Compositional Approach to Suspension and Other Improvements to LTL Translation. To appear in the proceedings of SPIN'13. You can find the new release here: http://spot.lip6.fr/dl/spot-1.1.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>. New in spot 1.1 (2013-04-28): * New features in the library: - The postprocessor class now takes an optional option_map argument that can be used to specify fine-tuning options, making it easier to benchmark different scenarios while developing new postprocessings. - A new translator class implements a complete translation chain, from LTL/PSL to TGBA/BA/Monitor. It performs pre- and post-processings in addition to the core translation, and offers an interface similar to that used in the postprocessor class, to specify the intent of the translation. - The degeneralization algorithm has learned three new tricks: level reset, level caching, and SCC-based ordering. The former two are enabled by default. Benchmarking has shown that the latter one does not always have a positive effect, so it is disabled by default. (See SPIN'13 paper.) - The scc_filter() function, which removes dead SCCs and also simplify acceptance conditions, has learnt how to simplify acceptance conditions in a few tricky situations that were not simplified previously. (See SPIN'13 paper.) - An experimental "don't care" (direct) simulation has been implemented. This simulations consider the acceptance of out-of-SCC transitions as "don't care". It is not enabled by default because it currently is very slow. - remove_x() is a function that take a formula, and rewrite it without the X operator. The rewriting is only correct for stutter-insensitive LTL formulas (See K. Etessami's paper in IFP vol. 75(6). 2000) This algorithm is accessible from the command-line using ltlfilt's --remove-x option. - is_stutter_insensitive() takes any LTL formula, and check whether it is stutter-insensitive. This algorithm is accessible from the command-line using ltlfilt's --stutter-insensitive option. - A new translation, called compsusp(), for "Compositional Suspension" is implemented on top of ltl_to_tgba_fm(). (See SPIN'13 paper.) - Some experimental LTL rewriting rules that trie to gather suspendable formulas are implemented and can be activated with the favor_event_univ option of ltl_simplifier. As always please check doc/tl/tl.tex for the list of rules. - Several functions have been introduced to check the strength of an SCC. is_inherently_weak_scc() is_weak_scc() is_syntactic_weak_scc() is_complete_scc() is_terminal_scc() is_syntactic_terminal_scc() Beware that the costly is_weak_scc() function introduced in Spot 1.0, which is based on a cycle enumeration, has been renammed to is_inherently_weak_scc() to match established vocabulary. * Command-line tools: - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x) flag to fine-tune the algorithms used. The available options are documented in the spot-x (7) manpage. For instance use '-x comp-susp' to use the afore-mentioned compositional suspension. - The output format of 'ltlcross --json' has been changed slightly. In a future version we will offer some reporting script that turn such JSON output into various tables and graphs, and these change are required to make the format usable for other benchmarks (not just ltlcross). - ltlcross will now count the number of non-accepting, terminal, weak, and strong SCCs, as well as the number of terminal, weak, and strong automata produced by each tool. * Documentation: - org-mode files used to generate the documentation about command-line tools (shown at http://spot.lip6.fr/userdoc/tools.html) is distributed in doc/org/. The resulting html files are also in doc/userdoc/. * Bug fixes: - There was a memory leak in the LTL simplification code, that could only be triggered when disabling advanced simplifications. - The translation of the PSL formula !{xxx} was incorrect when xxx simplified to false. - Various warnings triggered by new compilers. -- Alexandre Duret-Lutz

1 0

New journal publication
by Guillaume Lazzara 25 Apr '13

25 Apr '13

We are happy to announce that the following paper has been accepted for publication in the International Journal of Document Analysis and Recognition (IJDAR): Guillaume Lazzara (1) and Thierry Géraud (1) Efficient Multiscale Sauvola's Binarization http://publis.lrde.epita.fr/201302-IJDAR (1) EPITA Research and Development Laboratory (LRDE) This work is focused on the most commonly used binarization method: Sauvola's. It performs relatively well on classical documents. However, three main defects remain : the window parameter of Sauvola's formula do not fit automatically to the content; it is not robust to low contrasts; it is non-invariant with respect to contrast inversion. Thus, on documents such as magazines, the content may not be retrieved correctly which is crucial for indexing purpose. In this paper, we describe how to implement an efficient multiscale implementation of Sauvola's algorithm in order to guarantee good binarization for both small and large objects inside a single document without adjusting the window size to the content. We also describe on how to implement it in an efficient way, step by step. Pixel-based accuracy and OCR evaluations are performed on more than 120 documents. This implementation remains notably fast compared to the original algorithm. For fixed parameters, text recognition rates and binarization quality are equal or better than other methods on small and medium text and is significantly improved on large text. Thanks to the way it is implemented, it is also more robust on textured text and on image binarization. This implementation extends the robustness of Sauvola's algorithm by making the results almost insensible to the window size whatever the object sizes. Its properties make it usable in full document analysis toolchains. -- Guillaume Lazzara EPITA Research and Development Laboratory (LRDE) 14-16 rue Voltaire F-94276 Le Kremlin-Bicetre France phone +33 1 53 14 59 39 - fax +33 1 53 14 59 22

1 0

[Seminaire-LRDE] Mercredi 24 avril 2013: Peter Van Roy, Université catholique de Louvain
by Daniela Becker 03 Apr '13

03 Apr '13

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 24 avril 2013 (11--12h), Salle L-Alpha du LRDE. Au programme: * 11h: Designing robust distributed systems with weakly interacting feedback structures -- Peter Van Roy, Université catholique de Louvain http://www.info.ucl.ac.be/~pvr/WIFSpaper.pdf Large distributed systems on the Internet are subject to hostile environmental conditions such as node failures, erratic communications, and partitioning, and global problems such as hotspots, attacks, multicast storms, chaotic behavior, and cascading failures. How can we build these systems to function in predictable fashion in such situations as well as being easy to understand and maintain? In our work on building self-managing systems in the SELFMAN project, we have discovered a useful design pattern for building complex systems, namely as a set of Weakly Interacting Feedback Structures (WIFS). A feedback structure consists of a graph of interacting feedback loops that together maintain one global system property. We give examples of biological and computing systems that use WIFS, such as the human respiratory system and the TCP family of network protocols. We then show the usefulness of the design pattern by applying it to the Scalaris key/value store from SELFMAN. Scalaris is based on a structured peer-to-peer network with extensions for data replication and transactions. Scalaris achieves high performance: from 4000 to 14000 read-modify-write transactions per second on a cluster with 1 to 15 nodes each containing two dual-core Intel Xeon processors at 2.66 GHz. Scalaris is a self-managing system that consists of five WIFS, for connectivity, routing, load balancing, replication, and transactions. We conclude by explaining why WIFS are an important design pattern for building complex systems and we outline how to extend the WIFS approach to allow proving global properties of these systems. -- Peter Van Roy is coauthor of the classic programming textbook "Concepts, Techniques, and Models of Computer Programming" and professor at the Université catholique de Louvain in Belgium. His group hosts the Mozart Programming System (see www.mozart-oz.org) with which he explores the relationship between programming languages and distributed programming. He wrote the Aquarius Prolog compiler, the first to generate code competitive in performance with C compilers. He received a M.S. and Ph.D. in Computer Science from the University of California at Berkeley and a French "Habilitation à Diriger des Recherches" from the Université Paris Diderot. !!! Attention !!! La session prévue le 10 avril 2013 sur les "Langages de développement et sécurité --- Mind your language" par Eric Jaeger et Olivier Levillain (ANSSI) est reportée au Mercredi 29 mai 2013. Et le 22 mai Basile Starynkevitch, CEA LIST, montrera comment "Etendre le compilateur GCC avev MELT". Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://www.lrde.epita.fr/mailman/listinfo/seminaire

1 0