advertisement

advertisement

Information about An Algebra of Hierarchical Graphs @ IMT Job Market Seminar 2009

We dene an algebraic theory of hierarchical graphs, whose equational part characterises graph isomorphism, i.e. it is formed by a sound and complete set of axioms equating two terms whenever they represent the same hierarchical graph. Our algebra can thus be understood as a high-level language for describing graphs with a nested structure,

and is then particularly suited for the visual specication of process calculi with inherently hierarchical features such as sessions, transactions or locations. We illustrate our approach by encoding CaSPiS, a recently

proposed session-centered calculus.

and is then particularly suited for the visual specication of process calculi with inherently hierarchical features such as sessions, transactions or locations. We illustrate our approach by encoding CaSPiS, a recently

proposed session-centered calculus.

advertisement

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

The structure of data, programs and all that We observe 1) composition, 2) containment and 3) references.

The structure of data, programs and all that We observe 1) composition, 2) containment and 3) references. Programs (e.g. Pascal) 1. control ﬂow 2. scopes 3. variables

The structure of data, programs and all that We observe 1) composition, 2) containment and 3) references. Programs (e.g. Pascal) 1. control ﬂow 2. scopes 3. variables Data (e.g. XML) 1. element list 2. tag hierarchy 3. references

The structure of data, programs and all that We observe 1) composition, 2) containment and 3) references. Programs (e.g. Pascal) 1. control ﬂow 2. scopes 3. variables Data (e.g. XML) 1. element list 2. tag hierarchy 3. references Other examples: ﬁle system navigation workﬂows (BPEL) diagrams (UML) etc.

The structure of modern data, programs and all that Modern systems increase the relevance of containment and the interplay with composition and references becomes more subtle.

The structure of modern data, programs and all that Modern systems increase the relevance of containment and the interplay with composition and references becomes more subtle. E.g. Nested... Transactions

The structure of modern data, programs and all that Modern systems increase the relevance of containment and the interplay with composition and references becomes more subtle. E.g. Nested... Transactions Locations

The structure of modern data, programs and all that Modern systems increase the relevance of containment and the interplay with composition and references becomes more subtle. E.g. Nested... Transactions Locations Sessions

The structure of modern data, programs and all that Modern systems increase the relevance of containment and the interplay with composition and references becomes more subtle. E.g. Nested... Transactions Locations Sessions Membranes Etc.

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Networking scenario Let us consider a simple networking scenario with some structure: topology (e.g. line, bus, ring, etc.) nesting (e.g. home sub-network, etc.) references (e.g. ﬁle sharing, services, etc.)

Networking scenario: visual approach bus

Networking scenario: visual approach line bus

Networking scenario: visual approach line bus ring

Networking scenario: visual approach line bus subnet ring

Networking scenario: visual approach line bus subnet ring

Networking scenario: visual approach line + refs bus + refs subnet + refs ring + refs

Networking scenario: textual approach host | host | host | host | host

Networking scenario: textual approach host ; host ; host host | host | host | host | host

Networking scenario: textual approach host ; host ; host host | host | host | host | host < host ; host ; host ; host ; host >

Networking scenario: textual approach host ; host ; host host | host | host | host | host [ host ; host ] < host ; host ; host ; host ; host >

Networking scenario: textual approach < host ; host(a) ; host ; host(a) ; host >

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Two trends to formal textual and visual speciﬁcations Algebraic Graph-based Terms elements Graphs (diagrams) host(a) | host(b) ﬂat, hierarchical, etc.

Two trends to formal textual and visual speciﬁcations Algebraic Graph-based Terms elements Graphs (diagrams) host(a) | host(b) ﬂat, hierarchical, etc. Operations vocabulary Graph compositions ·|· : Bus × Bus → Bus Union, tensor, etc.

Two trends to formal textual and visual speciﬁcations Algebraic Graph-based Terms elements Graphs (diagrams) host(a) | host(b) ﬂat, hierarchical, etc. Operations vocabulary Graph compositions ·|· : Bus × Bus → Bus Union, tensor, etc. Axioms equivalence Homomorphisms x|y≡y|x isomorphism, etc.

Two trends to formal textual and visual speciﬁcations Algebraic Graph-based Terms elements Graphs (diagrams) host(a) | host(b) ﬂat, hierarchical, etc. Operations vocabulary Graph compositions ·|· : Bus × Bus → Bus Union, tensor, etc. Axioms equivalence Homomorphisms x|y≡y|x isomorphism, etc. Rewrite rules dynamics Transformation rules host(x) −→ host

