Contents

Geometric Theorem Proving
Determining Reachability in Petri Nets
Green's Relations for Semigroups
Module Presentations



[MCS Home]

Applications of Gröbner Basis Theory

this page is still in the process of being written

Geometric Theorem Proving

Theorem proving is one of the traditional applications for Gröbner basis theory. The basic idea is that (by using an affine co-orninate system) the geometric conditions shown by a diagram can all be represented as polynomial equations. So we can represent the hypotheses as h1=0, ..., hn=0. Any conclusion c=0 can be deduced from the hypotheses if and only if c is a member of the ideal <h1, ..., hn>. Thus problems such as proving Pappus' theorem can be expressed as ideal membership problems - and solved using Gröbner bases.

Determining Reachability in Petri Nets

Petri nets are graphical and mathematical means of modelling the dynamic behaviour of systems. A Petri net is a bipartite graph with two types of node - places and transitions. The state of a system is represented by a marking of the Petri net with tokens at the places. Transitions represent the events which could potentially effect the state of the system modelled. The places and transitions are connected by a flow relation, each transition having input places and output places. If the input places to a transition all hold tokens then the transition is enabled, this corresponds to the even being possible. If the event does occur, then the transition fires, tokens are removed from the input places and added to the input places. Given an initial marking of the Petri net it is a key question to find out what other markings may be reachable through some sequence of events.

Reversiblity corresponds to the ability to reset the device which is being modelled, this is actually a key feature of some models (e.g. navigation systems for mobile robots). When the net is reversible, the reachability problem can be solved using Gröbner bases.

The application of Gröbner bases is achieved by labelling the places in the net. A marking then is associated to a power product of place labels raised to the power of the number of tokens held at that place. If we now represent transitions by difference binomials i.e. minimum input - minimum output, and let <T> be the ideal they generate, then we can observe that a marking M is reachable from the initial marking if and only if the difference between their representing power products is in the ideal <T>. This means that by calculating a Gröbner basis for <T> we can decide which markings are reachable, and in some circumstances, catalogue all the reachable markings.

Green's Relations for Semigroups

Green's relations are a way of expressing the local structure of an abstract semigroup in terms of groups with certain actions on them. Eggbox diagrams are used to depict the partitions of a semigroup into L-classes, R-classes, D-classes and H-classes as defined by Green's relations. We can sometimes determine the classes by using Gröbner bases applied directly to the presentation, giving the possibility for dealing with infinite semigroups having infinitely many H-classes, L-classes or R-classes.

Module Presentations

[University Home][MCS Home][University Index A-Z][University Search][University Help]

Author: Anne Heyworth
Last updated: 14th May 2001
MCS Web Maintainer
Any opinions expressed on this page are those of the author.
© University of Leicester.