January 2018 - Annonce

Spot 2.5 released
by Alexandre Duret-Lutz 20 Jan '18

20 Jan '18

We are happy to announce the release of Spot 2.5. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). A detailed list of new features in this new release is given at the end of this email. The main features of this release are algorithms for working with parity acceptance, new functions to convert to co-Büchi when possible, a new tool for LTL synthesis, and some speedup of our determinization algorithm. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. (Note that due to some technical issues on our side, it might be a few days before the packages for Debian *unstable* are updated.) This release contains code contributed by Alexandre Gbaguidi Aïsse, Thibaud Michaud, Laurent Xu, Maximilien Colange, Etienne Renault, and myself. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.5 (2018-01-20) Build: - We no longer distribute the doxygen-generated documentation in the tarball of Spot to save space. This documentation is still available online at https://spot.lrde.epita.fr/doxygen/. If you want to build a local copy you can configure Spot with --enable-doxygen, or simply run "cd doc && make doc". - All the images that illustrate the documentation have been converted to SVG, to save space and improve quality. Tools: - ltlsynt is a new tool for synthesizing a controller from LTL/PSL specifications. - ltlcross learned --reference=COMMANDFMT to specify a translator that should be trusted. Doing so makes it possible to reduce the number of tests to be performed, as all other translators will be compared to the reference's output when available. Multiple reference can be given; in that case other tools are compared against the smallest reference automaton. - autcross, ltlcross, and ltldo learned --fail-on-timeout. - ltl2tgba, autfilt, and dstar2tgba have some new '--parity' and '--colored-parity' options to force parity acceptance on the output. Different styles can be requested using for instance --parity='min odd' or --parity='max even'. - ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option to force co-Büchi acceptance on the output. Beware: if the input language is not co-Büchi realizable the output automaton will recognize a superset of the input. Currently, the output is always state-based. - genltl learned to generate six new families of formulas, taken from the SYNTCOMP competition on reactive synthesis, and from from Müller & Sickert's GandALF'17 paper: --gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz --gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz --ms-example=RANGE GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...))) --ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) - autfilt learned --streett-like to convert automata with DNF acceptance into automata with Streett-like acceptance. - autfilt learned --acceptance-is=ACC to filter automata by acceptance condition. ACC can be the name of some acceptance class (e.g. Büchi, Fin-less, Streett-like) or a precise acceptance formula in the HOA syntax. - ltldo learned to limit the number of automata it outputs using -n. - ltlfilt learned to measure wall-time using --format=%r, and cpu-time with --format=%R. - The --format=%g option of tools that output automata used to print the acceptance condition as a *formula* in the HOA format. This %g may now take optional arguments to print the acceptance *name* in different formats. For instance ... | autfilt -o '%[s]g.hoa' will separate a stream of automata into different files named by their acceptance name (Buchi, co-Buchi, Streett, etc.) or "other" if no name is known for the acceptance condition. - Tools that produce formulas now support --format=%[OP]n to display the nesting depth of operator OP. - The new -x tls-impl=N option allows to fine-tune the implication-based simplification rules of ltl2tgba. See the spot-x(7) man page for details. - All tools learned to check the SPOT_OOM_ABORT environment variable. This is only useful for debuging out-of-memory conditions. See the spot-x(7) man page for details. New functions in the library: - spot::iar() and spot::iar_maybe() use index appearance records (IAR) to translate Rabin-like automata into equivalent parity automaton. This translation preserves determinism and is especially useful when the input automaton is deterministic. - spot::print_aiger() encodes an automaton as an AIGER circuit, as required by the SYNTCOMP competition. It relies on a new named property "synthesis outputs" that describes which atomic propositions are to be encoded as outputs of the circuits. - spot::dnf_to_streett() converts any automaton with a DNF acceptance condition into a Streett-like automaton. - spot::nsa_to_nca(), spot::dfn_to_nca(), spot::dfn_to_dca(), and spot::nsa_to_dca(), convert automata with DNF or Streett-like acceptance into deterministic or non-deterministic co-Büchi automata. spot::to_dca() and spot::to_nca() dispatch between these four functions. The language of produced automaton includes the original language, but may be larger if the original automaton is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 paper. Currently only supports state-based output. - spot::scc_info::states_on_acc_cycle_of() returns all states visited by any accepting cycle of the specified SCC. It only works on automata with Streett-like acceptance. - spot::is_recurrence(), spot::is_persistence(), and spot::is_obligation() test if a formula is a recurrence, persistance or obligation. The SPOT_PR_CHECK and SPOT_O_CHECK environment variables can be used to select between multiple implementations of these functions (see the spot-x(7) man page). - spot::is_colored() checks if an automaton is colored (i.e., every transition belongs to exactly one acceptance set). - spot::change_parity() converts between different parity acceptance conditions. - spot::colorize_parity() transforms an automaton with parity acceptance into a colored automaton (which is often what people working with parity automata expect). - spot::cleanup_parity_acceptance() simplifies a parity acceptance condition. - spot::parity_product() and spot::parity_product_or() are specialized (but expensive) products that preserve parity acceptance. - spot::remove_univ_otf() removes universal transitions on the fly from an alternating Büchi automaton using Miyano and Hayashi's breakpoint algorithm. - spot::stutter_invariant_states(), spot::stutter_invariant_letters(), spot::highlight_stutter_invariant_states(), ... These functions help study a stutter-sensitive automaton and detect the subset of states that are stutter-invariant. See https://spot.lrde.epita.fr/ipynb/stutter-inv.html for examples. - spot::acc_cond::name(fmt) is a new method that names well-known acceptance conditions. The fmt parameter specifies the format to use for that name (e.g. to the style used in HOA, or that used by print_dot()). - spot::formula::is_leaf() method can be used to detect formulas without children (atomic propositions, or constants). - spot::nesting_depth() computes the nesting depth of any LTL operator. - spot::check_determinism() sets both prop_semi_deterministic() and prop_universal() appropriately. Improvements to existing functions in the library: - spot::tgba_determinize() has been heavily rewritten and optimized. The algorithm has (almost) not changed, but it is much faster now. It also features an optimization for stutter-invariant automata that may produce slightly smaller automata. - spot::scc_info now takes an optional argument to disable some features that are expensive and not always necessary. By default scc_info tracks the list of all states that belong to an SCC (you may now ask it not to), tracks the successor SCCs of each SCC (that can but turned off), and explores all SCCs of the automaton (you may request to stop on the first SCC that is found accepting). - In some cases, spot::degeneralize() would output Büchi automata with more SCCs than its input. This was hard to notice, because very often simulation-based simplifications remove those extra SCCs. This situation is now detected by spot::degeneralized() and fixed before returning the automaton. A new optional argument can be passed to disable this behavior (or use -x degen-remscc=0 from the command-line). - The functions for detecting stutter-invariant formulas or automata have been overhauled. Their interface changed slightly. They are now fully documented. - spot::postprocessor::set_type() can now request different forms of parity acceptance as output. However currently the conversions are not very smart: if the input does not already have parity acceptance, it will simply be degeneralized or determinized. - spot::postprocessor::set_type() can now request co-Büchi acceptance as output. This calls the aforementioned to_nca() or to_dca() functions. - spot::remove_fin() will now call simplify_acceptance(), introduced in 2.4, before attempting its different Fin-removal strategies. - spot::simplify_acceptance() was already merging identical acceptance sets, and detecting complementary sets i and j to perform the following simplifications Fin(i) & Inf(j) = Fin(i) Fin(i) | Inf(j) = Inf(i) It now additionally applies the following rules (again assuming i and j are complementary): Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t - spot::formula::map(fun) and spot::formula::traverse(fun) will accept additionnal arguments and pass them to fun(). See https://spot.lrde.epita.fr/tut03.html for some examples. Python-specific changes: - The "product-states" property of automata is now accessible via spot.twa.get_product_states() and spot.twa.set_product_states(). - twa_word instances can be displayed as SVG pictures, with one signal per atomic proposition. For some examples, see the use of the show() method in https://spot.lrde.epita.fr/ipynb/word.html - The test suite is now using v4 of the Jupyter Notebook format. - The function rabin_is_buchi_realizable() as its name suggests checks if a rabin aut. is Büchi realizable. It is heavily based on tra_to_tba() algorithm. Deprecation notices: (These functions still work but compilers emit warnings.) - spot::scc_info::used_acc(), spot::scc_info::used_acc_of() and spot::scc_info::acc() are deprecated. They have been renamed spot::scc_info::marks(), spot::scc_info::marks_of() and spot::scc_info::acc_sets_of() respectively for clarity. Backward incompatible changes: - The spot::closure(), spot::sl2(), spot::is_stutter_invariant() functions no longer take && arguments. The former two have spot::closure_inplace() and spot::sl2_inplace() variants. These functions also do not take a list of atomic propositions as an argument anymore. - The spot::bmrand() and spot::prand() functions have been removed. They were not used at all in Spot, and it is not Spot's objective to provide such random functions. - The spot::bdd_dict::register_all_propositions_of() function has been removed. This low-level function was not used anywhere in Spot anymore, since it's better to use spot::twa::copy_ap_of(). Bugs fixed: - spot::simplify_acceptance() could produce incorrect output if the first edge of the automaton was the only one with no acceptance set. In spot 2.4.x this function was only used by autfilt --simplify-acceptance; in 2.5 it is now used in remove_fin(). - spot::streett_to_generalized_buchi() could generate incorrect automata with empty language if some Fin set did not intersect all accepting SCCs (in other words, the fix from 2.4.1 was incorrect). - ltlcross could crash when calling remove_fin() on an automaton with 32 acceptance sets that would need an additional set. - the down_cast() helper function used in severaly headers of Spot was not in the spot namespace, and caused issues with some configurations of GCC. -- Alexandre Duret-Lutz