Goal statement The spirit of our research is ”to conciliate algebraic and graph-based speciﬁcations”

Goal statement The spirit of our research is ”to conciliate algebraic and graph-based speciﬁcations” The work presented in this talk has the goal to ”Equip algebraic speciﬁcations with a graphical representation that is Intuitive Easy to deﬁne Easy to prove correct

Main technical goal: mapping coherent wrt. equivalence graph1 network1 host(a) | host | [ host | host(a)]

Main technical goal: mapping coherent wrt. equivalence graph1 network1 host(a) | host | [ host | host(a)]

Main technical goal: mapping coherent wrt. equivalence graph1 network1 host(a) | host | [ host | host(a)] congruent network2 host | [ host | host(a)] | host(a)

Main technical goal: mapping coherent wrt. equivalence graph1 network1 host(a) | host | [ host | host(a)] congruent graph2 network2 host | [ host | host(a)] | host(a)

Main technical goal: mapping coherent wrt. equivalence graph1 network1 host(a) | host | [ host | host(a)] congruent isomorphic graph2 network2 host | [ host | host(a)] | host(a)

Main technical problem: representation distance grammar, structural congruence, etc. very diﬀerent syntax! adjacency matrix, tuples, sets, morphisms

Main technical problem: representation distance similar syntax solution: graph algebras similar syntax

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

The syntax of the graph algebra G, H ::= 0 the empty graph

The syntax of the graph algebra G, H ::= 0 | x a node called x

The syntax of the graph algebra G, H ::= 0 | x | t(x) an edge labelled with t attached to x

The syntax of the graph algebra G, H ::= 0 | x | t(x) | G || H parallel composition: disjoint union up to common nodes

The syntax of the graph algebra G, H ::= 0 | x | t(x) | G || H | (νx)G declaration of a new node x

The syntax of the graph algebra D ::= Tx [G] G, H ::= 0 | x | t(x) | G || H | (νx)G graph G with interface of type T exposing x

The syntax of the graph algebra D ::= Tx [G] G, H ::= 0 | x | t(x) | G || H | (νx)G | D(y ) a nested graph attached to y

The syntax of the graph algebra D ::= Tx [G] G, H ::= 0 | x | t(x) | G || H | (νx)G | D(y ) a nested graph attached to y

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Hierarchical graph isomorphism

Hierarchical graph isomorphism

Structural axioms characterise graph isomorphism G || H ≡ H || G (PARALLEL1) G || (H || I) ≡ (G || H) || I (PARALLEL2) is equivalent to

Structural axioms characterise graph isomorphism G || H ≡ H || G (PARALLEL1) G || (H || I) ≡ (G || H) || I (PARALLEL2) G || 0 ≡ G (NODES1) (νx)(νy )G ≡ (νy )(νx)G (NODES2) (νx)0 ≡ 0 (NODES5) (νx)G ≡ (νy )G{y /x } if y ∈ fn(G) (NODES3) Lx [G] ≡ Ly [G{y /x }] if |y | ∩ fn(G) = ∅ (NODES4) G || (νx)H ≡ (νx)(G || H) if x ∈ fn(G) (NODES5) Lx [(νy )G](z) ≡ (νy )Lx [G](z) if y ∈ |x| ∪ |z| (NODES6) x || G ≡ G if x ∈ fn(G) (NODES7) These axioms are rather standard and thus intuitive to those familiar with algebraic speciﬁcations.

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Typical structures are derived operators (network) nesting [X ] def SubBus p [X (p)], with X : Bus =

Typical structures are derived operators (network) parallel composition X | Y def Busp [X (p)|| Y (p)] = Axiom Busx [G](y ) ≡ G{y /x } gets rid of associativity and commutativity.

Typical structures are derived operators (network) sequential composition X ; Y def Linein,out [(νmid) X (in, mid) || Y (mid, out)] =

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

The model of hierarchical graphs intuitive visual representation complex textual representation we are hiding

The model of hierarchical graphs intuitive visual representation complex textual representation we are hiding Linein,out [(ν mid) host(in, mid) ; SubLinein,out [(ν mid) host(in, mid) ; host(mid, out) ; ] (mid,out) ]

From graph terms to graphs

From graph terms to graphs Formal deﬁnition x = x, ∅, ⊥ , ⊥, ∅, {x}, ∅ l(x) = |x|, e, e → x , ⊥, ∅, |x|, ∅ (νx)G = GG , IG , XG , FG x, ∅ 0 = ∅, ⊥, ⊥, ∅, ∅ G || H = GG ⊕ HH , IG ⊕ IH , XG ⊕ XH , FG ∪ FH , ∅ Lx [G] = FG , e , e → x , e → GG , IG , XG , e → idFG , FG x, x D(x) = GD {VD /x }, ID , XD {VD /x }, FD ∪ |x|, ∅ if D : L ∧ ﬂatL ∈≡d D(x) = ID (e){x /FID (e) }, IID (e) , XID (e) , FID (e) ∪ |x|, ∅ if D : L ∧ ﬂatL ∈≡d

From graph terms to graphs the algebra is oﬀering... eq X | Y = Bus[p . p | X{p} | Y{p}] 1 self-contained line of code vs 13 lines full of auxiliary functions!

Main result: coherence for the graph algebra graphterm1 graph1 Bus[ p . host(p,a) | host(p) ... ] congruent isomorphic graph2 graphterm2 Bus[ p . host(p) ... | host(p,a) ]

Outline Introduction On structural issues A simple scenario Goal statement An algebra of hierarchical graphs A syntax for hierarchical graphs Identifying equivalent graphs Expressing typical structures Hiding the complexity of hierarchical graphs Conclusion

Main application of the result: encodings are facilitated graph1 network1 host(a) | host | [ host | host(a)] congruent isomorphic graph2 network2 host | [ host | host(a)] | host(a)

Main application of the result: encodings are facilitated graphterm1 graph1 Bus[ p . network1 host(p,a) | host(p) host(a) ... | host | [ host | host(a)] ] congruent congruent isomorphic graph2 network2 graphterm2 host Bus[ p . | [ host | host(a)] host(p) | host(a) ... | host(p,a) ]

The algebra facilitates a modular implementation Speciﬁcation Graph languages formats networks dot algebra graphs pi-calculus GraphML caspis External etc. Tools

The algebra facilitates a modular implementation Speciﬁcation Graph languages formats networks dot algebra graphs pi-calculus GraphML caspis analysis External etc. Tools

Implementation snapshot (a simple visualiser) Available at www.albertolluch.com/adr2graphs

Applications (general) Modelled with the algebra Network topologies [BL09]

Applications (general) Modelled with the algebra Network topologies [BL09] Process calculi [GLB]

Applications (general) Modelled with the algebra Network topologies [BL09] Process calculi [GLB] Workﬂows [GLB]

Applications (general) Modelled with the algebra Network topologies [BL09] Process calculi [GLB] Workﬂows [GLB] Modelled without the algebra Service modelling language [BLME07]

Applications (general) Modelled with the algebra Network topologies [BL09] Process calculi [GLB] Workﬂows [GLB] Modelled without the algebra Service modelling language [BLME07] UML4SOA proﬁle [BLME07]

Applications (general) Modelled with the algebra Network topologies [BL09] Process calculi [GLB] Workﬂows [GLB] Modelled without the algebra Service modelling language [BLME07] UML4SOA proﬁle [BLME07] Architectural styles [BLM08]

Applications (service oriented calculi) CaSpiS (sessions) Nesting of sessions Sharing of session channels Activity A has invoked two services S1, S2 creating two nested sessions with channels a, b.

Applications (service oriented calculi) CaSpiS (sessions) Nesting of sessions Sharing of session channels Sagas (transactions) A saga as an ordinary workﬂow Nesting of transactions compensated with another workﬂow. Workﬂow constructs A workﬂow as saga without compensation ﬂow.

Related work GS-Graphs [CG99] syntactical structure, algebraic presentation ﬂat (hierarchy-as-tree)

Related work GS-Graphs [CG99] syntactical structure, algebraic presentation ﬂat (hierarchy-as-tree) Ranked Graphs [Gad03] node sharing, calculi encoding no composition interface, ﬂat

Related work GS-Graphs [CG99] syntactical structure, algebraic presentation ﬂat (hierarchy-as-tree) Ranked Graphs [Gad03] node sharing, calculi encoding no composition interface, ﬂat Hierarchical Graphs [DHP02] basic model, composition interface no node sharing, no algebraic syntax

Related Work Bigraphs [JM03] nesting + linking 2 overlapping structures, complex syntax, no composition interface, ﬂat

Related Work Bigraphs [JM03] nesting + linking 2 overlapping structures, complex syntax, no composition interface, ﬂat Graph Algebra, SHR [CMR94] basic algebra ﬂat, no composition interface

Concluding remarks The graph algebra . . . Grounds on widely-accepted models; Hides the complexity of hierarchical graphs; Enables proofs by structural induction; Extends ADR with node sharing and serves as primitive algebra for ADR; Simpliﬁes the modelling of process calculi; Oﬀers a technique for complementing textual and visual notations in formal tools; Has been evaluated on calculi, networks, etc. Natural implementation in Maude (support for theorem proving, model checking, simulation, etc.)

Thanks for your attention

Credits and references I Roberto Bruni and Alberto Lluch Lafuente. Ten virtues of structured graphs. In Invited paper at the 8th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’09), Electronic Communications of the EASST, 2009. To appear. Roberto Bruni, Alberto Lluch Lafuente, and Ugo Montanari. Hierarchical Design Rewriting with Maude. In Proceedings of the 7th International Workshop on Rewriting Logic and its Applications (WRLA’08), Electronic Notes in Theoretical Computer Science. Elsevier, 2008. To appear. Roberto Bruni, Alberto Lluch Lafuente, Ugo Montanari, and Emilio Tuosto. Service Oriented Architectural Design. In Proceedings of the 3rd International Symposium on Trustworthy Global Computing (TGC’07), volume 4912 of Lecture Notes in Computer Science, pages 186–203. Springer, 2007. Andrea Corradini and Fabio Gadducci. An algebraic presentation of term graphs, via gs-monoidal categories. applied categorical structures. Applied Categorical Structures, 7:7–299, 1999. Andrea Corradini, Ugo Montanari, and Francesca Rossi. An abstract machine for concurrent modular systems: CHARM. Theoretical Compututer Science, 122(1&2):165–200, 1994. Frank Drewes, Berthold Hoﬀmann, and Detlef Plump. Hierarchical graph transformation. Journal on Computer and System Sciences, 64(2):249–283, 2002.

Credits and references II Fabio Gadducci. Term graph rewriting for the pi-calculus. In Atsushi Ohori, editor, Proceedings of the 1st Asian Symposium on Programming Languages and Systems, volume 2895 of Lecture Notes in Computer Science, pages 37–54. Springer, 2003. Fabio Gaducci, Alberto Lluch Lafuente, and Roberto Bruni. Graphical representation of process calculi via an algebra of hierarchical graphs. Manuscript available at http://www.albertolluch.com/papers/adr.algebra.pdf. O. H. Jensen and R. Milner. Bigraphs and mobile processes. Technical Report 570, Computer Laboratory, University of Cambridge, 2003. Note: Some ﬁgures have been borrowed from the Internet and the referred papers.

An algebra of hierarchical graphs ... Job Market Seminars IMT Lucca, May 25 2009. Outline ... The graph algebra ...

Read more

Architectural Design Rewriting ... An algebra of hierarchical graphs and its application to structural ... , IMT Job Market Seminar, June 2009 ...

Read more

Type of Job Organization ... Algebra, Differential ... Node entropy optimization of novel graph class Universal hierarchical graph using entropy ...

Read more

Research Seminars. IMT organizes and promotes Research Seminars ... Using graph coloring as a ... Job Market Seminars ...

Read more

Il sito di IMT Alti Studi Lucca utilizza cookie di Sessione e di Profilazione per ... Research Seminars ; Job Market Seminars ... process algebra, ...

Read more

IMT Journal; Conferences; ... Determinants of supermarket shopping behaviour in an emerging market. Journal of ... & Muncherjee, N. (2009). Fatigue and Job ...

Read more

Hierarchical Graph Laplacian Eigen ... Student-Run Applied & Math Seminar: Andrew Port: Wed, Mar 4 2009, ... Stability of equilibria in incomplete markets:

Read more

Properties of Hierarchical Archimedean Copulas ... Über das Geschlecht von Graphen, ... 31.08.2009 (Bachelorabschlussmodul Algebra) ...

Read more

Seminar and Colloquia: 2009 ... Capital, Capital Markets, ... kswappable graphs, and diophantine approximation. Time: ...

Read more

## Add a comment