Document Open Access Logo

Weighted Relational Models for Mobility

Author James Laird

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.24.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

James Laird

Cite AsGet BibTex

James Laird. Weighted Relational Models for Mobility. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.24

Abstract

We investigate operational and denotational semantics for computational and concurrent systems with mobile names which capture their computational properties. For example, various properties of fixed networks, such as shortest or longest path, transition probabilities, and secure data flows, correspond to the ``sum'' in a semiring of the weights of paths through the network: we aim to model networks with a dynamic topology in a similar way. Alongside rich computational formalisms such as the lambda-calculus, these can be represented as terms in a calculus of solos with weights from a complete semiring $R$, so that reduction associates a weight in R to each reduction path. Taking inspiration from differential nets, we develop a denotational semantics for this calculus in the category of sets and R-weighted relations, based on its differential and compact-closed structure, but giving a simple, syntax-independent representation of terms as matrices over R. We show that this corresponds to the sum in R of the values associated to its independent reduction paths, and that our semantics is fully abstract with respect to the observational equivalence induced by sum-of-paths evaluation.
Keywords
  • Concurrency
  • Mobility
  • Denotational Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Bahamonde. Tensor product of partially-additive monoids. Semigroup Forum, 32(1):31-53, 1985. Google Scholar
  2. Emmanuel Beffara. Quantitative testing semantics for non-interleaving. CoRR, abs/0906.3994, 2009. Google Scholar
  3. G. Bellin and P. J. Scott. On the pi-calculus and linear logic. Theoretical Computer Science, 135(1):11-65, 1994. Google Scholar
  4. R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. Differential categories. Mathematical. Structures in Comp. Sci., 16, 2006. Google Scholar
  5. M. Boreale and F. Gaducci. Processes as formal power series: A coinductive approach to denotational semantics. Theoretical Computer Science, 360(1-3):440-458, 2006. Google Scholar
  6. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22:465-476, 1979. Google Scholar
  7. T. Ehrhard and O. Laurent. Acyclic solos and differential interaction nets. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  8. T. Ehrhard and O. Laurent. Interpreting a finitary pi-calculus in differential nets. Information and Computation, 208(6):606-633, 2010. Google Scholar
  9. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309, 2003. Google Scholar
  10. T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006. Google Scholar
  11. C. Fornet and G. Gonthier. The reflexive chemical abstract machine and the join-calculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL'96), 1996. Google Scholar
  12. J. S. Golan. The theory of semirings with applications in mathematics and theoretical computer science. Addison-Wesley, 1992. Google Scholar
  13. R. Guitart. Tenseurs et machines. Cahiers de Topologie et Geometrie Differentielle, XXI(1):5-62, 1980. Google Scholar
  14. K. Honda and N. Yoshida. On reduction-based process semantics. Theoretical Computer Science, 152:437-686, 1995. Google Scholar
  15. A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Math. Proc. Camb. Phil. Soc., 119:447-468, 1996. Google Scholar
  16. J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of LICS'13, 2013. Google Scholar
  17. C. Laneve and B. Victor. Solos in concert. Mathematical Structures in Computer Science, 13(5), 2003. Google Scholar
  18. P. Melliès, N. Tabareau, and C. Tasson. An explicit formula for the free exponential modality of linear logic. In Proc. ICALP'09, number 5556 in LNCS, pages 247-260, 2009. Google Scholar
  19. R. Milner. Functions as processes. Math. Struct. in Computer Science, 2(2):119-141, 1992. Google Scholar
  20. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part i. I AND II. INFORMATION AND COMPUTATION, 100, 1989. Google Scholar
  21. M. Mohri. Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics, 7(3):321-350, 2002. Google Scholar
  22. C. Laneve. J. Parrow and B. Victor. Solo diagrams. In Proceedings of TACS 2001, LNCS. Springer, 2001. Google Scholar
  23. J. Parrow and B. Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. In Proceedings of LICS'98, pages 176-185. IEEE press, 1998. Google Scholar
  24. D. Sangiorgi and D. Walker. The Pi-Calculus: A theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  25. L. Wischik and P. Gardner. Explicit fusions. Theoretical Computer Science, 340(3):606-630, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact