Re: [isabelle] Theory of labeled, directed graphs in Isabelle



Hi Alex,

thank you very much for your fast answer. I've checked the theory file
you pointed me to and I guess it could serve as a good base.

>> I'm looking for a graph theory in Isabelle that supports directed graphs
>> with labeled edges. Has anybody already done such a development or knows
>> some good pointers on how to model these?
> 
> I recently formalized such graphs for some work I did on termination.
> You can find it in recent development snapshots
> (HOL/Library/Graphs.thy). But since I created this for a particular task
> (representing size-change graphs in termination proofs) it is probably
> not very well developed, and I don't know if it fits your needs.
> 
> My graphs are basically just relations with a new constructor wrapped
> around them:
> 
> datatype ('n, 'e) graph = Graph "('n * 'e * 'n) set"
> 
> This means that the set of nodes is assumed to be the whole type, which
> is not what everybody wants, I suppose... Also, since they can be
> infinite and so on, they are rather abstract (as opposed to concrete
> data structures for efficient computation).
> 
> Operations on graphs are a certain composition, addition (which is just
> union) and transitive closure. There is also a notion of (finite and
> infinite) path.
> 
> What is the application you have in mind?

I'm formalizing the model-checking algorithm for security protocols used
by Scyther (http://people.inf.ethz.ch/cremersc/scyther/index.html)

Its essential component is an abstraction of the concrete traces given
by the operational semantics. A class of traces is represented by an
acyclic graph with the possible events as vertices and the edges
defining for which events the execution order matters. The edge labels
are used by the algorithm to characterize the development of the
intruder knowledge.

Thus, what I need from the graph theory are directed, acyclic, labeled
graphs with a restricted node set, edge and vertice changes, transitive
closure and finite paths. How difficult would it be to adapt your theory
to this needs? Is it a viable way at all?

Thank you again for your help,
Simon






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.