Séminaire interuniversitaire de logique mathématique (3ème cycle FNRS)
 Sauf mention contraire, le cours de DEA et les séminaires du jeudi après-midi ont lieu à l'ULB, Campus de la Plaine, au local 2NO906. Un itinéraire (bilingue) est disponible. Les exposés du vendredi ont lieu
à l'UMH, Campus de la Plaine.
 

 

Programme 2004-2005
Pour recevoir le programme par email lors de ses mises à jour, laissez-nous vos coordonnées à l'adresse
http://www.umh.ac.be/math/logic/logicdb/inscription.php

Programme ULB-UMH

 

  Second semestre (Janvier-Mars)

2005

Cours du matin (11h - 12h30)

Exposés de l'après-midi (14h30 - 16h)

20 janvier, ULB,
local 2NO906

Pas de séance

 

Thomas Brihaye (UMH)
Vérification d'automates temporisés avec poids.

03 février, ULB,
local 2NO906

Pas de séance

Roland Hinnion (ULB)
Un modèle de termes pour une théorie predicative, intensionnelle des ensembles partiels.

10 février, ULB,
local 2NO906

Pas de séance

Sonja Smets (VUB)
On Quantum Transition Systems and Quantum Dynamic Algebra

17 févier, ULB,
local 2NO906

Pas de séance

M.Schellekens (Cork)
Towards a Calculus for Modular Software Timing

24 février, ULB,
local 2NO906

Pas de séance

Georges Hansoul (ULg)
Bisimulations en algèbre universelle

03 mars, ULB,
local 2NO906

Pas de séance

Léon Horsten (KUL)
Partial Kripke-Feferman (joint work with Volker Halbach, Oxford University)

10 mars, ULB,
local 2NO906

Pas de séance

Bruno Teheux (ULg)
Opérateurs sur les MV-algèbres

17 mars, ULB,
local 2NO906

Pas de séance

Philippe Kreutz (ULB)
L'extensionalité des rapports de perception

24 mars,ULB,
local 2NO906

Pas de séance

Marc Peeters (ULB)
Présentation de la méréologie de Lesniewski

14 avril, ULB,
local 2NO906

Pas de séance

Michel Rigo (Ulg)
Système de numération et régularité pour les polynômes sur un corps fini

21 avril, ULB,
local 2NO906

Pas de séance

Emilie Charlier (ULg)
Systèmes de numération et reconnaissabilité

28 avril, ULB,
local 2NO906

Pas de séance

Jacques Riche (KUL)
Logiques Relevantes

5 mai

Congé

Congé

12 mai, ULB,
local 2NO906

Pas de séance

Pas de séance

19 mai, ULb,
local 2NO906

Pas de séance

Pas de séance

!!! du vendredi 20 mai au dimanche 22 mai à Gand !!!

JOINT BeNeLuxFra CONFERENCE in MATHEMATICS

JOINT BeNeLuxFra CONFERENCE in MATHEMATICS

26 mai, ULB,
local 2NO906

Pas de séance

Marc Dominicy (ULB)
En quoi les langages naturels sont-ils « informels »?

2 juin, ULB,
local 2NO906

Pas de séance

Pas de séance

9 juin, ULB,
local 2NO906

Pas de séance

D. Niwinski (Warsaw University)
On the complexity of infinite computations

16 juin, ULB,
local 2NO906

K.Meer (Odense)
Real number models and probabilistically checkable proofs

Pas de séance

Résumés:

Damian Niwinski (Warsaw) "On the complexity of infinite computations"
Finite-state automata constitute the very basic level in classical complexity theory. In contrast, when applied to infinite words and trees, they reveal a remarkable definability power, going beyond the Borel hierarchy. Still, some good properties of finite automata remain, like decidability of normal forms. The talk will compare various complexity hierarchies with the emphasis on decidability questions, and present some recent results obtained by the author in collaboration with Igor Walukiewicz and Filip Murlak.
The transparencies are available here.

Klaus Meer (Odense) "Real number models and probabilistically checkable proofs"
Probabilistically checkable proofs (PCPs) represent one of the most important recent areas in theoretical computer science . The idea is to make verification proofs of NP-problems more stable: Reading only a {\em constant}number of data units in such a potential proof will be sufficient to detect faults with high probability.
In this talk we introduce the PCP notion for the real number model of Blum, Shub, and Smale. We then study the existence of certain such ``transparent'' proofs for the class NP$_{\mathbb R}$ of real number decision problems verifiable in polynomial time.

Jacques Riche (KUL) "Logiques relevantes"
Dans une première partie, on pourra expliquer ce qu'il faut entendre par "Logique Relevante" en présentant les motivations historiques à partir des paradoxes classiques liés à l'implication matérielle, depuis Lewis et l'implication stricte jusqu'à Church, Ackermann et l'Entailment de Anderson & Belnap. Pour situer ces logiques en termes plus familiers, on pourrait dire qu'elles sont non-classiques, non-monotones et paraconsistantes.
Si ces motivations reposent sur des arguments aussi bien philosophiques que logiques, une approche plus neutre, algébrique, du genre Curry, permet de la comparer à l'algèbre booléenne, par exemple, et d'arriver à une caractérisation algébrique de différents systèmes de ces logiques (groupoïdes résidués, monoïdes de De Morgan, distributoïdes etc.). L'intérêt de cette caractérisation est de montrer que ces logiques, dotées d'une sémantique appropriée, dite "de Routley-Meyer", ont une contrepartie algébrique naturelle. Une théorie de la représentation permet alors de relier leurs aspects sémantiques et algébriques et d'éclairer ainsi la partie logique qui concerne la relation d'implication ou de conséquence logique. Puisque c'est de cela qu'il s'agit.
Dans une seconde partie, on évoquera de manière plus ou moins détaillée quelques questions particulières liées à ces logiques. Par exemple, leurs rapports avec la logique classique, avec la logique combinatoire et le lambda calcul, les questions de décision et de complexité; leurs rapports avec l'arithmétique, l'algèbre, la théorie des nombres, la théorie des modèles etc. Ou encore certaines caractéristiques propres qui les distinguent dans le domaine plus général de la logique.

Marc Peeters (ULB) "Présentation de la méréologie de Lesniewski"
Après une présentation de l'auteur, je traiterai de la solution que Lesniewski a apportée à l'antinomie de Russell, résolution qui débouche sur la méréologie. Ensuite, j'aborderai quelques pistes contemporaines.

Marc Dominicy (ULB): En quoi les langages naturels sont-ils « informels »?

Philippe Kreutz (ULB) "L'extensionalité des rapports de perception"
Il est bien connu que des verbes tels que voir et entendre possèdent un sens perceptuel dans les énoncés avec construction infinitivale mais éventuellement un sens épistémique dans les énoncés avec une complétive en «que». Les premiers, au contraire des seconds, respectent (sauf vis-à-vis des expressions propositionnelles) le principe de substitution salva veritate des expressions co-référentielles. La distinction classique entre les attributions de re et de dicto s’avère insatisfaisante pour rendre compte de cette donnée et ce, aussi bien dans une perspective frégéenne que dans une approche millienne de la référence. A la lumière des travaux de [Dretske, 1981] et de [Stenning & Inder, 1995), nous montrerons que cette divergence de comportement à l’égard du principe de substitution s’explique plutôt par la nature respective (analogique Vs non-analogique) des représentations liées aux modalités perceptuelles et épistémiques.

Bruno Teheux(ULg): Dualité pour des MV-algèbres à opérateurs
Nous commencerons par définir une notion d'opérateur sur les MV-algèbres en discutant des différentes axiomatisations qu'il aurait été possible d'utiliser. Nous construirons ensuite une dualité pour la classe des MV-algèbres à opérateurs dont la MV-algèbre sous-jacente est dans une variété finiment engendrée déterminée. Cette dualité est une extension de la dualité connue pour les algèbres de Boole à opérateurs. Nous obtiendrons une axiomatisation de la catégorie duale et nous intéresserons à la construction des sommes dans cette catégorie. Enfin, nous aborderons le problème de l'extension d'un opérateur défini sur l'algèbre de Boole des idempotents d'une MV-algèbre en un opérateur sur la MV-algèbre.

Léon Horsten (KUL):"Partial Kripke-Feferman (joint work with Volker Halbach, Oxford University)"
Feferman and Reinhardt have formalized Kripke's semantical partial inductive theory of truth in classical logic. The resulting system, KF (Kripke-Feferman), has been extensively studied. We argue that for philosophical reasons, Kripke's semantical theory should be formalized in partial logic. We undertake this task, and investigate the proof-theoretical strength of the resulting proof system.

Georges Hansoul (ULg) "Bisimulations en algèbre universelle"
Des disciplines mathématiques variées ont eu recours sous des dénominations diverses à ce qui est maintenant à la mode sous le nom de bisimulation.Il s'agit tout simplement de l'usuel concept d'homomorphisme pour des structures où les fonctions peuvent prendre plusieurs valeurs en un point.Cette simple observation permet un petit traitement algébrique du concept, que nous présentons ici, ainsi que deux applications: algèbres de Boole et logique modale.

