November 2022 - Annonce

Paper published in Information & Computation
by Uli Fahrenberg 05 Mar '23

05 Mar '23

The following paper has been published in Information & Computation: Posets With Interfaces as a Model for Concurrency Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternativelytaking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures. https://www.lrde.epita.fr/wiki/Publications/fahrenberg.22.iandc

1 2

Paper accepted at FM 2023: Energy Problems in Finite and Timed Automata with Büchi Conditions
by Uli Fahrenberg 05 Mar '23

05 Mar '23

We are happy to announce that the following article has been accepted at the he 25th International Symposium on Formal Methods (FM 2023) to be held in Lübeck in March 2023: Energy Problems in Finite and Timed Automata with Büchi Conditions Sven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier Abstract: We show how to efficiently solve energy Büchi problems in finite weighted Büchi automata and in one-clock weighted timed Büchi automata; all our algorithms are implemented in a pipeline based on TChecker and Spot. Solving the latter problem is done by using the corner-point abstraction; the former problem is handled by a modified version of Bellman-Ford interleaved with Couvreur's algorithm. The paper is available at https://arxiv.org/abs/2205.04392

1 1

ELS 2023 is on track!
by Didier Verna 29 Nov '22

29 Nov '22

Dear collegues, I'm happy to announce that ELS 2023, the 16th European Lisp Symposium will be held in Amsterdam (and online) on April 24-25! A preliminary call for papers will follow soon. Stay tuned for updates. Best, -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Papiers acceptés
by Souheib Baarir 04 Nov '22

04 Nov '22

Hi every one, I'm happy to annonce the publication of the following papers : 1) In SETTA'2022 Title : Diversifying a parallel SAT solver with Bayesian Moment Matching Authors : V. Vallade, S.Nejati, J.Sopena, V. Ganesh and S. Baarir Abstract : In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores. The key insight underpinning our method is that Bayesian reasoning is a powerful way to guide the CDCL search procedure away from fruitless parts of the search space of a satisfiable Boolean formula, and towards those regions that are likely to contain satisfying assignments. 2) In VMCAI'2023 Title : CosySEL: Improving SAT Solving Using Local Symmetries Authors : S. Saouli , S. Baarir , C. Dutheillet and J. Devriendt Abstract : Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new tool, CosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of Local symmetries. We conduct our experiments on instances issued from the last ten sat competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems See you, Souheib.

1 0