Annonce

annonce@lrde.epita.fr

566 discussions

Paper accepted at FORTE'22: LTL under reductions with weaker conditions than stutter invariance

by Renault Etienne

We are happy to announce that the following article has been accepted to the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22), one of the three conference of the 17th International Federated Conference on Distributed Computing Techniques (DisCoTec'22) to be held on June 13-17 in Lucca, Italy. (Philipp will go there to present the paper.) ====================================================================== LTL under reductions with weaker conditions than stutter invariance Emmanuel Paviot-Adet (1)(2), Denis Poitrenaud (1)(2), Etienne Renault (3), Yann Thierry-Mieg (1) (1) SorbonneUniversité,CNRS,LIP6,F-75005Paris,France (2) Université de Paris,F-75006Paris,France (3) LRDE, EPITA, France Verification of properties expressed as 𝜔-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. https://www.lrde.epita.fr/wiki/Publications/paviot.22.forte <https://www.lrde.epita.fr/wiki/Publications/paviot.22.forte>

3 years, 1 month

Paper accepted at FORTE'22: Effective Reductions of Mealy Machines

by Alexandre Duret-Lutz

3 years, 2 months

Paper accepted at TACAS'22: Practical Applications of the ACD

by Alexandre Duret-Lutz

We are happy to announce that the following article has been accepted to the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22) to be held in Munich in April 2022. ====================================================================== Practical Applications of the Alternating Cycle Decomposition Antonio Casares¹, Alexandre Duret-Lutz², Klara J. Meyer³, Florian Renkin², and Salomon Sickert⁴ ¹LaBRI, Universitée de Bordeaux, France ²LRDE, EPITA, France ³Independent Researcher ⁴School of Computer Science and Engineering, The Hebrew Univ., Israel In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot, and adapt it to the framework of Emerson-Lei automata, i.e., ω-automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of Emerson-Lei automata into parity automata with strong optimality guarantees: the resulting parity automaton is minimal among those automata that can be obtained by duplication of states. Our empirical results show that this transformation is usable in practice. Further, we show how the ACD can generalize many other specialized constructions such as deciding typeness of automata and degeneralization of generalized Büchi automata, providing a framework of practical algorithms for ω-automata. https://www.lrde.epita.fr/wiki/Publications/casares.22.tacas ======================================================================

3 years, 5 months