1 0

Séminaire des étudiants CSI : Mercredi 24 janvier 2018 - Salle L7
by Daniela Becker 18 Jan '18

18 Jan '18

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mercredi 24 janvier 2018 à partir de 14h00 en L7 au LRDE (KB). Les étudiants ING3 présenteront le résultat de leurs travaux des derniers mois. Au programme : SPOT — BIBLIOTHEQUE DE MODEL CHECKING 14h00 : Traduction efficace de formules LTL d’équité en automates déterministes – LAURENT XU En vérification formelle de la logique temporelle linéaire (LTL) à l’aide d’!-automates, la négation d’une formule LTL est traduite en !-automate. La construction d’un automate plus petit réduit beaucoup le temps d’exécution et la consommation mémoire des opérations suivantes de la chaîne de traitement de la vérification formelle. Müller et Sickert ont présenté une méthode efficace pour traduire n’importe quelle formule LTL en un petit automate déterministe. Cette méthode consiste à découper la formule en trois ensembles de sous-formules qui appartiennent respectivement au fragment de sureté ou de garantie, au fragment d’équité et au reste. Ils traduisent ensuite individuellement ces ensembles de sous-formules en automates déterministes qu’ils combinent par la suite. Spot peut déjà traduire les formules d’obligation en automates déterministes minimaux. Les formules d’obligation étant un surensemble des formules de sureté et de garantie, on généralise la traduction de Müller et Sickert en remplaçant le fragment de sureté ou de garantie par le fragment d’obligation. En ce qui concerne le fragment d’équité, ils ont présenté un algorithme de traduction efficace qui produit de petits automates déterministes. Ils ont également présenté comment construire efficacement un produit de ces automates avec d’autres automates. Nous présentons comment nous implémentons ces deux méthodes dans Spot. 14h30 : Tester l’appartenance à Persistence ou Récurrence dans Spot – ALEXANDRE GBAGUIDI AÏSSE Il existe une hiérarchie de propriétés temporelles, définie par Manna et Pnueli (1990). Cette hiérarchie contient entre autres les classes de récurrence et persistence. Savoir si une formule de logique temporelle à temps linéaire (LTL) f est récurrente (respectivement persistente) est intéressant car cela guarantit que f peut être traduit en un automate de Büchi déterministe (respectivement en un automate de co-Büchi). Auparavant, Spot, une bibliothèque de manipulation de formules LTL avait une unique façon de tester l’appartenance d’une formule aux classes de persistence ou récurrence. Grâce à nos précédents travaux présentés dans A co-Büching Toolbox, Spot a désormais deux façons de procéder. Nous avons comparé et amélioré ces deux méthodes en matière de temps d’exécution. 15h00 : Approches incrémentales pour la synthèse de contrôleur – THIBAUD MICHAUD Nous proposons deux approches incrémentales pour le problème de la synthèse de contrôleur à partir de spécifications en logique temporelle. Dans un travail antérieur, nous avons decrit notre implémentation d’un outil de synthèse de contrôleur reposant sur la réductibilité du problème à la résolution d’un jeu à parité, et avons établi que l’étape la plus coûteuse était la déterminisation d’un !-automate. Nous décrivons maintenant deux approches pour mitiger le problème : l’une est basée sur les automates good-for-games, et l’autre restreint les actions du contrôleur afin de simplifier la déterminisation. Nos expérimentations montrent que la deuxième approche est bien plus prometteuse que la première. Attention : le LRDE a déménagé, il se trouve au 24 rue Pasteur, 2e étage, au fond de la cour Pasteur (https://www.lrde.epita.fr/wiki/Contact) -- Daniela Becker Responsable administrative du LRDE

1 0

New Publication: "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"
by Colange Maximilien 05 Jan '18

05 Jan '18

We are happy to announce that the following article has been accepted for publication in the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), to be held in Thessaloniki, Greece, from April 14th to April 20th 2018. "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving" Hakan Metin (1), Souheib Baarir (1,2,3), Maximilien Colange (3), Fabrice Kordon (1) (1): Sorbonne Universités, UPMC, LIP6 CNRS UMR 7606, France (2): Université Paris Nanterre (3): LRDE, EPITA, Le Kremlin-Bicêtre, France Abstract: SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. /Static symmetry breaking /is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones. This paper presents a new way to handle symmetries, that avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions. -- Maximilien Colange Assistant Professor LRDE -- EPITA (+33) 1 53 14 59 45

1 0