Annonce July 2019

annonce@lrde.epita.fr

1 participants
2 discussions

New publication: Generic Emptiness Check for Fun and Profit (ATVA'19)

by Alexandre Duret-Lutz

I'm happy to announce the the following article has been accepted in to the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19), to be held on October 27-31, 2019 in Taipei, Taiwan. Generic Emptiness Check for Fun and Profit Christel Baier (1), František Blahoudek (2), Alexandre Duret-Lutz (3), Joachim Klein (1), David Müller (1), and Jan Strejček (4) (1) Technische Universität Dresden, Germany (2) University of Mons, Belgium (3) LRDE, EPITA, Le Kremlin-Bicêtre, France (4) Masaryk University, Brno, Czech Republic We present a new algorithm for checking the emptiness of ω-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions. https://www.lrde.epita.fr/wiki/Publications/baier.19.atva -- Alexandre Duret-Lutz

5 years, 2 months

Spot 2.8 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.8 Spot is a library of algorithms for manipulating LTL formulas and omega-automata objects (as commonly used in model checking). This release contains code contributed by Clément Gillard and myself. A detailed list of new features is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that since Debian 10 ("Buster") was released a few days ago, the "stable" Debian packages we distribute are now built for Buster. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8 (2019-07-10) Command-line tools: - autfilt learned --highlight-accepting-run=NUM to highlight some accepting run with color NUM. - ltldo, ltlcross, and autcross are now preferring posix_spawn() over fork()+exec() when available. - ltlcross has new options --determinize-max-states=N and --determinize-max-edges=M to restrict the use of determinization-based complementation to cases where it produces automata with at most N states and M edges. By default determinization is now attempted up to 500 states and 5000 edges. This is an improvement over the previous default where determinization-based complementation was not performed at all, unless -D was specified. - ltlcross will now skip unnecessary cross-checks and consistency-checks (they are unnecessary when all automata could be complemented and statistics were not required). - genaut learned --m-nba=N to generate Max Michel's NBA familly. (NBAs with N+1 states whose determinized have at least N! states.) - Due to some new simplification of parity acceptance, the output of "ltl2tgba -P -D" is now using a minimal number of colors. This means that recurrence properties have an acceptance condition among "Inf(0)", "t", or "f", and persistance properties have an acceptance condition among "Fin(0)", "t", or "f". - ltldo and ltlcross learned shorthands to call the tools ltl2na, ltl2nba, and ltl2ngba from Owl 19.06. Similarly, autcross learned a shorthand for Owl's dra2dpa. Documentation: - https://spot.lrde.epita.fr/tut90.html is a new file that explains the purpose of the spot::bdd_dict object. Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that returns an accepting run in an automaton with any acceptance condition. - twa::accepting_run() and twa::intersecting_run() now work on automata using Fin in their acceptance condition. - simulation-based reductions have learned a trick that sometimes improve transition-based output when the input is state-based. (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now has 1 state instead of 2 in previous versions. Similarly, 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.) - simulation-based reductions hae learned another trick to better merge states from transiant SCCs. - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. These methods also exist in acc_cond::acc_code. - minimize_obligation() learned to work on very weak automata even if the formula or negated automaton are not supplied. (This allows "autfilt [-D] --small" to minimize very-weak automata whenever they are found to represent obligation properties.) - There is a new spot::scc_and_mark_filter objet that simplifies the creation of filters to restrict spot::scc_info to some particular SCC while cutting new SCCs on given acceptance sets. This is used by spot::generic_emptiness_check() when processing SCCs recursively, and makes it easier to write similar code in Python. - print_dot has a new option 'g', to hide edge labels. This is helpful to display automata as "graphs", e.g., when illustrating algorithms that do not care about labels. - A new complement() function returns complemented automata with unspecified acceptance condition, allowing different algorithms to be used. The output can be alternating only if the input was alternating. - There is a new class output_aborter that is used to specify upper bounds on the size of automata produced by some algorithms. Several functions have been changed to accept an output_aborter. This includes: * tgba_determinize() * tgba_powerset() * minimize_obligation() * minimize_wdba() * remove_alternation() * product() * the new complement() * the postprocessor class, via the "det-max-state" and "det-max-edges" options. - SVA's first_match operator can now be used in SERE formulas and that is supported by the ltl_to_tgba_fm() translation. See doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a new operator, any code that switches over the spot::op type may need a new case for op::first_match. Furthermore, the output of "randltl --psl" will be different from previous releases. - The parser for SERE learned to recognize the ##n and ##[i:j] operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is replaced in different ways depending on the values of i, a, and b. The formula::sugar_delay() function implements this SVA operator in terms of the existing PSL operators. ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. - The F[n:m] and G[n:m] operators introduced in Spot 2.7 now support the case where m=$. - spot::relabel_apply() makes it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula. - The LTL simplifier learned the following rules: F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ") G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") (f & g) R h = f R h if h implies g (f & g) M h = f M h if h implies g (f | g) W h = f W h if g implies h (f | g) U h = f U h if g implies h Gf | F(g & eventual) = f W (g & eventual) if !f implies g Ff & G(g | universal) = f M (g | universal) if f implies !g f U (g & eventual) = F(g & eventual) if !f implies g f R (g | universal) = G(g | universal) if f implies !g - cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, colorize_parity() learned that coloring transitiant edges does not require the introduction of a new color. - A new reduce_parity() function implements and generalizes the algorithm for minimizing parity acceptance by Carton and Maceiras (Computing the Rabin index of a parity automaton, 1999). This is a better replacement for cleanup_parity() and colorize_parity(). See https://spot.lrde.epita.fr/ipynb/parity.html for examples. - The postprocessor and translator classes are now using reduce_parity() for further simplifications. - The code for checking recurrence/persistence properties can also use the fact the reduce_parity() with return "Inf(0)" (or "t" or "f") for deterministic automata corresponding to recurrence properties, and "Fin(0)" (or "t" or "f") for persistence properties. This can be altered with the SPOT_PR_CHECK environment variable. Deprecation notices: - The virtual function twa::intersecting_run() no longuer takes a second "from_other" Boolean argument. This is a backward incompatibility only for code that overrides this function in a subclass. For backward compatibility with programs that simply call this function with two argument, a non-virtual version of the function has been introduced and marked as deprecated. - The spot::acc_cond::format() methods have been deprecated. These were used to display acceptance marks, but acceptance marks are unrelated to acceptance conditions, so it's better to simply print marks with operator<< without this extra step. Bugs fixed: - The gf_guarantee_to_ba() is relying on an inplace algorithm that could produce a different number of edges for the same input in two different transition order. - A symmetry-based optimization of the LAR algorithm performed in spot::to_parity() turned out to be incorrect. The optimization has been removed. "ltlsynt --algo=lar" is the only code using this function currently. -- Alexandre Duret-Lutz

5 years, 3 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce July 2019