Spot 2.10 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.10 Spot is a C++17 for LTL and ω-automata manipulation, with applications to model checking and reactive synthesis. This is a major release that has been under development for 19 months. It contains new features contributed by Jérôme Dubois, Antoine Martin, Étienne Renault, Florian Renkin, Philipp Schlehuber, and myself. A summary of those changes is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10 (2021-11-13) Build: - Spot is now built in C++17 mode, so you need at least GCC 7 or clang 5 to compile it. The current versions of all major linux distributions ship with at least GCC 7.4, so this should not be a problem. There is also an --enable-c++20 option to configure in case you want to force a build of Spot in C++20 mode. Command-line tools: - ltlsynt has been seriously overhauled, while trying to preserve backward compatibility. Below is just a summary of the main user-visible changes. Most of the new options are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html + ltlsynt now accepts only one of the --ins or --outs options to be given and will deduce the value of the other one. + ltlsynt learned --print-game-hoa to output its internal parity game in the HOA format (with an extension described below). + ltlsynt --aiger option now takes an optional argument indicating how the bdd and states are to be encoded in the aiger output. The option has to be given in the form ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only obligatory argument decides whether "if-then-else" ("ite") or irreducible-sum-of-products ("isop") is to be used. "both" executes both strategies and retains the smaller circuits. The additional options are for fine-tuning. "ud" also encodes the dual of the conditions and retains the smaller circuits. "dc" computes if for some inputs we do not care whether the output is high or low and try to use this information to compute a smaller circuit. "subX" indicates different strategies to find common subexpressions, with "sub0" indicating no extra computations. + ltlsynt learned --verify to check the computed strategy or aiger circuit against the specification. + ltlsynt now has a --decompose=yes|no option to specify if the specification should be decomposed into independent sub-specifications, the controllers of which can then be glued together to satisfy the input specification. (cf. [finkbeiner.21.nfm] in doc/spot.bib) + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat to specifies how to simplify the synthesized controler. - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi option, or -b for short. This outputs Büchi automata without forcing state-based acceptance. The following aliases have also been added for consistency: --gba is an alias for --tgba, because the "t" of --tgba is never forced. --sba is an alias for -B/--ba, because -B really implies -S and that is not clear from --ba. As a consequence of the introduction of --sba, the option --sbacc (an alias for --state-based-acceptance) cannot be abbreviated as --sba anymore. - autfilt learned a --kill-states=NUM[,NUM...] option. - ltlcross, autcross, ltldo have learned shorthands for the commands of Owl 21.0. For instance running ltlcross 'owl-21 ltl2nba' ... is equivalent to running ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ... Library: - Spot now provides convenient functions to create and solve games. (twaalgos/game.hh) and some additional functions for reactive synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh). - A new class called aig represent an and-inverter-graphs, and is currently used during synthesis. (twaalgos/aiger.hh) - Some new *experimental* classes, called "twacube" and "kripkecube" implement a way to store automata or Kripke structures without using BDDs as labels. Instead they use a structure called cube, that can only encode a conjunction of litterals. Avoiding BDDs (or rather, avoiding the BuDDy library) in the API for automata makes it possible to build multithreaded algorithms. /!\ Currently these classes should be considered as experimental, and their API is very likely to change in a future version. Functions like twacube_to_twa(), twa_to_twacube(), can be used to bridge between automata with BDD labels, and automata with cube labels. In addition to the previous conversion, we implemented various state-of-the-art multi-threaded emptiness-check algorithms: [bloemen.16.ppopp], [bloemen.16.hvc], [evangeslita.12.atva], [renault.13.lpar], [holzmann.11.ieee] (see doc/spot.bib). The mc_instanciator class provides an abstraction for launching, pinning, and stopping threads inside of parallel model-checking algorithms. The class ltsmin_model class, providing support for loading various models that follow ltsmin's PINS interinterface, has been adjusted and can now produce either a kripke instance, or a kripkecube instance. - The postprocessor::set_type() method can now accept options postprocessor::Buchi and postprocessor::GeneralizedBuchi. These syntaxes is more homogeneous with the rest of the supported types. Note that postprocessor::BA and postprocessor::TGBA, while still supported and not yet marked as deprecated, are best avoided in new code. postprocessor::set_type(postprocessor::TGBA) can be replaced by postprocessor::set_type(postprocessor::GeneralizedBuchi) and postprocessor::set_type(postprocessor::BA) by postprocessor::set_type(postprocessor::Buchi) postprocessor::set_pref(postprocessor::Small | postprocessor::SBAcc) Note that the old postprocessor::BA option implied state-based acceptance (and was unique in that way), but the new postprocessor::Buchi specifies Büchi acceptance without requiring state-based acceptance (something that postprocessor did not permit before). - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which used to take ages are now instantaneous. (Issue #412.) - remove_fin() learned to remove more unnecessary edges by using propagate_marks_vector(), both in the general case and in the Rabin-like case. - simplify_acceptance() learned to simplify acceptence formulas of the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x always implies that of y. (Issue #406.) - simplifiy_acceptance_here() and propagate_marks_here() learned to use some patterns of the acceptance condition to remove or add (depending on the function) colors on edges. As an example, with a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can be simplied to {0}, but the oppose rewriting can be useful as well. (Issue #418.) - The parity_game class has been removed, now any twa_graph_ptr that has a "state-player" property is considered to be a game. - the "state-player" property is output by the HOA printer, and read back by the automaton parser, which means that games can be saved and loaded. - print_dot() will display states from player 1 using a diamond shape. - print_dot() learned to display automata that correspond to Mealy machines specifically. - print_dot() has a new option "i" to define id=... attributes for states (S followed by the state number), edges (E followed by the edge number), and SCCs (SCC followed by SCC number). The option "i(graphid)" will also set the id of the graph. These id attributes are useful if an automaton is converted into SVG and one needs to refer to some particular state/edge/SCC with CSS or javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS - spot::postproc has new configuration variables that define thresholds to disable some costly operation in order to speedup the processing of large automata. (Those variables are typically modified using the -x option of command-line tools, and are all documented in the spot-x(7) man page.) wdba-det-max Maximum number of additional states allowed in intermediate steps of WDBA-minimization. If the number of additional states reached in the powerset construction or in the followup products exceeds this value, WDBA-minimization is aborted. Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used or when det-max-states is set. simul-max Number of states above which simulation-based reductions are skipped. Defaults to 4096. Set to 0 to disable. This also applies to the simulation-based optimization of the determinization algorithm. simul-trans-pruning For simulation-based reduction, this is the number of equivalence classes above which transition-pruning for non-deterministic automata is disabled. Defaults to 512. Set to 0 to disable. This applies to all simulation-based reduction, as well as to the simulation-based optimization of the determinization algorithm. Simulation-based reduction perform a number of BDD implication checks that is quadratic in the number of classes to implement transition pruning. dpa-simul Set to 0/1 to disable/enable simulation-based reduction performed after running a Safra-like determinization to optain a DPA. By default, it is only disabled with --low or if simul=0. dba-simul Set to 0/1 to disable/enable simulation-based reduction performed after running the powerset-like construction (enabled by option tba-det) to obtain a DBA. By default, it is only disabled with --low or if simul=0. spot::translator additionally honor the following new variables: tls-max-states Maximum number of states of automata involved in automata-based implication checks for formula simplifications. Defaults to 64. exprop When set, this causes the core LTL translation to explicitly iterate over all possible valuations of atomic propositions when considering the successors of a BDD-encoded state, instead of discovering possible successors by rewriting the BDD as a sum of product. This is enabled by default for --high, and disabled by default otherwise. When unambiguous automata are required, this option forced and cannot be disabled. (This feature is not new, but was not tunable before.) - In addition the to above new variables, the default value for ba-simul (controling how degeneralized automata are reduced) and for det-simul (simulation-based optimization of the determinization) is now equal to the default value of simul. This changes allows "-x simul=0" to disable all of "ba-simul", "dba-simul", "dpa-simul", and "det-simul" at once. - tgba_powerset() now takes an extra optional argument to specify a list of accepting sinks states if some are known. Doing so can cut the size of the powerset automaton by 2^|sinks| in favorable cases. - twa_graph::merge_edges() had its two passes swapped. Doing so improves the determinism of some automata. - twa_graph::kill_state(num) is a new method that removes the outgoing edge of some state. It can be used together with purge_dead_states() to remove selected states. - The new functions reduce_direct_sim(), reduce_direct_cosim() and reduce_iterated() (and their state based acceptance version, reduce_direct_sim_sba(), reduce_direct_cosim_sba() and reduce_iterated_sba()), are matrix-based implementation of simulation-based reductions. This new version is faster than the signature-based BDD implementation in most cases, however there are some cases it does not capture yet.. By default, the old one is used. This behavior can be changed by setting SPOT_SIMULATION_REDUCTION environment variable or using the "-x simul-method=..." option (see spot-x(7)). - The automaton parser will now recognize lines of the form #line 10 "filename" that may occur *between* the automata of an input stream to specify that error messages should be emitted as if the next automaton was read from "filename" starting on line 10. (Issue #232) - The automaton parser for HOA is now faster at parsing files where a label is used multiple times (i.e., most automata): it uses a hash table to avoid reconstructing BDDs corresponding to label that have already been parsed. This trick was already used in the never claim parser. - spot::twa_graph::merge_states() will now sort the vector of edges before attempting to detect mergeable states. When merging states with identical outgoing transitions, it will now also consider self-looping transitions has having identical destinations. Additionally, this function now returns the number of states that have been merged (and therefore removed from the automaton). - spot::zielonka_tree and spot::acd are new classes that implement the Zielonka Tree and Alternatic Cycle Decomposition, based on a paper by Casares et al. (ICALP'21). Those structures can be used to paritize any automaton, and more. The graphical rendering of ACD in Jupyter notebooks is Spot's first interactive output. See https://spot.lrde.epita.fr/ipynb/zlktree.html for more. Python: - Bindings for functions related to games. See https://spot.lrde.epita.fr/ipynb/games.html and https://spot.lrde.epita.fr/tut40.html for examples. - Bindings for functions related to synthesis and aig-circuits. See https://spot.lrde.epita.fr/ipynb/synthesis.html - spot::twa::prop_set was previously absent from the Python bindings, making it impossible to call make_twa_graph() for copying a twa. It is now available as spot.twa_prop_set (issue #453). Also for convenience, the twa_graph.__copy__() method, called by copy.copy(), will duplicate a twa_graph (issue #470). Bugs fixed: - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) - There were two corners cases under which sat_minimize() would return the original transition-based automaton when asked to produce state-based output without changing the acceptance condition. Deprecation notices: - twa_graph::defrag_states() and digraph::defrag_states() now take the renaming vector by reference instead of rvalue reference. The old prototype is still supported but will emit a deprecation warning.

