An Algebraic Framework for Defining Behaviours of Concurrent Systems. Part 1: The Constructive Presentation

• Autorzy: Winkowski J.
• Języki publikacji: EN

Abstrakty

EN

The paper is the first part of a two-part paper that contributes with a concept of a process viewed as a model of a run of a phenomenon (discrete, continuous, or of a mixed type), with operations allowing to define complex processes in terms of their components, with the respective algebras, and with the idea of using the formal tools thus obtained to describe the behaviours of concurrent systems. A process may have an initial state (a source), a final state (a target), or both. A process can be represented by a partially ordered multiset. Processes of which one can be a continuation of the other can be composed sequentially. Independent processes, i.e. processes which do not disturb each other, can be composed in parallel. Processes may be prefixes, i.e. independent components of initial segments of other processes. Processes in a universe of objects and operations on such processes form a partial algebra, called algebra of processes. Algebras of processes are partial categories with respect to the sequential composition, and partial monoids with respect to the parallel composition. Algebras of processes can be used to define behaviours of concurrent systems. The behaviour of a system can be defined as the set of possible processes of this system with a structure on this set. Such a set is prefix-closed. The structure on this set reflects the prefix order and, possibly, specific features of the behaviour like observability, the relation to flow of real time, etc. Algebras of processes can also be used to define behaviours, to define operations on behaviours similar to those in the existing calculi of behaviours, and to define random behaviours. The first part of the whole paper investigates algebras of processes and their applications to describing behaviours of systems. In the second part the properties of algebras of processes described in the first part are regarded as axioms defining a class of abstract partial algebras, called behaviouroriented algebras, and they initiate a theory of such algebras.

Słowa kluczowe

EN

process; state; sequential composition; parallel composition; category; partial category; partial monoid; independence; structure; behaviour; random behaviour

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 97, nr 1/2
• Strony: 235--273
• Opis fizyczny: Bibliogr. 34 poz.

Twórcy

autor

Winkowski J.

• Józef Winkowski, Instytut Podstaw Informatyki PAN, Ordona 21, 01-237 Warszawa, Poland,

Bibliografia

