- Annonce

Spot 2.11.1 released
by Alexandre Duret-Lutz 10 Oct '22

10 Oct '22

We are happy to announce the release of Spot 2.11.1 Spot is a C++17 library for handling of linear-time temporal logic formulas and omega automata. It comes with a set of command-line utilities (to automate various tasks) and Python binding for easy prototyping. Some applications are model-checking and reactive synthesis. Spot 2.11 is a major release containing new features and improvements implemented over the last 11 months by Florian Rankin, Philipp Schlehuber-Caissier, Antoine Martin, and myself. A detailled list of changes is appended to this email. Spot 2.11.1 fixes a couple of build issues discovered before I had time to announce 2.11... You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) had been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). The removal of "development", is nothing to worry about: we are still continuing to develop Spot as part of our research. However a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.1 (2022-10-10) Bugs fixed: - Fix a build issue preventing the update of website (issue #516). - Fix a compilation error with clang-14 on FreeBSD (issue #515). New in spot 2.11 (2022-10-08) Build: - configure will now diagnose situations where Python bindings will be installed in a directory that is not part of Python's search path. A new configure option --with-pythondir can be used to modify this installation path. (Issue #512) - A new configure option --enable-pthread enables the compilation of Spot with -pthread, and render available the parallel version of some algorithms. If Spot is compiled with -pthread enabled, any user linking with Spot should also link with the pthread library. In order to not break existing build setups using Spot, this option is currently disabled by default in this release. We plan to turn it on by default in some future release. Third-party project using Spot may want to start linking with -pthread in prevision for this change. Command-line tools: - autfilt has a new options --aliases=drop|keep to specify if the HOA printer should attempt to preserve aliases present in the HOA input. This defaults to "keep". - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html - ltlfilt has a new --sonf option to produce a formula's Suffix Operator Normal Form, described in [cimatti.06.fmcad]. The associated option --sonf-aps allows listing the newly introduced atomic propositions. - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). - ltlsynt has a new option --tlsf that takes the filename of a TLSF specification and calls syfco (which must be installed) to convert it into an LTL formula. - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. - ltlsynt has a new option --hide-status to hide the REALIZABLE or UNREALIZABLE output expected by SYNTCOMP. (This line is superfluous, because the exit status of ltlsynt already indicate whether the formula is realizable or not.) - ltlsynt has a new option --dot to request GraphViz output instead of most output. This works for displaying Mealy machines, games, or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for examples. - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba options. Those are used to generate pairs of automata that should include each other, and are used to show a regression (in speed) present in Spot 2.10.x and fixed in 2.11. - genltl learned --eil-gsi to generate a familly a function whose translation and simplification used to be very slow. In particular genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba was reported as taking 9 days. This is now instantaneous. Library: - The new function suffix_operator_normal_form() implements transformation of formulas to Suffix Operator Normal Form, described in [cimatti.06.fmcad]. - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected to recognize the same language. The "original-states" should be prefered property when that integer correspond to some actual state. - tgba_determinize() learned to fill the "original-classes" property. States of the determinized automaton that correspond to the same subset of states of the original automaton belong to the same class. Filling this property is only done on demand as it inccurs a small overhead. - sbacc() learned to take the "original-classes" property into account and to preserve it. - The HOA parser and printer learned to map the synthesis-outputs property of Spot to the controllable-AP header for the Extended HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 - The automaton parser learned to parse games in the PGSolver format. See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for an example. - "aliases" is a new named property that is filled by the HOA parser using the list of aliases declared in the HOA file, and then used by the HOA printer on a best-effort basis. Aliases can be used to make HOA files more compact or more readable. But another possible application is to use aliases to name letters of a 2^AP alphabet, in applications where using atomic propositions is inconvenient. - print_dot() learned option "@" to display aliases, as discussed above. - to_finite() is a new function that help interpreting automata build from LTLf formula using the from_ltlf() function. It replace the previously suggested method of removing and atomic proposition and simpifying automata, that failed to deal with states without successors. See updated https://spot.lrde.epita.fr/tut12.html - the HOA parser learned to not ignore self-loops labeled with [f] and to turn any state that have colors but no outgoing transitions into a state with a [f] self-loop. This helps dealing with automata containing states without successors, as in the output of to_finite(). - purge_dead_states() will now also remove edges labeled by false (except self-loops). - When parsing formulas with a huge number of operands for an n-ary operator (for instance 'p1 | p2 | ... | p1000') the LTL parser would construct that formula two operand at a time, and the formula constructor for that operator would be responsible for inlining, sorting, deduplicating, ... all operands at each step. This resulted in a worst-than-quadratic slowdown. This is now averted in the parser by delaying the construction of such n-ary nodes until all children are known. - complement() used to always turn tautological acceptance conditions into Büchi. It now only does that if the automaton is modified. - The zielonka_tree construction was optimized using the same memoization trick that is used in ACD. Additionally it can now be run with additional options to abort when the tree as an unwanted shape, or to turn the tree into a DAG. - contains() can now take a twa as a second argument, not just a twa_graph. This allows for instance to do contains(ltl, kripke) to obtain a simple model checker (that returns true or false, without counterexample). - degeneralize() and degeneralize_tba() learned to work on generalized-co-Büchi as well. - product() learned that the product of two co-Büchi automata is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. - spot::postprocessor has a new extra option "merge-states-min" that indicates above how many states twa_graph::merge_states() (which perform a very cheap pass to fuse states with identicall succesors) should be called before running simulation-based reductions. - A new function delay_branching_here(aut) can be used to simplify some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂) and (q₁,ℓ,M,q₃) differ only by their destination state, and are the only incoming transitions of their destination states, then q₂ and q₃ can be merged (taking the union of their outgoing transitions). This is cheap function is automatically called by spot::translate() after translation of a formula to GBA, before further simplification. This was introduced to help with automata produced from formulas output by "genltl --eil-gsi" (see above). - spot::postprocessor has new configuration variable branch-post that can be used to control the use of branching-postponement (disabled by default) or delayed-branching (see above, enabled by default). See the spot-x(7) man page for details. - spot::postprocessor is now using acd_transform() by default when building parity automata. Setting option "acd=0" will revert to using "to_parity()" instead. - to_parity() has been almost entirely rewritten and is a bit faster. - When asked to build parity automata, spot::translator is now more aggressively using LTL decomposition, as done in the Generic acceptance case before paritizing the result. This results in much smaller automata in many cases. - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only twa_graph::merge_states() supports it. Python bindings: - The to_str() method of automata can now export a parity game into the PG-Solver format by passing option 'pg'. See https://spot.lrde.epita.fr/ipynb/games.html for an example. Deprectation notice: - spot::pg_print() has been deprecated in favor of spot::print_pg() for consistency with the rest of the API. Bugs fixed: - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could produce unexpected result if begin and end where already pointing into the universal edge vector, since the later can be reallocated during that process. - Printing an alternating automaton with print_dot() using 'u' to hide true state could produce some incorrect GraphViz output if the automaton as a true state as part of a universal group. - Due to an optimization introduces in 2.10 to parse HOA label more efficiently, the automaton parser could crash when parsing random input (not HOA) containing '[' (issue #509).

1 0

Soutenance de thèse de Florian Renkin
by Florian Renkin 06 Sep '22

06 Sep '22

Bonjour, J'ai le plaisir de vous inviter à la soutenance (en français) de ma thèse intitulée : "Transformations d'ω-automates pour la synthèse de contrôleurs réactifs". Vous êtes également cordialement invité au pot qui suivra. Version web : https://www.lrde.epita.fr/~frenkin/thesis.php Date Vendredi 7 octobre, 9h30 Lieu Amphi 401, 14-16 rue Voltaire, Le Kremlin-Bicêtre 94270 Jury _Rapporteurs_ * Olivier Carton, Université Paris Cité * Nicolas Markey, Université de Rennes _Examinateurs_ * Hanna Klaudel, Université d'Évry * Laure Petrucci, Université Sorbonne Paris Nord * Nathalie Sznajder : Sorbonne Université _Encadrants_ * Alexandre Duret-Lutz, EPITA * Adrien Pommellet, EPITA Résumé Le travail de cette thèse s'inscrit dans le cadre de la création de manière automatique de systèmes corrects à partir de spécifications, ce que l'on appelle "synthèse". Ce besoin de création automatique vient d'une part de la complexité de plus en plus importante des systèmes que l'on crée mais aussi de la difficulté de vérifier si un système est correct. Pour que la synthèse soit utilisable en pratique, y compris dans l'industrie, il faut être capable de produire des solutions pour des problèmes plus ou moins complexes en un temps raisonnable. De plus, on peut chercher à optimiser les systèmes produits afin qu'ils soient les plus simples possibles. Pour décrire les contraintes que le système doit respecter, nous utiliserons des formules de logique linéaire temporelle (LTL) qui ajoutent aux opérateurs Booléens traditionnels une notion de temps discret afin d'exprimer des contraintes telles que "il existera un instant où la variable sera vraie". Dans notre cas, il s'agira de produire un contrôleur réactif, c'est-à-dire associant à une suite d'assignations de variables Booléennes d'entrées une suite d'assignations de variables Booléennes de sorties. L'approche de la synthèse LTL que nous allons décrire consiste à : (1) Traduire la spécification LTL en un jeu de parité où un joueur contrôle l'environnement alors que le second représente les actions que peut faire le contrôleur. (2) Rechercher dans ce jeu s'il existe une stratégie gagnante pour le second joueur. (3) Cette stratégie indique les actions que doit faire le contrôleur pour respecter les spécifications et il reste alors à l'encoder sous la forme voulue (circuit, programme, …). Une partie de la première étape est une procédure dite de paritisation consistant à obtenir à partir d'un automate quelconque un automate de parité. Une contribution majeure de cette thèse consiste en l'amélioration de cette procédure. Dans cette optique, nous proposons et comparons divers algorithmes de paritisation. La première méthode est une combinaison d'algorithmes existants auxquels ont été associées des heuristiques mais aussi de nouveaux algorithmes. La seconde est l'adaptation d'une méthode introduite en 2021 par Casares _et al._ assurant une forme d'optimalité sur la taille de l'automate de parité obtenu. Dans les deux cas, ces algorithmes ont à la fois pour objectif de réduire le temps nécessaire pour une telle transformation mais aussi de limiter la taille de l'automate créé. Une autre contribution consiste à proposer des techniques de simplification du contrôleur. En particulier, nous tirerons parti des libertés offertes par la spécification. Par exemple, si l'on souhaite un système allumant une ampoule lorsqu'une présence est détectée, alors ce qu'il faut faire lorsque personne n'est détecté n'a pas d'importance. Pour obtenir un système simple, on peut décider de toujours allumer l'ampoule et le système n'a alors plus besoin d'un capteur. Deux types de simplifications seront décrites. La première est inspirée d'un outil existant (MeMin) et utilise un SAT-solver pour obtenir une solution minimale. La complexité de la recherche d'optimalité (NP-complet) nous incite également à nous tourner vers une seconde méthode basée sur les BDD visant à fournir un système réduit plus rapidement mais sans garantie d'optimalité. Ces deux contributions majeures ont été intégrées à l'outil ltlsynt distribué avec la bibliothèque Spot et ont été accompagnées de plusieurs améliorations que nous évaluons : une décomposition du problème permettant de créer des contrôleurs pour des sous-parties de la spécification mais aussi une méthode permettant de s'affranchir de la construction d'un jeu pour une certaine classe de formules. Ces travaux ont fait l'objet de publications dans les conférences ATVA'19 (première méthode de paritisation), TACAS'22 (seconde méthode de paritisation), FORTE'22 (simplification de contrôleur), CAV'22 (présentation des évolutions de Spot) ainsi que d'une présentation de ltlsynt lors de la conférence SYNT'21. L'outil ltlsynt a par ailleurs participé aux éditions 2020, 2021 et 2022 de la Syntcomp. A bientôt, Florian Renkin

1 0

[CfP] ICCQ 2023 - 3rd International Conference on Code Quality
by Didier Verna 06 Sep '22

06 Sep '22

ICCQ 2023 https://www.iccq.ru/2023.html Sat 22 Apr 2023, St. Petersburg, Russia Due to the pandemic situation, the conference will be held in online mode: all speakers will present their work remotely over Zoom. The Third International Conference on Code Quality (ICCQ) is a one-day computer science event focused on static and dynamic analysis, program verification, programming languages design, software bug detection, and software maintenance. ICCQ is organized in cooperation with IEEE Computer Society. Program Committee ================= Andrey Terekhov (Chair), SPbU Alexandre Bergel, University of Chile Laura M. Castro, Universidade da Coruña Stephen Chang, UMass Boston Daniele Cono D’Elia, Sapienza University of Rome Pierre Donat-Bouillud, Czech Technical University Bernhard Egger, Seoul National University Sebastian Erdweg, Johannes Gutenberg University Mainz Samir Genaim, Universidad Complutense de Madrid Shachar Itzhaky, Technion Yusuke Izawa, Tokyo Institute of Technology Ranjit Jhala, University of California, San Diego Tetsuo Kamina, Oita University Christoph Kirsch, University of Salzburg Yu David Liu, Binghamton University Wolfgang de Meuter, Vrije Universiteit Brussel Antoine Miné, Sorbonne Université Guillermo Polito, CRIStAL Xuehai Qian, University of Southern California Junqiao Qiu, Michigan Technological University Yann Régis-Gianas, Nomadic Labs Yudai Tanabe, Tokyo Institute of Technology Tachio Terauchi, Waseda University Didier Verna, EPITA David West, New Mexico Highlands University Guannan Wei, Purdue University Vadim Zaytsev, University of Twente Important Dates =============== Paper/abstract submission: 18 Dec 2022 (anywhere on Earth) Author notification: 1 Mar 2023 Camera-ready submissions: 25 Mar 2023 Conference: 22 Apr 2023 Call for Papers =============== Papers will be published in the Proceedings of ICCQ and submitted for inclusion into IEEE Xplore subject to meeting their scope and quality requirements; to be indexed by Web of Science, Scopus, Google Scholar, DBLP, and others. We consider the following criteria when evaluating papers: Novelty: The paper presents new ideas and results and places them appropriately within the context established by previous research. Importance: The paper contributes to the advancement of knowledge in the field. We also welcome papers that diverge from the dominant trajectory of the field. Evidence: The paper presents sufficient evidence supporting its claims, such as proofs, implemented systems, experimental results, statistical analyses, case studies, and anecdotes. Clarity: The paper presents its contributions, methodology and results clearly. Papers will be reviewed by at least three PC members using a double-blind review process. Instructions for Authors ======================== Submissions must be in PDF, printable in black and white on US Letter sized paper. All submissions must adhere to the acmart sigplan template (two columns, 11pt font size). Compile it with this header: \documentclass[sigplan,11pt,nonacm=true]{acmart} \settopmatter{printfolios=false,printccs=false,printacmref=false} Submitted papers must be at least 4 and at most 16 pages long, including bibliographical references and appendices. Submissions that do not meet the above requirements will be rejected without review. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Paper accepted at CONCUR'22
by Uli Fahrenberg 06 Sep '22

06 Sep '22

The following paper has been accepted at the 33rd International Conference on Concurrency Theory (CONCUR 2022), to be held in Warsaw next week: A Kleene Theorem for Higher-Dimensional Automata Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański (LR(D)E, NTNU Gjøvik, U of Sheffield, Warsaw U) We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

1 0

article accepted: The 34th Symposium on Implementation and Application of Functional Languages
by Jim Newton (lrde) 16 Aug '22

16 Aug '22

Hi, I’m pleased to announce I’ve had a paper accepted for presentation at The 34th Symposium on Implementation and Application of Functional Languages (https://ifl22.github.io <https://ifl22.github.io/>). The paper is entitled: How to fold and color a map: Comparing Use-Cases of Tree-Fold vs Fold-Left. You may view the article here https://drive.google.com/file/d/1-65beERt9UylSmxgsWe-gcl3Hz8JvjzC/view?usp=… as it is not yet available on /lrde/doc, pending an IT issue. ABSTRACT In this article we examine some consequences of computation order of two different conceptual implementations of the fold function. We explore a set of performance- and accuracy-based experiments on two implementations of this function. In particular, we contrast the traditional fold-left implementation with another approach we refer to as tree-fold. It is often implicitly supposed that the binary operation in question has constant complexity. We explore several application areas which diverge from that assumption: rational arithmetic, floating-point arithmetic, and Binary Decisions Diagram construction. These are binary operations which degrade in performance as the fold iteration progresses. We show that these types of binary operations are good candidates for tree-fold. Kind regards Jim

1 0

Quickref 4.0b1 is out
by Didier Verna 10 Jun '22

10 Jun '22

Dear all, following the recent release of Declt 4.0, I'm happy to announce that Quickref 4.0 is on its way too, resulting in an update of the official website (https://quickref.common-lisp.net/) which now contains automatically generated documentation for 2110 Common Lisp libraries. The Docker images are up to date too. More details here: https://www.didierverna.net/blog/index.php?post/2022/05/26/Quickref-4.0-bet… -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Declt 4.0 beta 1 is released
by Didier Verna 10 Jun '22

10 Jun '22

Dear all, I'm happy to announce the release of Declt 4.0 beta 1. Although tagged as a beta version, this release is stable and constitutes the first of three steps in a major infrastructure overhaul. Declt is the rendering engine behind Quickref, a website providing automatic documentation for more than two thousand Common Lisp libraries. The long list of fixes, improvements, and new features in this release is proved here: https://www.didierverna.net/blog/index.php?post/2022/05/10/Declt-4.0-beta-1… For more information on Declt / Quickref: https://www.lrde.epita.fr/~didier/software/lisp/typesetting.php The Quickref website: https://quickref.common-lisp.net/ -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

sortie de mon essai "Données, Transparence et Démocratie"
by Olivier Ricou 07 Jun '22

07 Jun '22

Bonjour, Je suis heureux de vous annoncer la sortie de mon essai Données, Transparence et Démocratie http://opendata.ricou.eu.org/ Je pars du fait que notre système politique va mal et que la confiance en nos institutions est faible. Un remède me semble être de donner à chacun les outils pour vérifier les actions de l'État et pour participer. Cela passe par la transparence, dans notre cas l'ouverture des données publiques, et par la prise en compte des retours des citoyens. L'ouverture des données publiques est inscrite dans la loi depuis 2016 mais elle a du mal à se mettre en place, pour des raisons techniques et politiques. Elle peut aussi être ralentie par le sentiment d'inutilité lorsque des données publiées ne trouvent pas leur public. Aussi le but de mon essai est de souligner l'importance de cette ouverture et de pousser chacun d'entre nous à exploiter ces données dans un but personnel ou pour le bien public. Cette ouverture offre aussi de nombreuses opportunités économiques et sociales que je présente dans ce livre. N'hésitez pas à me faire part de vos impressions ou remarques, par mail ou sur mon fil Twitter @egeopol https://twitter.com/egeopol Olivier Ricou.

1 0

New publication: "From Spot 2.0 to Spot 2.10: What's New?" (CAV'22)
by Alexandre Duret-Lutz 06 Jun '22

06 Jun '22

We are happy to announce that the following article has been accepted to the 34th International Conference on Computer Aided Verification (CAV'22) to be held in Haifa, Israel, in August 7-10, 2022. ====================================================================== From Spot 2.0 to Spot 2.10: What's New? Alexandre Duret-Lutz¹ Étienne Renault¹ Maximilien Colange² Florian Renkin¹ Alexandre Gbaguidi Aisse² Philipp Schlehuber-Caissier¹ Thomas Medioni² Antoine Martin¹ Jérôme Dubois¹ Clément Gillard² Henrich Lauko² ¹LRDE, EPITA, France ²previously at LRDE Spot is a C++17 library for LTL and ω-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support ω-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata. https://www.lrde.epita.fr/wiki/Publications/duret.22.cav ======================================================================

1 0

Conférence GETCO
by Uli Fahrenberg 26 May '22

26 May '22

Bonjour, École polytechnique, LRDE and EPITA are organizing a scientific conference next week, "GETCO: Geometric and Topological Methods in Computer Science". See https://www.lix.polytechnique.fr/~smimram/getco22/ for program etc. Most talks will take place in Amphi 0, except for some parallel sessions in the afternoons which will be in KB404. Even if you are not registered, you're welcome to come and join us for some of the talks. Bien cordialement, for the organisers, Uli Fahrenberg, LRDE

1 0