The development of a concurrent system poses unique challenges, especially those related to correctness and consistency, as such a system usually involves several interactive processes executing simultaneously. To deal with some of these challenges, we resorted to Labeled Event Structures (LES) and category theory as the formal methods to model concurrent systems. Specifically, in this paper, we proposed an idea to define categories and corresponding constructs, such as product and sum, to model events and relationships among events represented by LES. To explain the idea, several examples are developed. Though a mathematical proof, the proposed idea helped to build a correct-by-construction approach for formalizing LES models of concurrent systems.
References
[1]
Winskel, G. (1989) An Introduction to Event Structures. Proceeding of Linear, Time, Branching Time and Partial Order in Logics and Models for Concurrency, Berlin, 30 May-3 June 1989, 364-397.
[2]
Baldan, P., Busi, N., Corradini, A. and Pinna, G.M. (2000) Domain and Event Structure Semantics for Petri Nets with Read and Inhibitor Arcs. Theoretical Computer Science, 323, 129-189. https://doi.org/10.1016/j.tcs.2004.04.001
[3]
Kuang, H. (2013) Towards a Formal Reactive Autonomic Systems Framework Using Category Theory. Ph.D. Thesis, Concordia University, Montreal.
[4]
Sampson, A.T. (2008) Process-Oriented Patterns for Concurrent Software Engineering. Ph.D. Thesis, University of Kent, Kent.
[5]
Hinchey, M.G., Rouff, C.A., Rash, J.L. and Truszkowski, W.F. (2005) Requirements of an Integrated Formal Method for Intelligent Swarms. Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, 5-6 September 2005, 125-133. https://doi.org/10.1145/1081180.1081196
[6]
Zhu, M., Grogono, P. and Ormandjieva, O. (2017) Exploring Relationships between Syntax and Semantics of a Process-Oriented Language by Category Theory. Proceedings of the 8th International Conference on Ambient Systems, Networks and Technologies, Madeira, 16-19 May 2017, 241-248. https://doi.org/10.1016/j.procs.2017.05.342
[7]
Zhu, M., Grogono, P., Ormandjieva, O. and Kuang H. (2016) Using Failures and Category Theory to Verify Process Communications between Design and Implementation of Concurrent Systems. Proceedings of the 7th International Conference on Ambient Systems, Networks and Technologies, Madrid, 23-26 May 2016, 700-704. https://doi.org/10.1016/j.procs.2016.04.155
[8]
Loogen, R. and Goltz, U. (1991) Modelling Nondeterministic Concurrent Processes with Event Structures. Fundamenta Informaticae, 14, 39-73.
[9]
León, H.P.D., Haar, S. and Longuet, D. (2012) Conformance Relations for Labeled Event Structures. Proceedings of the 6th International Conference on Tests and Proofs, Prague, 31 May-1 June 2012, 83-98. https://doi.org/10.1007/978-3-642-30473-6_8
[10]
Castellan, S. and Clairambault, P., Rideau, S. and Winskel, G. (2016) Concurrent Games. Logical Methods in Computer Science, 13, 1-51.
[11]
Bruni, R., Melgratti, H. and Montanari, U. (2006) Event Structure Semantics for Nominal Calculi. Proceedings of 17th International Conference on Concurrency Theory, Bonn, 27-30 August 2006, 295-309.
[12]
Winskel, G. and Nielsen, M. (1995) Models for Concurrency. Handbook of Logic in Computer Science, Vol. 4, 1-148.
[13]
Nielsen, M., Sassone, V. and Winskel, G. (1996) Models for Concurrency: Towards a Classification. Theoretical Computer Science, 170, 297-348. https://doi.org/10.1016/S0304-3975(96)80710-9
[14]
Hildebrandt, T.T. (2000) Categorical Models for Fairness: Completion vs. Delay. Proceedings of the First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, Cork, 20-21 July 2000, 188.
[15]
Sisiaridis, D., Kuchta, V. and Markowitch, O. (2016) A Categorical Approach in Handling Event-Ordering in Distributed Systems. Proceedings of IEEE 22nd International Conference on Parallel and Distributed Systems, Wuhan, 13-16 December 2016, 1145-1150. https://doi.org/10.1109/ICPADS.2016.0150
[16]
Enguix, G.B. and Lopez, M.D.J. (2007) Agent-Environment Interaction in a Multi-Agent System: A Formal Model. Proceedings of the GECCO Conference on Genetic and Evolutionary Computation, London, 7-11 July 2007, 2607-2612.
[17]
Goubault, E. and Mimram, S. (2010) Formal Relationships between Geometrical and Classical Models for Concurrency. Proceedings of the Workshop on Geometric and Topological Methods in Computer Science, Denmark, 11-15 January 2010, 77-109.
[18]
Abdel Gawad, M.A. (2017) Novel Uses of Category Theory in Modeling OOP. CoRR, abs/1709.08056, 1-8.
