*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Theory of labeled, directed graphs in Isabelle*From*: Simon Meier <meier-simon at student.ethz.ch>*Date*: Tue, 17 Apr 2007 12:28:50 +0200*In-reply-to*: <46248259.6000806@in.tum.de>*References*: <46247852.40208@student.ethz.ch> <46248259.6000806@in.tum.de>*User-agent*: Thunderbird 1.5.0.10 (X11/20070324)

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

**References**:**[isabelle] Theory of labeled, directed graphs in Isabelle***From:*Simon Meier

**Re: [isabelle] Theory of labeled, directed graphs in Isabelle***From:*Alexander Krauss

- Previous by Date: [isabelle] Grants for RISC/SCIEnce Training School: Deadline Extension
- Next by Date: [isabelle] CFV'07 Call for Papers
- Previous by Thread: Re: [isabelle] Theory of labeled, directed graphs in Isabelle
- Next by Thread: [isabelle] Grants for RISC/SCIEnce Training School: Deadline Extension
- Cl-isabelle-users April 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list