M.Schellekens (Cork):"Towards a Calculus for Modular Software Timing"
The Centre for Efficiency-Oriented Languages CEOL (http://www.ceol.ucc.ie/) was set up with initial funding of Euro 1M from Science Foundation Ireland and collaborates with Sun Microsystems. Software Timing is crucial for many Computer Science applications. Yet timing is well known to quickly lead to difficult mathematical problems. CEOL focuses on the development of a new programming language ACETT: the Average-Case Execution Time Tool. ACETT is currently implemented at CEOL in Java 5.0 In this talk we outline the new mathematical principles which have led to the development of ACETT and how this approach affects four mainstream Computer Science areas: Automated Average-Case Analysis, Semantics & Complexity, Random Structures and Real-Time Languages. Average-Case Time Analysis is one of the most thoroughly studied areas of Computer Science and is notoriously difficult, involving a variety of techniques which, typically, do not allow for automation. Currently algorithms must be analyzed on a case-by-case basis, and it is not feasible in general to express the Average-Case time of algorithms via a recurrence equation, though excellent techniques are available to solve these recurrences. A well-known example of an algorithm for which the exact average-case time is not known is the sorting algorithh Heapsort, as discussed by Knuth, Edelkamp and Flajolet.
We introduce a new unified approach to Average-Case Time analysis and outline the mathematical ideas which led to this development. The novel programming language ACETT is proposed for which the Average-Case Time Complexity is shown to be Linearly-Compositional; i.e. the Average-Case Time of ACETT-programs can be expressed as linear combinations of the Average-Case Time of their basic components. This considerably simplifies the Average-Case Time analysis of ACETT-programs and opens the way for (semi-)automation via modular timing. We discuss a new ACETT-version of Heapsort, Percolating Heapsort, for which the exact time analysis is possible (as opposed to classical Heapsort). Finally, we give an overview of future work in this area.

Sonja Smets (VUB) "On Quantum Transition Systems and Quantum Dynamic Algebra" (Joint work with A. Baltag, Comlab, Oxford University)
I will first introduce the classical setting of Propositional Dynamic Logic (PDL). This classical setting will be compared to a Quantum version of Propositional Dynamic Logic (called QPDL). I will focus mainly on the Kripke style semantics for QPDL, i.e. on Quantum Transition Systems. Next I will give (short) outlines of the Proof System and of the Dynamic Algebra. These axiomatizations of QPDL solve a lot of problems: 1) These axiomatizations are complete with respect to infinite Hilbert spaces endowed with (phase-free) quantum actions! 2) QPDL supports my previous work on this issue by providing a clear and intuitive dynamic-operational meaning to key postulates such as Orthomodularity and the Covering Law. 3) QPDL provides a link between traditional quantum logic and the needs of quantum computation.

Roland Hinnion (ULB): "Un modèle de termes pour une théorie predicative, intensionnelle des ensembles partiels"
Il est bien connu que, parmi les théories ensemblistes basées sur une forme de compréhension (/abstraction) "positive", celles qui sont "classiques" et celles qui sont "paraconsistantes" ont été étudiées avec succès, et que l'on dispose de modèles (entre autres topologiques) très riches. Par contre, la version "ensembles partiels" (/ensembles naifs dans des logiques "paracomplètes"ou "partielles") résiste étrangement aux techniques connues. Cet exposé montrera que la technique de "forcing" employée pour les ensembles positifs fournit un résultat dans le cas "partiel" également.

Thomas Brihaye (UMH): "Vérification d'automates temporisés avec poids" (travail en collaboration avec Véronique Bruyère et Jean-François Raskin)
Dans cet exposé, on étudiera le problème de "model checking" (vérification) sur le modèle des automates temporisés avec poids (weighted timed automata) pour la logique WCTL. On commencera par rappeler et illustrer les notions suivantes: automates temporisés (introduits par Alur et Dill en 90), logique CTL (introduite par Clarke, Emerson, Halpren au début des années 80). Ensuite, on expliquera comment et pourquoi, on introduit les automates temporisés avec poids et la logique WCTL. On se consacrera ensuite à l'étude de la décidabilité de WCTL. Cette étude nécessitera l'utilisation de l'outil bisimulation que l'on rappelera au préalable.

 

