Hostname: page-component-848d4c4894-x5gtn Total loading time: 0 Render date: 2024-05-01T09:59:29.762Z Has data issue: false hasContentIssue false
  • English
  • Français

A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes

Published online by Cambridge University Press:  27 February 2017

PAOLO BOTTONI ,
DANIELE GORLA ,
STEFANO KASANGIAN  and
ANNA LABELLA
PAOLO BOTTONI
Affiliation:
Dipartimento di Informatica, “Sapienza” Università di Roma, Rome, Italy Email: bottoni@di.uniroma1.it, gorla@di.uniroma1.it, labella@di.uniroma1.it
DANIELE GORLA
Affiliation:
Dipartimento di Informatica, “Sapienza” Università di Roma, Rome, Italy Email: bottoni@di.uniroma1.it, gorla@di.uniroma1.it, labella@di.uniroma1.it
STEFANO KASANGIAN
Affiliation:
Dipartimento di Matematica, Università di Milano, Milan, Italy Email: stefano.kasangian@gmail.com
ANNA LABELLA
Affiliation:
Dipartimento di Informatica, “Sapienza” Università di Roma, Rome, Italy Email: bottoni@di.uniroma1.it, gorla@di.uniroma1.it, labella@di.uniroma1.it
Get access Rights & Permissions [Opens in a new window]

Abstract

The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB, obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational models.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 28 , Issue 4 , April 2018 , pp. 508 - 532
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aceto, L., Ingólfsdóttir, A., Larsen, K.G. and Srba, J. (2007). Reactive Systems: Modelling, Specification and Verification, Cambridge University Press.CrossRefGoogle Scholar
Borceux, F. (1994). Handbook of Categorical Algebra: Volume 1, Basic Category Theory, Encyclopedia of Mathematics and its Applications, Cambridge University Press. Available at http://opac.inria.fr/record=b1126837 Google Scholar
Bottoni, P., Labella, A. and Kasangian, S. (2012). Spatial and temporal aspects in visual interaction. Journal of Visual Languages and Computing 23 (2) 91–102. Special issue dedicated to Prof. Piero Mussio. Available at http://www.sciencedirect.com/science/article/pii/S1045926X11000772 CrossRefGoogle Scholar
Braüner, T. and Ghilardi, S. (2007). First-order modal logic. In: Patrick Blackburn, J.V.B. and Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, Elsevier, 549–620. http://www.sciencedirect.com/science/article/pii/S1570246407800127 CrossRefGoogle Scholar
Cardelli, L. (1982). Real time agents. In: Proceedings of the 9th Colloquium on Automata, Languages and Programming 94–106. Available at http://dl.acm.org/citation.cfm?id=646236.682864 CrossRefGoogle Scholar
De Nicola, R., Gorla, D. and Labella, A. (2010). Tree-functors, determinacy and bisimulations, Mathematical Structures in Computer Science 20 319–358. Available at http://journals.cambridge.org/article_S0960129509990272 CrossRefGoogle Scholar
Freyd, P. and Scedrov, A. (1990). Categories, Allegories, Mathematical Library, vol. 39, North-Holland.Google Scholar
Ghezzi, R. (2012). Enriched categories and presheaves: Their interconnections, generators and logics, Master's thesis, Università degli studi di Milano.Google Scholar
Ghilardi, S. and Meloni, G.C. (1988). Modal and tense predicate logic: Models in presheaves and categorical conceptualization, In: Borceux, F. (ed.) Categorical Algebra and its Applications, Springer, 130–142. Available at http://dx.doi.org/10.1007/BFb0081355 CrossRefGoogle Scholar
Hennessy, M. and Milner, R. (1985). Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32 (1) 137–161. http://doi.acm.org/10.1145/2455.2460 CrossRefGoogle Scholar
Huth, M. and Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning About Systems, Cambridge University Press.CrossRefGoogle Scholar
Johnstone, P. T. (2002). Sketches of An Elephant: A Topos Theory Compendium, vol. 1, Oxford Logic Guides, Clarendon Press. Available at http://opac.inria.fr/record=b1107183 CrossRefGoogle Scholar
Kasangian, S. and Labella, A. (1999). Observational trees as models for concurrency. Mathematical Structures in Computer Science 9 (6) 687–718. Available at http://dx.doi.org/10.1017/S0960129599002935 CrossRefGoogle Scholar
Klin, B. (2007). Coalgebraic modal logic beyond sets. Electronic Notes in Theoretical Computer Science 173 177–201.CrossRefGoogle Scholar
Lawvere, B. (1970). Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In: Heller, A. (ed.) Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics, vol. 17, American Mathematical Society, 1–14.Google Scholar
Lawvere, F. W. (1969). Adjointness in foundations. Dialectica 23 (3–4) 281–296. Available at http://dx.doi.org/10.1111/j.1746-8361.1969.tb01194.x CrossRefGoogle Scholar
Milner, R. (1989). Communication and Concurrency, Prentice-Hall.Google Scholar
Pisani, C. (2010). A logic for categories. Theory and Applications of Categories 24 394–417.Google Scholar
Pitts, A. M. (2000). Categorical logic. Handbook of Logic in Computer Science, Oxford University Press, 39–123. Available at http://dl.acm.org/citation.cfm?id=373919.373928 Google Scholar
Rosenthal, K. I. (1993). ‘A note on categories enriched in quantaloids and modal and temporal logic, Cahiers de Topologie et Géométrie Différentielle Catégoriques 34 (4) 267–277. Available at http://eudml.org/doc/91529 Google Scholar
Streicher, T. (2003). Categorical models of constructive logic. Available at http://www.mathematik.tu-darmstadt.de/~streicher/cmcl.pdf.Google Scholar
Walters, R. F. C. (1981). Sheaves and cauchy-complete categories. Cahiers de Topologie et Géométrie Différentielle Catégoriques 22 (3) 283–286. Available at http://eudml.org/doc/91273 Google Scholar