3 years, 8 months

[CfP] 15th European Lisp Symposium, March 21-22 2022, Porto, Portugal

by Didier Verna

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 15th European Lisp Symposium Call for Papers March 21-22, 2022 FEUP, Porto, Portugal & Online In co-location with <Programming> http://www.european-lisp-symposium.org/2022 Sponsored by EPITA ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Important Dates ~~~~~~~~~~~~~~~ - Submission deadline: January 23, 2022 - Author notification: February 21, 2022 - Final papers due: March 7, 2022 - Symposium: March 21-22, 2022 Scope ~~~~~ The European Lisp Symposium is a premier forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp dialects, including Common Lisp, Scheme, Emacs Lisp, Clojure, Racket, ACL2, AutoLisp, ISLISP, Dylan, SKILL, Hy, Shen, Carp, Janet, uLisp, Picolisp, Gamelisp, TXR, and so on. We encourage everyone interested in Lisp to participate. The 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 Technical Program ~~~~~~~~~~~~~~~~~ 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 4 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. 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 http://www.easychair.org/conferences/?conf=els2021 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. Programme Chair ~~~~~~~~~~~~~~~ Jim Newton - EPITA Research Lab (LRDE), France Programme Committee ~~~~~~~~~~~~~~~~~~~ tba -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