Premier semestre (Octobre-Décembre)

2004

Cours du matin (11h - 12h30), sauf mention contraire

Exposés de l'après-midi (14h30 - 16h), sauf mention contraire

7 octobre
UMH, bâtiment le Pentagone, salle 0A11.

Fundamental Computer Science F.N.R.S. Contact Group Meeting on Constraints in Computer Science

Fundamental Computer Science F.N.R.S. Contact Group Meeting on Constraints in Computer Science

14 octobre
ULB,
local 2NO906

cours de DEA : Logique et Géométrie
 Christian Michaux (UMH)
Espaces définissables et quotients dans les structures o-minimales, d'après van den Dries.

Felix Klaedtke (ETH Zurich)

On the Automata Size for Presburger Arithmetic

21 octobre
ULB,
local 2NO906

suite du cours de DEA par C. Michaux.

Thomas Brihaye (UMH)

Bisimulations de systèmes dynamiques et combinatoire des mots

28 octobre
UMH

exceptionnellement, pas de séance à l'ULB.

suite du cours de DEA par C. Michaux,
!!!! exceptionnellement à l'UMH, au local 2D20 (salon bleu) du 2ième étage, Pentagone !!!!

4 novembre

pas de séance

Olivier Esser (ULB)

Topologie et modèle de termes dans NF

5 novembre
UMH

vv

suite du cours de DEA par C. Michaux,
!!! à l'UMH, au local 2D20 (salon bleu) du 2ième étage, Pentagone !!!

11 novembre

Congé

Congé

18 novembre

TBA

Roland Hinnion (ULB)

Intensional positive sets

19 novembre
UMH

vv

suite du cours de DEA par C. Michaux,
!!! à l'UMH, au local 2D20 (salon bleu) du 2ième étage, Pentagone !!!

25 novembre

TBA

Nicolas Guzy (UMH)

Corps de Hardy

2 décembre

TBA

Marcel Crabbé (UCL)

Sémantique sans coupures

3 décembre
UMH, exceptionnellement de 14h à 17h

 

TBA

Cédric Rivière (UMH)

Relations d'équivalence définissables dans les structures o-minimales et élimination des imaginaires (d'après A. Pillay)

9 décembre

TBA

Nicolas Guzy (UMH)

Corps de séries logarithmique-exponentielles

16 décembre

TBA

Thierry Libert (ULB)

Des modèles topologiques pour l'abstraction positive et l'élimination des quantificateurs

13 --17 décembre

MOVEP'04 à l'ULB

MOVEP'04 à l'ULB

23 décembre

Congé

Congé

Résumés:

Cédric Rivière (UMH):"Relations d'équivalence définissables dans les structures o-minimales et élimination des imaginaires (d'après A. Pillay)"
Nous exposerons l'article de Anand Pillay : Some remarks on definable equivalence relation in o-minimal structures, paru dans le JSL, 51, 3, 1986.

Thierry Libert (ULB):"Des modèles topologiques pour l'abstraction positive et l'élimination des quantificateurs"
Le sujet de l'exposé est l'abstraction positive en théorie des ensembles. Par "abstraction" - au lieu de "compréhension" - il est sous-entendu que le langage est muni d'un abstracteur "{-|-}" permettant la formation de termes primitifs. Je démonterai ici l'existence de modèles $\kappa$-topologiques, pour tout cardinal régulier $\kappa$. Une propriété caractéristique des modèles canoniques nous amènera alors à prouver l'élimination des quantificateurs pour les formules positives de la théorie. Enfin, nous illustrerons aussi l'utilité des modèles topologiques pour établir de simples résultats d'indépendance.

Nicolas Guzy (UMH): "Corps de séries logarithmique-exponentielles"
Suite à l'exposé du 25/10, nous allons introduire un autre exemple de corps valué différentiel qui joue un rôle central en algèbre différentielle ordonnée: le corps des séries logarithmiques-exponentielles. Il s'agit d'étendre le corps des séries de Laurent sur les réels de façon canonique afin de le munir d'une exponentiation qui "se comporte bien". Nous allons dans cet exposé confronter les différentes approches (van den Dries, Marker, Macintyre et Kulhmann) de ce problème.

Nicolas Guzy (UMH): "Corps de Hardy"
Rosenlicht a introduit dans les années 70 la notion de corps valué différentiel, c'est-à-dire un corps muni d'une dérivation et d'une valuation qui interragissent fortement (en particulier la dérivation est continue pour la topologie de la valuation). Nous allons, au fil d'exemples canoniques tels que les corps de Hardy, développer les notions naturelles liées à ces valuations. Nous parlerons ainsi des couples asymptotiques étudiés récemment de façons modèle-théorique par van den Dries et Aschenbrenner.

