Email Gateway (Aug 18 2022 at 10:24): Email Gateway (Aug 18 2022 at 10:24):From: Simon Meier <meier-simon@student.ethz.ch>
Hi,
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?
Thank you very much for your help,
Simon Meier
Email Gateway (Aug 18 2022 at 10:24):From: Alexander Krauss <krauss@in.tum.de>
Hi Simon,
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?
Alex
Email Gateway (Aug 18 2022 at 10:25):From: Simon Meier <meier-simon@student.ethz.ch>
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 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
Last updated: Nov 21 2024 at 12:39 UTC