• [1] Baldan, P., Bruni, R., Montanari, U., Pre-nets, read arcs and unfolding: a functorial presentation, Proceedings of WADT'02,Wirsing, M., Pattison, D., Hennicker, R., (Eds.), Springer LNCS 2755 (2002) 145-164
• [2] Bergstra, J., Klop, J., The algebra of recursively defined processes and the algebra of regular processes, in Paradaens, J., (Ed.), Proc. of 11th ICALP, Springer LNCS 172 (1984) 82-95
• [3] Best, E., Devillers, R., Sequential and Concurrent Behaviour in Petri Net Theory, Theoret. Comput. Sci. 55 (1987) 87-136
• [4] Corradini, A., Montanari, U., Rossi, F., Graph Processes, Fundamenta Informaticae 26 (1996), 241-265
• [5] Degano, P., Meseguer, J., Montanari, U., Axiomatizing Net Computations and Processes, in Proc. of 4th LICS Symposium, IEEE (1989) 175-185
• [6] Droste, M., Shortt, R. M., Continuous Petri Nets and Transition Systems, in Ehrig, H., et al. (Eds.), Unifying Petri Nets, Springer LNCS 2128 (2001) 457-484
• [7] Glabbeek, R., J., van, Plotkin, G., D., Configuration Structures, Proceedings of LICS'95, Kozen, D., (Ed.), IEEE Computer Society Press (1995) 199-209
• [8] Hart, S., Sharir, M., Pnueli, A., Termination of Probabilistic Concurrent Programs, ACM Trans. On Programming Languages and Systems, Vol. 5, No. 3, July 1983, 356-380
• [9] Kwiatkowska, M., Model checking for probability and time: from theory to practice, Proc. of 18th IEEE Symposium on Logic in Computer Science (LICS'03), IEEE Computer Society Press (2003), 351-360
• [10] Lynch, N., Segala, R., Vaandrager, F., Observing Branching Structure Through Probabilistic Contexts, Siam Journal on Computing 37 (4), 977-1013, September 2007
• [11] Meseguer, J., Montanari, U., Sassone, V., Process versus Unfolding semantics for Place/Transition Nets, Theoret. Comput. Sci. 153, n. 1-2 (1996) 171-210
• [12] Meyer, P. A., Probability and Potentials, Blaisdell Publishing Company,Waltham, Massachusetts, Toronto, London (1966)
• [13] Milner, R., Synthesis of Communicating Behaviour, Proc. of MFCS'78, Winkowski, J. (Ed.), Springer LNCS 64 (1978) 71-83 (1980)
• [14] Milner, R., A Calculus of Communicating Systems, Springer LNCS 92 (1980)
• [15] Milner, R., Calculi of interaction, Acta Informatica 33 (1996) 707-737
• [16] Mitra, S., Lynch, N., Trace-based Semantics for Probabilistic Timed I/O Automata, Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy, April 3-5, 2007, Springer LNCS 4416, Full version: http://theory.lcs.mit.edu/~mitras/research/PTIOA-066 -full.pdf (1980)
• [17] Montanari, U., Rossi, F., Contextual Nets, Acta Informatica 32 (1995) 545-596
• [18] Nerode, A., Kohn,W., Models for Hybrid Systems: Automata, Topologies, Controllability, Observability, Springer LNCS 736 (1993) 317-356
• [19] Parthasarathy, K. R., Introduction to Probability and Measure, New Delhi (1980)
• [20] Petri, C. A., Introduction to General Net Theory, in W. Brauer (Ed.): Net Theory and Applications, Springer LNCS 84 (1980) 1-19
• [21] Pluenecke, H., K-density, N-density and finiteness properties, APN 84, Springer LNCS 188 (1985) 392-412
• [22] Pnueli, A., Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, in: J. W. de Bakker, W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Comp. Sc. 224, Springer, Berlin, 1986, 510-584
• [23] Reisig, W., Petri Nets: An Introduction, Springer-Verlag (1985)
• [24] Rozenberg, G., Thiagarajan, P. S., Petri Nets: Basic Notions, Structure, Behaviour, in J. W. de Bakker,W. P. de Roever and G. Rozenberg (Eds.): Current Trends in Concurrency, Springer LNCS 224 (1986) 585-668
• [25] Varacca, D., V¨olzer, H., Winskel, G., Probabilistic Event Structures and Domains, in P. Gardner and N. Yoshida (eds.), CONCUR 2004, Springer LNCS 3170 (2004), 497-511
• [26] Winkowski, J., Maggiolo-Schettini, A., An Algebra of Processes, Journal of Comp. and System Sciences, Vol. 35, No. 2, October 1987, 206-228
• [27] Winkowski, J., Behaviours of Concurrent Systems, Theoret. Comput. Sci. 12 (1980) 39-60
• [28] Winkowski, J., An Algebraic Description of System Behaviours, Theoret. Comput. Sci. 21 (1982) 315-340
• [29] Winkowski, J., An Algebraic Characterization of Independence of Petri Net Processes, Information Processing Letters 88 (2003), 73-81
• [30] Winkowski, J., Towards a Framework for Modelling Systems with Rich Structures of States and Processes, Fundamenta Informaticae 68 (2005), 175-206, http://www.ipipan.waw.pl/~wink/winkowski.htm
• [31] Winkowski, J., An Axiomatic Characterization of Algebras of Processes of Petri Nets, Fundamenta Informaticae 72 (2006), 407-420, http://www.ipipan.waw.pl/~wink/winkowski.htm
• [32] Winkowski, J., Behaviour Algebras, Fundamenta Informaticae 75 (2007), 537-560 http://www.ipipan.waw.pl/~wink/winkowski.htm
• [33] Winkowski, J., Towards a Framework for Modelling Behaviours of Hybrid Systems, Fundamenta Informaticae 80 (2007), 311-332 ICS PAS Report 1002 (2007), http://www.ipipan.waw.pl/~wink/winkowski.htm,
• [34] Winkowski, J., An Algebraic Framework for Defining Random Concurrent Behaviours, Fundamenta Informaticae 85 (2008), 481-496, http://www.ipipan.waw.pl/~wink/winkowski.htm,