Marcel Crabbé (UCL):"Sémantique sans coupures"
Nous caractériserons la validité relativement aux modèles véritablement gloutons pour des schémas de compréhension. Nous proposerons ainsi un autre regard sur le phénomène d'absorption des coupures. Nous terminerons en indiquant une raison pour laquelle l'axiome d'extensionnalité écrit sans égalité (avoir les mêmes éléments implique avoir les mêmes propriétés) est fragile à l'extrême.

Roland Hinnion (ULB): "Intensional positive sets"
Positive extensional set theory is well-known nowadays; here we discuss the possibility of replacing extensionality by intensionality; we compare the systems, and discuss also the compatibility with ordinary (ZF-) sets. The main construction is a (rather) simple forcing;the hope is to apply that later to analogue (but still open) problems concerning partial sets...

Olivier Esser (ULB): "Topologie et modèle de termes dans NF"
Dans cet exposé, nous étudierons diverses topologies associées à NF et plus particulièrement la topologie de Stone associée aux modèles de permutations de NF: pour un modèle V de NF et une formule \phi, on déclare ouvert les ensembles suivants {\sigma | V^{\sigma} |= \phi}

Thomas Brihaye (UMH): "Bisimulations de systèmes dynamiques et combinatoire des mots"
Dans cet exposé, je commencerai par rappeler la notion de bisimulation entre deux systèmes de transition. Je la comparerai ensuite avec la notion d'equivalence de langage (dans le cas de systèmes finis). Le reste de l'exposé sera consacré à une analyse combinatoire de la notion de bisimulation entre systèmes dynamiques. On expliquera entre autre comment encoder des trajectoires de systèmes continus à travers des mots. Enfin, on donnera une étude systématique de cette technique qui a été introduite dans le but d'étudier les automates hybrides o-minimaux.

