2021/05/27 by Jade Master, Master, Jade
Computer Science · #(Primary) 18M35 (Secondary) 18D20 #18B10 #18C10 #18D40 #18N10 #Category Theory (math.CT) #Distributed systems and fault tolerance #FOS: Mathematics #Formal Methods in Verification #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.2105.12905
openalex publication_date 2021/05/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This thesis aims to develop a compositional theory for the operational semantics of networks. The networks considered are described by either internal or enriched graphs. In the internal case we focus on Q-nets, a generalization of Petri nets based on a Lawvere theory Q. Q-nets include many known variants of Petri nets including pre-nets, integer nets, elementary net systems, and bounded nets. In the enriched case we focus on graphs enriched in a quantale R regarded as matrices with entries in R. These R-matrices represent distance networks, Markov processes, capacity networks, non-deterministic finite automata, simple graphs, and more. The operational semantics of Q-nets is constructed as an adjunction between Q-nets and categories internal to the category of models of Q. Similarly, the operational semantics of R-matrices is constructed as an adjunction between R-matrices and categories enriched in R. The left adjoint of this adjunction sends an R-matrix M to the R-category FR(M) whose hom-objects are solutions of the algebraic path problem: a generalization of the shortest path problem to graphs weighted in R. For both Q-nets and R-matrices we use the theory of structured cospans to study the compositionality of the above operational semantics. For each type of network we construct a double category whose morphisms are "open networks", i.e. networks with certain vertices designated as input or output. We introduce the black-boxing of an open network, a profunctor describing the externally observable behavior of an open network. We introduce a class of open networks called "functional open networks" for which black-boxing preserves composition.