CSI Seminar 2017-07-04

Laboratoire de Recherche et Développement de l’EPITA Séminaire des étudiants-chercheurs 4 July 2017 10h00-16h15, Salle L0 http://www.lrde.epita.fr EPITA / LRDE 14-16 rue Voltaire 94276 Le Kremlin-Bicêtre

Spot

10h00 A co-Büching Toolbox – Alexandre Gbaguidi Aïsse

Thanks to the HOA format there are less and less barriers between '"`UNIQ--math-00000005-QINU`"'-automata with different acceptance conditions. Spot, a library for '"`UNIQ--math-00000006-QINU`"'-automata manipulation, supports arbitrary acceptance condition and performs some conversions between them. We augmented the set of supported acceptance conversions with new algorithms that convert (when possible) all common classes of non deterministic '"`UNIQ--math-00000007-QINU`"'-automata to deterministic co-Büchi. Boker and Kupferman solved this conversion whith asymptotically tight constructions. We implement their methods with some optimizations and adjustments: we made it work with Streett-like acceptance, any acceptance in disjunctive normal form (including Rabin-like) and also transition-based acceptance. Using these conversions gives a new way to check whether an LTL formula is a persistence formula. 10h30 Two-automaton emptiness check in Spot – Clément Gillard

Spot is library that handles '"`UNIQ--math-00000009-QINU`"'-automata whose acceptance conditions are expressed with at most 32 acceptance sets. Since the acceptance condition of the product of two automata has to use the sum of their setswe cannot produce a product whose operands use more than 32 sets in total. A typical operation on automata is to compute '"`UNIQ--math-0000000A-QINU`"' to know if '"`UNIQ--math-0000000B-QINU`"' intersects '"`UNIQ--math-0000000C-QINU`"'. When it is implemented as '"`UNIQ--math-0000000D-QINU`"', the computation of the product throttles the amout of acceptance sets A and B can use. We propose a new function '"`UNIQ--math-0000000E-QINU`"' which does the emptiness check of '"`UNIQ--math-0000000F-QINU`"' without actually building an automaton and hence without any limit on the acceptance conditions. The ltlcross tool can now compare automata using a total of more than 32 acceptance sets. 11h00 Improvements of Simulation-based Reduction – Laurent Xu

In model checking using '"`UNIQ--math-0000003B-QINU`"'-automata, the construction of smaller automata reduces a lot the runtime and the memory consumption of costly operations such as the synchronized product. As the minimization of deterministic Büchi automata is an NP-complete problem, we focus our work on reduction operations. Spot already implements a method of reduction by simulation working with all existential automata with any type of acceptance. This method uses a one-step simulation based on the signatures of the states. L. Clemente and R. Mayr propose a reduction by '"`UNIQ--math-0000003C-QINU`"'-step simulation only working with Büchi automata and show that increasing this number of steps may improve the reduction. We try to generalize the existing reduction operation in Spot to make it work with signature-based '"`UNIQ--math-0000003D-QINU`"'-step simulations. We also present how we can extend the existing reduction to make it work with alternating automata. 11h30 Partial order reduction in SPOT – Vincent Tourneur

Nowadays, model-checking tools suffer from a scalling problem, due to their memory consuption. Partial order reduction is one way allowing to notably reduce it, by computing only needed data on-the-fly. There are many state-of-the-art algorithms, and this method is used in many softwares (such as SPIN or LTSmin). We are going to talk about the implementation of it in the Spot libraryand then the optimisation. The results show a great decrease of the memory consuption, which implies some gain in all subsequent steps. 13h30 Integration of TChecker in Spot – Arthur Remaud

A timed automaton is an '"`UNIQ--math-00000003-QINU`"'-automaton which describe a model containing continue time conditions. Without treatments, those automata can have an infinite states space. However, we can translate them in finite automatacalled zone graph, to analyze their properties. In this report, we show how the timed automata have been integrated at Spot. We use TChecker, a program created at the LaBRI. We explain then how we integrate the representation of those TChecker's zone graph in Spot. Then we show how Spot's algorithms can read this translation to work on timed automata and zone graphes. We then explain how inconvenients of TChecker have been adapted to make simpler its utilisation by Spot. 14h00 LTL Synthesis with Spot – Thibaud Michaud

We present a new tool for circuit synthesis from LTL specifications. It reduces the synthesis problem to a parity game using Spot's efficient algorithms on '"`UNIQ--math-00000003-QINU`"'-automata. Two methods have been implemented for the resolution of the game: a recent algorithm by Calude et al. which has the best known theoretical complexity for the problem, and Zielonka's recursive algorithm known for its good practical performances. Finally, the winning strategy is translated to an And-Inverter Graph that models the original LTL formula.

Olena

14h45 Binary Partition Tree for Image Processing – Fabien Houang

Binary Partition Tree is an efficient structure to store region information for image processing, segmentation and information retrieval. It is a hierarchical structure to simplify operations and recognition on an image. It can use different region models and distance function calculation to create itself. Usually, we construct this tree on a segmented image for efficiency and time saving. All this parameters can variate and change the BPT representation of your image. The resistance of our tree to noise can also be studied, to find out what level of the tree is influenced by the noise. 15h15 Morse-Smale Complex computation with Watershed Cut – Victor Collette

The Morse-Smale complex is a useful tool to analyse the topology of an image. However, its computation is quite expensive, and several algorithms exist having some differences in the definition of the complex. On the other hand, the Watershed Cut is a morphological algorithm, which segments grayscale images. It considers that an image is an edge-weighted graph, where the weights are given by the image gradient. Lidija Comic was the first to coin a possible equivalence between the algorithms to compute the Morse-Smale complex and the Watershed Cut with specific markers on the minima and maxima of the image. In this work, we discuss about this possibility, and we propose an implementation of a modified Watershed Cut algorithm working on vertex-weighted graphs as a way to compute the Morse-Smale complex. 15h45 Evaluation method of text detection algorithm rating – Aliona Dangla

Several methods to evaluate text detection algorithms exist. However, they give different results, so it is difficult to estimate their relevance. In order to evaluate these methods, the proposed solution is to compare the automatic evaluations with the human evaluation by considering the latter as a reference. In order to obtain this reference, a website has been created so that a large number of users can easily classify the results of a large number of text detection algorithms on large image bases. The user interface has been developed to minimize the number of comparisons that the user must make in order to obtain a consistent ranking. The website will be tested with the results of the 2013 ICDAR competition, which is composed of height methods on a data set of 233 images.