Felix Klaedtke (ETH Zurich): "On the Automata Size for Presburger Arithmetic"
Presburger arithmetic is the first-order theory with addition and the ordering over the integers. Its decidability was first proved independently by Presburger and Skolem by the method of quantifier elimination. Its complexity has been investigated intensively since. Due to the applicability of Presburger arithmetic in various domains (e.g., system verification and compiler optimization) it is important to have effective decision procedure for Presburger arithmetic or fragments of it.
Recently, it has become popular to use automata for deciding Presburger arithmetic. An idea that goes at least back to an article by Buechi in 1960: Integers are represented as words (e.g., using the 2's complement representation), and the automata are recursively constructed from the formulas. The constructed automaton for a formula precisely accepts the words representing integers which make the formula true. A crude complexity analysis on such an automata-based decision procedure leads to a non-elementary worst-case complexity. However, empirical results show that automata-based decision procedures are competitive to other methods.
In this talk we analyze this automata-based approach. Our analysis provides a triple exponential upper bound on the size of the minimal deterministic automaton for a Presburger arithmetic formula, and it partly explains the "good" empirical results. Our analysis is based on a comparison of automata and quantifier-free formulas that are obtained by an improvement of Cooper's quantifier elimination method for Presburger arithmetic. Moreover, we give an example showing that this triple exponential upper bound on the automata size is tight (even for nondeterministic automata). Slides of the talk.

cours de DEA : Logique et Géométrie
 Christian Michaux (UMH)
"Espaces définissables et quotients dans les structures o-minimales, d'après van den Dries".
Dans cette série de lectures, nous introduirons la catégorie d'espaces définissables dans le cadre des structures o-minimales. Nous commencerons par montrer que cette notion est indépendante de l'atlas sous-jacent et est caractérisée par le faisceau induit. On montrera que les espaces définissables affines sont exactement ceux dont la topologie est régulière. Cette étendue sera ensuite étendue aux groupes définissables (en particulier linéaires algébriques) et à leur quotients (sous une action). Ces résultats constituent une extension de résultats de la géométrie semi-algébrique réelle.

Fundamental Computer Science F.N.R.S. Contact Group:

The theme of the day will be « Constraints in Computer Science ». This includes constraints in databases, constraint programming, constraints in verification, constraints for the modeling of combinatorial problems, constraints and logic.
Registration : registration is by email. If you wish to participate in this FNRS day, please send your name and surname, affiliation and email to the secretary of the group Prof. J.-F. Raskin (jraskin@ulb.ac.be). There are no registration fees. The closing date for registrations is october 1, 2004.

The schedule of the day is as follows:
9h : Welcome
9h15 - 10h : Alexander Serebrenik, "On termination of binary CLP programs"
10h - 10h30 : Coffie break
10h30 -11h30 : Invited talk. Prof. B. Kuijpers (University of Limburg) "Constraint Databases, Data Structures and Efficient Query Evaluation"
11h30 - 12h15 : Floris Geert, "On the decidability of termination of query evaluation in transitive closure logics for polynomial constraint databases"
12h15 - 14h : Lunch break
14h -14h45 : Isabelle Dony, "A Program Verification System Based on Oz"
14h45-15h30 : Louis Latour, "From Automata to Formulas: Convex Integer Polyhedra"
15h30 - 16h : Coffie break
16h - 16h45 : Axel Legay, "Boolean Binary Decision Diagrams (ongoing work)"
16h45-17h30 : Hadrien Mélot, "Discovering optimal inequalities among graph invariants with the help of a computer"

Here are the abstracts of the talks :
Alexander Serebrenik, "On termination of binary CLP programs"
Termination of binary CLP programs has recently become an important question in the termination analysis community. The reason for this is due to the fact that some of the recent approaches to termination of logic programs abstract the input program to a binary CLP program and conclude termination of the input program from termination of the abstracted program.
In this paper we introduce a class of binary CLP programs such that their termination can be proved by using linear level mappings. We show that membership to this class is decidable and present a decision procedure.
Further, we extend this class to programs such that their termination proofs require a combination of linear functions. In particular we consider as level mappings tuples of linear functions and piecewise linear functions.

Geert Floris: "On the decidability of termination of query evaluation in transitive closure logics for polynomial constraint databases".
In this talk we present extensions of first-order logic with different types of transitive-closure operators and report on decidability results related to the termination of the evaluation of queries expressible in these transitive-closure logics on constraint databases.
It turns out that termination is undecidable in general. However, we identify some cases where the decision problem becomes decidable, and even expressible in first-order logic over the reals. Based on this result, we identify a particular transitive-closure logic for which termination of query evaluation is decidable and which is more expressive than first-order logic over the reals.
Furthermore, we can define a guarded fragment in which exactly the terminating queries of this language are expressible.

Isabelle Dony, "A Program Verification System Based on Oz"
We present an imperative program verification system that exploits many powerful aspects of Oz. Our verification system supports an expressive assertion language for writing specifications and loop invariants. It is able to prove the correctness of elaborated imperative programs consisting of several subproblems that are checked independently.
We illustrate the functionalities of our system on a few non trivial examples. Then, we explain that, using Oz constraint programming and other convenient programming mechanisms of Oz, the implementation of the system is straightforward. We also provide information about the efficiency of our implementation.

Louis Latour, "From Automata to Formulas: Convex Integer Polyhedra"
Automata-based representations have recently been investigated as a tool for representing and manipulating sets of integer vectors. In this talk, we study some structural properties of automata accepting the encodings (most significant digit first) of the solutions of systems of linear Diophantine inequations, i.e., convex polyhedra in $\Z^n$. Based on those structural properties, we develop an algorithm that takes as input an automaton and generates a quantifier-free formula that represents exactly the set of integer vectors accepted by the automaton.

Axel Legay, "Boolean Binary Decision Diagrams (ongoing work)"
Verification of computer systems is now widely done with the help of symbolic representations which allow the manipulation of impressively large (or even infinite) sets of configurations. Amount all symbolic representations, the BDD representation is certainly the most used when considering systems whose set of configurations can be encoded using a finite memory (for example, bounded integers). One of the main advantages of the BDD representation is that it allows to implement efficiently all operations and tests needed by the state-space exploration process.

Hadrien Mélot, "Discovering optimal inequalities among graph invariants with the help of a computer"
During the last two decades, several attempts to develop computer systems have been made in order to obtain new conjectures in graph theory. These systems can be divided in two classes : automated systems if they provide conjectures without human intervention - except for the problem statement ? and computer-assisted systems otherwise.
We present a new computer-assisted system (GraPHedron) which uses a polyhedral approach to discover optimal linear inequalities under certain constraints defined by a given class of graphs and a selected set of graph invariants. Of course, the meaning of "optimal inequality" will be precised and we will show how the system can be used to identify such relations.


Archive des séminaires passés

Retour à la page de garde / Back to the homepage Page maintenue par Cédric Rivière