3 years, 8 months

New publication: CP21

by akheireddine

Greetings, We are pleased to announce that the following paper has been accepted to the 27th International Conference on Principles and Practice of Constraint Programming (CP'21) that will take place online, on the 25-29th of October 2021. Title and corresponding authors: "Towards better Heuristics for Solving Bounded Model Checking Problems" Anissa Kheireddine(1) and Etienne Renault(1) and Souheib Baarir(2) (1) LRDE, EPITA, Le Kremlin-Bicêtre, France (2) LIP6, Sorbonne Université, Paris, France Abstract: This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results. More information at : https://www.lrde.epita.fr/wiki/Publications/kheireddine.21.cp

3 years, 10 months

New publication: SPIN'21

by Renault Etienne

Greetings, We are pleased to announce that the following paper has been accepted to the 27th International SPIN Symposium on Model Checking of Software (SPIN'21) that will take place online, on the 12-13th of July 202. Title and corresponding authors: "Go2Pins: a framework for the LTL verification of Go programs" Alexandre Kirszenberg(1) and Antoine Martin(1) and Hugo Moreau(1) and Etienne Renault(1) (1) LRDE, EPITA, Le Kremlin-Bicêtre, France Abstract: We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. In this paper we demonstrate the usage of Go2Pins over benchmarks inspired by industrial problems and a set of LTL formulae. Even if Go2Pins is still at the early stages of development, our results are promising and show the the benefits of using black-box transitions. More information at : https://www.lrde.epita.fr/wiki/Publications/kirszenberg.21.spin <https://www.lrde.epita.fr/wiki/Publications/kirszenberg.21.spin>

4 years, 1 month

Paper accepted ELS 2021

by Jim Newton

Adrien Pommellet and I are happy to announce that our paper has been accepted for presentation at the 2021 European Lisp Symposium. ABSTRACT: We present a simple type system inspired by that of Common Lisp. The type system is intended to be embedded into a host language and accepts certain fundamental types from that language as axiomatically given. The type calculus provided in the type system is capable of expressing union, intersection, and complement types, as well as membership, subtype, disjoint, and habitation checks. We present a theoretical foundation and two sample implementations, one in Clojure and one in Scala.

4 years, 3 months

Accepted paper at ELS 2021

by Didier Verna

Dear all, Antoine Hacquard and I are pleased to announce that our submission to the 14th European Lisp Symposium has been accepted. The details are given below. ===== A Corpus Processing and Analysis Pipeline for Quickref ===== Antoine Hacquard & Didier Verna Quicklisp is a library manager working with your existing Common Lisp implementation to download and install around 2000 libraries, from a central archive. Quickref, an application itself written in Common Lisp, generates, automatically and by introspection, a technical documentation for every library in Quicklisp, and produces a website for this documentation. In this paper, we present a corpus processing and analysis pipeline for Quickref. This pipeline consists in a set of natural language processing blocks allowing us to analyze Quicklisp libraries, based on natural language contents sources such as README files, docstrings, or symbol names. The ultimate purpose of this pipeline is the generation of a keyword index for Quickref, although other applications such as word clouds or topic analysis are also envisioned. -- ¡En Seguida! -- New album: https://www.didierverna.com/records/en-seguida.php Available on all digital platforms now! Lisp, Jazz, Aïkido: http://www.didierverna.info

4 years, 3 months

Séminaire "morphologie mathématique, IA et astrométrie" (LRDE/IMCCE) le vendredi 5 mars

by Guillaume Tochon

Chers tous, Le vendredi 05 mars se tiendra à l'EPITA un séminaire conjointement organisé par le LRDE et l'IMCCE sur le thème "morphologie mathématique, IA et astrométrie". L'objectif de la journée est de pouvoir échanger autours des thématiques respectives des deux communautés présentes (astronomie et traitement d'images) ainsi que leurs interactions possibles. La journée se tiendra entre 9h30 et 16h30 en amphi IP11 de l'EPITA, et sera retransmise en parallèle sur Zoom (lien à venir) Le programme définitif de la journée est en pièce-jointe. Si vous êtes intéressés, merci de prévenir Élodie (elodie(a)lrde.epita.fr) ou Guillaume (guillaume.tochon(a)lrde.epita.fr) par mail en précisant si vous souhaitez participer en présentiel ou à distance Bien à vous, Élodie et Guillaume pour l'organisation côté LRDE, Valéry Lainey pour l'organisation côté IMCCE -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 24, rue Pasteur 94270 Le Kremlin-Bicêtre +33 1 53 14 59 39

4 years, 4 months

← Newer
1
2
3
4
5
6
7
8
...
57
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce