I am happy to announce that the following paper has been accepted in
the Conference on Formal Techniques for Distributed Objects,
Components and Systems (FORTE'14), to be held in Berlin on June 3–6.
Mechanizing the Minimization of
Deterministic Generalized Büchi Automata
Souheib Baarir (1,2) and Alexandre Duret-Lutz (3)
(1) Université Paris Ouest Nanterre la Défense
(2) Sorbonne Universités, UPMC Univ. Paris 6, LIP6
(3) EPITA, LRDE
https://www.lrde.epita.fr/wiki/Publications/baarir.14.forte
Abstract:
Deterministic Büchi automata (DBA) are useful to (probabilistic)
model checking and synthesis. We survey techniques used to obtain
and minimize DBAs for different classes of properties. We extend
these techniques to support DBA that have generalized and
transition-based acceptance (DTGBA) as they can be even smaller. Our
minimization technique—a reduction to a SAT problem—synthesizes a
DTGBA equivalent to the input DTGBA for any given number of states
and number of acceptance sets (assuming such automaton exists). We
present benchmarks using a framework that implements all these
techniques.
--
Alexandre Duret-Lutz
Bonjour,
nous avons le plaisir de vous annoncer la sortie du n°30 du bulletin du LRDE.
Ce numéro résume les dernières bonnes nouvelles du LRDE,
les avancées du projet Vaucanson 2 et les dernières publications du labo.
Vous pouvez télécharger le bulletin en couleur à la page suivante :
https://www.lrde.epita.fr/wiki/Latest_issue
--
Daniela Becker
Responsable administrative du LRDE
ELS'14 - 7th European Lisp Symposium
IRCAM, Paris, France
May 5-6, 2014
http://www.european-lisp-symposium.org/
Sponsored by IRCAM, CNRS, UPMC, EPITA, LispWorks, Franz Inc.
Latest News:
* SUBMISSION DEADLINE EXTENDED. You have two more week to submit!
* Registration is now open. Early registration fee until April 13.
See http://www.european-lisp-symposium.org/content-registration-full.html
The purpose of the European Lisp Symposium is to provide a forum for
the discussion and dissemination of all aspects of design,
implementation and application of any of the Lisp and Lisp-inspired
dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP,
Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We
encourage everyone interested in Lisp to participate.
The 7th 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
Please note that IRCAM, the conference venue, is a French institute
for research on music and acoustics. Submissions relating Lisp to
music or other acoustical matters will hence be particularly welcome,
although given no heightened favor during the review process.
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 2 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.
The symposium will also provide slots for lightning talks, to be
registered on-site every day.
All submissions should be formatted following the ACM SIGS guidelines
and include ACM classification categories and terms. For more
information on the submission guidelines and the ACM keywords, see:
http://www.acm.org/sigs/publications/proceedings-templates and
http://www.acm.org/about/class/1998.
Important dates:
- TODAY: Mark your calendar. Start planning now!
- 23 Mar 2014: Submission deadline **** EXTENDED ****
- 31 Mar 2014: Notification of acceptance
- 13 Apr 2014: Early registration deadline
- 21 Apr 2014: Final Papers due
- 05 May 2014: Symposium. Join us there!
Programme chair:
Kent Pitman, Hypermeta Inc., U.S.A.
Local chairs:
Didier Verna, EPITA Research Lab, France
Gérard Assayag, IRCAM, Paris, France
Programme committee:
Marie Beurton-Aimar — LaBRI, University of Bordeaux, France
Pierre Parquier — IBM France Lab, Paris, France
Rainer Joswig — Hamburg, Germany
Guiseppe Attardi — Università di Pisa, Italy
Taiichi Yuasa — Kyoto University, Japan
António Leitão — IST/Universidade de Lisboa, Portugal
Christophe Rhodes — Goldsmiths, University of London, UK
Olin Shivers — Northeastern University, USA
Charlotte Herzeel — IMEC, ExaScience Life Lab, Leuven, Belgium
Local organizers:
Daniela Becker, EPITA Research Lab, France
Sylvie Benoit, IRCAM, Paris, France
Search Keywords:
#els2014, ELS 2014, ELS '14, European Lisp Symposium 2014,
European Lisp Symposium '14, 7th ELS, 7th European Lisp Symposium,
European Lisp Conference 2014, European Lisp Conference '14
Ircam STMS Lab, IRCAM / CNRS / UPMC
--
Resistance is futile. You will be jazzimilated.
Lisp, Jazz, Aïkido: http://www.didierverna.info
========================================================================
Séminaire MeFoSyLoMa
http://www.mefosyloma.fr/
Méthodes Formelles pour les Systèmes Logiciels et Matériels
vendredi 28 Mars 2014, 14h-17h
Adresse:
LRDE (EPITA), Salle Alpha
Bâtiment X, 2e étage
18 rue Pasteur, 94270 Le Kremlin-Bicêtre
Métro Porte d'Italie
Plans d'accès :
https://www.google.com/maps?q=48.8152808,2.3623765https://www.lrde.epita.fr/~adl/dl/access-lrde.pdf
========================================================================
Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires
Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC),
LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de
Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la
confrontation de différentes approches ou points de vue sur
l'utilisation des méthodes formelles dans les domaines du génie
logiciel, de la conception de circuit, des systèmes répartis, des
systèmes temps-réel ou encore des systèmes d'information. Il
s'organise autour de réunions bimestrielles où sont exposés des
travaux de recherche récents sur ce thème.
========================================================================
Programme
14h00-15h00
Laura Carnevali - Université de Florence, "Quantitative evaluation
of non-Markovian models through the approach of stochastic state
classes: applications and future issues"
Abstract: The method of stochastic state classes supports steady
state and transient analysis of models that encompass multiple
timers with general distribution and possibly bounded
support. When the model underlies a Markov Regenerative Process
(MRP) that always reaches a regeneration point within a finite
number of steps, transient analysis can be limited to the first
regeneration epoch and repeated from every regenerative
point. This supports efficient derivation of the local and global
kernels that characterize the MRP behavior and enables transient
evaluation through the numerical integration of generalized Markov
renewal equations. Applications of the approach through the Oris
Tool are illustrated referring to the evaluation of availability
measures for maintenance procedures. Future research directions
are discussed in the area of probabilistic schedulability analysis
of real-time systems.
15h00-15h30
Ridha Benosman - CNAM, "Conception et Évaluation de Performances
d'un Bus Applicatif Parallèle et Orienté Service"
Abstract: De nombreuses solutions d'intégration d'applications à
base d'ESB on été proposées. Cependant, ces solutions
d'intégration ne supportent pas le traitement parallèle. et ne
tirent donc pas profit des technologies multicoeurs.
Nous proposons une solution de type "bus" permettant le traitement
parallèle. Pour cela, nous avons conçu et mis en oeuvre : un
mécanisme de multiplexage/démultiplexage en mesure de contrôler la
circulation du flux de données, un allocateur dynamique de
mémoires partagées répondant à certaines limitations du standard
des mémoires IPC et un nouveau connecteur permettant à l'ensemble
des threads d'une même application mère de fonctionner
simultanément sur des zones mémoires complètement disjointes.
15h30-16h00:
Pause café
16h00-16h30:
Vie du groupe
========================================================================
--
Alexandre Duret-Lutz
I am happy to announce that the following paper has just been
published in Vol. 5 of the International Journal on Critical
Computer-based Systems:
LTL Translation Improvements in Spot 1.0
Alexandre Duret-Lutz (LRDE/EPITA)
This is an extended version of my VECOS'11 paper, that was submitted
to IJCCBS in October 2012, accepted in April 2013, and published in
March 2014.
https://www.lrde.epita.fr/wiki/Publications/duret.14.ijccbs
Abstract:
Spot is a library of model-checking algorithms started in 2003.
This paper focuses on its module for translating linear-time
temporal logic (LTL) formulas into Büchi automata: one of the
steps required in the automata-theoretic approach to LTL
model-checking.
We detail the different algorithms involved in this translation: the
core translation itself, which performs many simplifications thanks
to its use of binary decision diagrams; the pre-processing of the LTL
formulas with rewriting rules chosen to help their translation;
and various post-processing algorithms whose use depends on the
intent of the translation: do we favor deterministic automata, or
small automata?
Using different benchmarks, we show how Spot competes with other
LTL translators, and how it has improved over the years.
--
Alexandre Duret-Lutz
Bonjour,
nous avons le plaisir de vous annoncer que le Laboratoire de Recherche
et Développement de l'EPITA (LRDE) a été retenu pour le programme de recherche
bilatéral franco-tchèque PHC Barrande 2014.
Ce programme a pour objectif de favoriser les échanges scientifiques et
technologiques entre des laboratoires de recherche des deux pays.
Le financement accordé pour le LRDE permettra de réaliser des actions de mobilité
de jeunes chercheurs, de doctorants et post-doctorants dans le cadre du projet Spot
avec le partenaire tchèque, la Faculté d'Informatique de la Masaryk University à Brno.
Pour en savoir plus : http://www.campusfrance.org/fr/barrande
--
Daniela Becker
Responsable administrative - LRDE
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 12 mars 2014 (11h--12h30), Salle L0 du LRDE.
Au programme:
* 11h-12h30: Programmation d'applications Web client-serveur avec Ocsigen
-- Vincent Balat, Université Paris Diderot et INRIA
http://ocsigen.org
Le Web a subi en quelques années une évolution radicale, passant d'une
plateforme de données à une plateforme d'applications. Mais la plupart
des outils de programmation n'ont pas été conçus pour cette nouvelle
vision du Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de
programmation adaptées aux besoins des sites Web modernes et des
applications Web distribuées. Il permet de programmer les parties client
et serveur dans le même langage, et même, comme une seule et même
application. La puissance expressive du langage OCaml permet
d'introduire une abstraction des technologies sous-jacentes dans le but
de simplifier la programmation d'interactions Web complexes. Le système
de types très avancé du langage permet d'améliorer la fiabilité des
programmes et le respect des standards. Cela permet aussi de réduire
beaucoup le temps de développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire
un exemple d'application simple.
-- Vincent Balat est maître de conférences à l'université Paris Diderot,
actuellement en délégation à l'INRIA. Il est le créateur et chef du
projet Ocsigen. Il est ancien élève de l'École Normale Supérieure de
Cachan. Son travail de recherche porte essentiellement sur
l'amélioration de l'expressivité et de la fiabilité des techniques de
programmation Web.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/seminaire