Abstract
Problems related to the construction of consensus out of distributed knowledge have become actual again under a new perspective with the diffusion of distributed ledger techniques. In particular, when dealing with contracts, different observers must agree that a contract is in a certain state, even if not all transactions performed under the contract are observable by all of them. In this paper, we revisit previous work on algebraic modelling of labelled non-deterministic concurrent processes, which identified an intuitionistic modal/temporal logic associated with a categorical model. We expand this logic with typical epistemic operators in a categorical framework in order to encompass distributed knowledge to speak about transactions and contracts.
Dedication : With this paper, we all wish to thank Rocco for the stimulating discussions, the original ideas and the collaborations carried out in the last twenty-five years. Furthermore, apart from being a colleague and a guide, he has always primarily been a friend for all of us, and his friendship is the main gift we received from him.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Remember that, by definition, enbl\((hon)=\)enbl\((brc)=\emptyset \) for \(hon\in \)Hon\(,brc\in \)Brc.
- 2.
Given a pullback square \(gq=fp\) in \(L_B\) and \(x\in {Sub(J)}\), the canonical morphisms \(g^*\forall _f(x)\rightarrow \forall _q{p}^*(x)\) and \(\exists _q{p}^*(x)\rightarrow {g}^*\exists _f(x)\) are iso.
References
Azzopardi, S., Pace, G.J., Schapachnik, F.: On observing contracts: deontic contracts meet smart contracts. In: Palmirani, M. (ed.) Legal Knowledge and Information Systems - JURIX 2018, vol. 313, pp. 21–30. IOS Press (2018)
Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. 225, 29–82 (2013)
Bernardo, M., De Nicola, R., Loreti, M.: Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes. Acta Informatica 52(1), 61–106 (2015)
Bottoni, P., Gorla, D., Kasangian, S., Labella, A.: A doctrinal approach to modal/temporal heyting logic and non-determinism in processes. Math. Struct. Comput. Sci. 28(4), 508–532 (2018)
Bottoni, P., Labella, A., Kasangian, S.: Spatial and temporal aspects in visual interaction. J. Vis. Lang. Comput. 23(2), 91–102 (2012)
Brünnler, K., Flumini, D., Studer, T.: A logic of blockchain updates. In: Artemov, S., Nerode, A. (eds.) LFCS 2018. LNCS, vol. 10703, pp. 107–119. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-72056-2_7
De Nicola, R., Di Stefano, L., Inverso, O.: Toward formal models and languages for verifiable multi-robot systems. In: Front. Robotics and AI 2018 (2018)
De Nicola, R., Gorla, D., Labella, A.: Tree-functors, determinacy and bisimulations. Math. Struct. Comput. Sci. 20, 319–358 (2010)
De Nicola, R., Labella, A.: Tree morphisms and bisimulations. Electr. Notes Theor. Comput. Sci. 18, 46–64 (1998)
De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Logic 5(1), 79–128 (2004)
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Presss, Cambridge (1995)
Hendricks, V., Symons, J.: Epistemic logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, fall 2015 edn. (2015)
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides, vol. 1. Clarendon Press, Oxford (2002). autre tirage: 2008
Kasangian, S., Labella, A.: Observational trees as models for concurrency. Math. Struct. Comput. Sci. 9(6), 687–718 (1999)
Lawvere, B.: Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In: Heller, A. (ed.) Applications of Categorical Algebra, Proceedings of Symposium in Pure Mathematics of the American Mathematical Society, No. 17, pp. 1–14 (1970)
Magazzeni, D., McBurney, P., Nash, W.: Validation and verification of smart contracts: a research agenda. Computer 50(9), 50–57 (2017)
Plaza, J.: Logics of public communications. Synthese 158(2), 165–179 (2007)
Roelofsen, F.: Distributed knowledge. J. Appl. Non-Class. Logics 17(2), 255–273 (2007)
Uriarte, R.B., De Nicola, R.: Blockchain-based decentralized cloud/fog solutions: challenges, opportunities, and standards. IEEE Commun. Stand. Mag. 2(3), 22–28 (2018)
Acknowledgements
Work partially supported by Sapienza, project “Consistency problems in distributed and concurrent systems”. We thank the anonymous referees for indication on how to improve this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Bottoni, P., Gorla, D., Kasangian, S., Labella, A. (2019). Modal Epistemic Logic on Contracts: A Doctrinal Approach. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds) Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science(), vol 11665. Springer, Cham. https://doi.org/10.1007/978-3-030-21485-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-21485-2_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-21484-5
Online ISBN: 978-3-030-21485-2
eBook Packages: Computer ScienceComputer Science (R0)