...

Networks - SYSMA@IMT Lucca

by user

on
Category:

software

62

views

Report

Comments

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
Fly UP