Comments
Description
Transcript
Networks - SYSMA@IMT Lucca
CINA: Compositionality, Interaction, Negotiation, Autonomicity, MIUR PRIN Project Final General Meeting, January 19-21, 2016, Civitanova General Description of Network Systems Ugo Montanari Dipartimento di Informatica, University of Pisa joint work with Roberto Bruni (and others) Networks Networks hypergraphs with labels, structure and observation interface labels/buffer content may change with executions structure usually changes only via explicit reconfiguration operations CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 2 Roadmap Networks • • • • Milner flowgraph algebras • Denotational process algebras • (Soft) constraint networks Networks as components & connectors • Petri nets • Signal flow graphs • Electric circuits • PROPS: product permutation categories From graphs to categories • Petri nets • Rewriting logic • Process calculi Conclusions CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 3 Roadmap Networks • • • • Milner flowgraph algebras • Denotational process algebras • (Soft) constraint networks Networks as components & connectors • Petri nets • Signal flow graphs • Electric circuits • PROPS: product permutation categories From graphs to categories • Petri nets • Rewriting logic • Process calculi Conclusions CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 4 A Variety of Networks • Communication networks & routing • Neural networks & connectivism • Computer networks • Stochastic models of the internet (Barabasi, Simon) • Social networks and concept mining, complex systems • Computation, semantics, economics of networks • Networks of connectors & buffers Ugo Montanari 5 Flow Graphs and Flow Algebras Robin Milner, Flow Graphs and Flow Algebras, JACM 1979 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 6 Flow Graphs and Flow Algebras Robin Milner, Flow Graphs and Flow Algebras, JACM 1979 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 7 CHARM, Chemical Abstract with Restriction Machine Corradini, Montanari, Rossi, An Abstract Machine for Concurrent Modular Systems: CHARM, TCS 1994 Parallel composition fuses visible nodes and hyperarcs with the same name Modelling concurrent constraint programming Modelling P/T Petri nets CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 8 Denotational Semantics George Milne, Robin Milner, Concurrent Processes and Their Syntax, JACM 1979 • Tony Hoare, Communicating Sequential Processes, CACM 1978 • Interpreting the algebra in a semantic domain CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 9 Networks of (soft) Constraints Bistarelli, Montanari, Rossi, Semiring-Based Constraint Satisfaction and Optimization, JACM 1997 Semiring definition of constraint composition c: (V→D)→S (c1 x c2)η = c1η x c2η CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 10 Courcelle Graph Algebras Graphs have an interface with a list of visible nodes called sources. There are basic graphs consisting of a single vertex or edge and three classes of operations on graphs: disjoint union where source lists are concatenated fusion of sources permutation, duplication and restriction of sources every operation is indexed by the arities of the involved sources: thus there are infinite operations The sets of graphs of bounded treewidth are exactly those that can be constructed using only a finite number of operations (but possibly unboundedly many times). Alternatively, the sets of graphs of bounded treewidth are subsets of graph languages generated by hyperedge replacement graph grammars 11 Seite CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 11 Structural Recursion on Graph Operations Inductive families of evaluations on Courcelle operations (or on graph productions) can be defined on several discrete and continuous domains. In practice, a tuple of properties must be defined on graph syntactic trees by structural recursion. It should be proved that the result of the evaluation does not depend on the particular syntactic tree of the given graph. Seite 12 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 12 Terminal Reliability An example: probability of a multiparty connection in a network all the arcs have independent probabilities of failure A subgraph connected to the rest of the graph by a set V of nodes a probability distribution assigns to each partition P of V the probability that exactly the nodes in each class of P are actually connected Inductively, given a graph production and the probability distributions for all the nonterminals in its right hand side compute the connection probability for the right hand side. Fratta, L., and Montanari, U., Terminal Reliability in a Communication Network: An Efficient Algorithm, Second International Symposium on Network Theory, Herceg-Novi, July 3-7, 1972, pp. 391-398. Seite 13 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 13 Back to (Almost) Milner Problem made of two subproblems p and q Empty subproblem Assignment for x in p has already been determined Atomic subproblem of a single constraint A + structural congruence: commutative monoidality of || , α-conversion, swapping of restrictions + nominal structure Terms up-to structural congruence are (hyper)graphs with hidden nodes: A(X) is a graph consisting of a single hyperedge and its distinct nodes Seite 14 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 14 Nominal structure Signature includes permutations bijective with axioms + distributivity over all other operators Permutations come with a notion of “untyped” free variables, independent on the specific algebra Seite 15 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 15 Secondary Optimization Problem Scope extension allows us to choose the order of variable elimination (secondary optimization problem) Apply from left to right as much as you can => assign variables as soon as you can Normal form (x)(y)(z)(v)(f1(x,y)+f2(y,z)+f3(z,v)+f4(v,x)) Canonical forms (x)(y)(f1(x,y)+(z)(f2(y,z)+(v)(f3(z,v)+f4(v,x)))) (y)(z)(f2(y,z)+(v)(f3(z,v)+(x)(f4(v,x)+f1(x,y)))) … … Seite 16 CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 16 Roadmap Networks • • • • Milner flowgraph algebras • Denotational process algebras • (Soft) constraint networks Networks as components & connectors • Petri nets • Signal flow graphs • Electric circuits • PROPS: product permutation categories From graphs to categories • Petri nets • Rewriting logic • Process calculi Conclusions CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 17 Components, Data, and Connectors Two decades ago: Sw systems seen as a collection of cooperating reusable components emerged as a trend Sw architectures are centered around three main kinds of elements: processing elements (components), data elements, and connecting elements (connectors) Ugo Montanari 18 Some Connectors from Literature Ugo Montanari 19 Some Connectors from Literature Reo by Arbab at al. channels and bounded buffers Ugo Montanari 20 Some Connectors from Literature BIP by Sifakis at al. Ugo Montanari 21 Some Connectors from Literature Span(Graph) by Katis, Sabadini and Walters Ugo Montanari 22 Some Connectors from Literature One-place buffers Ugo Montanari 23 Abstract Semantics Connectors can be seen as black boxes input interface output interface admissible signals on interfaces 1 2 3 4 1 2 1 2 1 2 3 3 3 4 Abstract semantics is just a matrix n inputs 2n rows m outputs 2m columns … 111 … sequential composition is matrix multiplication 0010 parallel composition is matrix expansion 0101 … Ugo Montanari 001 … An Example: Symmetries connectors boxes are immaterial 00 00 01 11 01 10 10 11 Ugo Montanari = Tiles Combine horizontal and vertical structures through interfaces initial configuration trigger effect final configuration Ugo Montanari Tiles Compose tiles horizontally Ugo Montanari Tiles Compose tiles horizontally (also vertically and in parallel) Ugo Montanari Sobocinski’s Nets with Boundaries Over-simplified graphical notation: transitions are not drawn Boundaries = attach points + for pending arcs Composition = can fuse and multiply transitions Ugo Montanari 29 PROPS: PRoduct Permutation categories The basic structure: symmetric monoidal categories • sequential and parallel composition • permutation of wires • axiomatization = string diagram isomorphism • additional connectors with axioms • Petri nets: 4 binary connectors: AND, OR, coAnd, coOR and buffers • most general combination of synchronization and nondeterminism • coalgebraic theory for F(X) = P(A x X) • bialgebraic theory: operations preserve bisimilarity • standard representatives of equivalence classes for finite Petri nets • Signal flow graphs => • Electric circuits => CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 30 Signal Flow Graphs Foundations of control theory S. J. Mason. Feedback Theory: I. Some Properties of Signal Flow Graphs. Massachusetts Institute of Technology, Research Laboratory of Electronics, 1953. Coalgebraic theory for F(X) = A x X J. J. M. M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs, TCSSci., 2005. PROP treatment Bonchi, Sobocinski, Zanasi, A Categorical Semantics of Signal Flow Graphs, CONCUR 2014 a sound and complete graphical theory of vector subspaces over the field of polynomial fractions, with relational composition buffers are derivatives in the operational calculus (e.g. via Laplace transforms) deterministic functional vs deadlock-prone relational CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 31 Electric Circuits John C. Baez, Brendan Fong, A Compositional Framework for Passive Linear Networks, arXiv.org resistor, reactors and capacitors buffers represent derivatives of the operational calculus nodes of the network with two values a potential (voltage of the node) and a current (current entering/exiting the node) again coalgebraic theory for F(X) = A x X the temporal series of the final coalgebra represent the temporal behavior of the circuit similar to the functional definition vs. temporal behavior of Fibonacci. CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 32 Roadmap Networks • • • • Milner flowgraph algebras • Denotational process algebras • (Soft) constraint networks Networks as components & connectors • Petri nets • Signal flow graphs • Electric circuits • PROPS: product permutation categories From graphs to categories • Petri nets • Rewriting logic • Process calculi Conclusions CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 33 Algebraic • “Petri nets are monoids” by Meseguer, Montanari – Algebra of (concurrent) computations via the lifting of the monoidal structure of markings to steps and computations • • • • • sequential composition “;” (of computations) plus identities (idle steps) plus parallel composition (of markings, steps and computations) plus functoriality of (concurrency!) leads to a (strictly) symmetric monoidal category of computations • Collective Token Philosophy (CTPh) – T(_) (commutative processes) • Individual Token Philosophy (ITPh) – P(_) (concatenable processes) CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 34 Collective vs. Token View Best-Devillers vs. Goltz-Reisig processes CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 35 The ITPh Story, I Petri* P(N) <u_> SMonCat* U(_) PTNets (_) DecOcc (_)+ Sassone’s chain of adjunctions D(_) Safe U(_) PreOrd F(_) Occ E(_) PES N(_) CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari Winskel’s chain of coreflections L(_) Dom Pr(_) 36 Pre-Nets • Under the CTPh, the construction T(_) is completely satisfactory – T(_) is left adjoint to the forgetful functor from CMonCat to Petri – T(_) can be conveniently expressed at the level of (suitable) theories (e.g. in PMEqtl) • But the CTPh does not model concurrency • We argue that, under the ITPh, all the difficulties are due to the multiset (marking) view of states • Pre-nets (Roberto Bruni et al.) are the natural implementation of P/T nets under the ITPh – pre-sets and post-sets are strings, not multisets! – for each transition t: u v, just one implementation CINA, Civitanova Marche, 19-21 37 tp,q : p q is considered January 2016 - Ugo Montanari Pre-Nets, Algebraically PreNets Z(_) SMonCat G(_) • Under the ITPh, the construction Z(_) is completely satisfactory – Z(_) is left adjoint to the forgetful functor from SMonCat to PreNets – Z(_) can be conveniently expressed at the level of (suitable) theories (e.g. in PMEqtl) – All the pre-nets implementations R of the same P/T net N have isomorphic Z(R) – P(N) can be recovered from (any) Z(R) CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 38 The Pre-Net Picture • Functorial diagram reconciling all views • Algebraic semantics via adjunction • A missing link in the unfolding <p_> SMonCat Z(_) G(_) PreNets U(_) PreOcc E(_) ? PES PreOrd (_) L(_) Dom Pr(_) A(_) CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari PTNets 39 Operational Concurrency Quite similar developments: • Term rewriting (2-categories), Jose Meseguer • Logic programming (double categories), Andrea Corradini • Graphs (DPO / SPO) Paolo Baldan • Process Calculi (Tiles, monoidal double categories), Fabio Gadducci, Roberto Bruni CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 40 Roadmap Networks • • • • Milner flowgraph algebras • Denotational process algebras • (Soft) constraint networks Networks as components & connectors • Petri nets • Signal flow graphs • Electric circuits • PROPS: product permutation categories From graphs to categories • Petri nets • Rewriting logic • Process calculi Conclusions CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 41 Conclusion Additional kinds of networks Computational fields Synchronized hyperedge replacement Neural networks Bayesian networks Additional interpreted domains Cyberphysical systems Hardware and software architectures Heterogeneous systems CINA, Civitanova Marche, 19-21 January 2016 - Ugo Montanari 42