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).
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
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
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.
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
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.
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
======================================================================
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