×

Bundle event structures: a revised cpo approach. (English) Zbl 1043.68068

Summary: Bundle event structures equipped with a partial order \(\triangleq\) have been used to give a true concurrency denotational semantics for LOTOS. This model has also been extended by time and stochastic information. Unfortunately it fails to yield a complete partial order (cpo) as we illustrate by an example. We propose a subset of all bundle event structures such that it forms a cpo. This subset is closed under the usual operators on bundle event structures. And as a consequence these operators are continuous. Therefore, this subset can be used to give a denotational semantics of LOTOS.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

LOTOS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S.; Jung, A., Domain theory, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, 3 (1994), Clarendon Press: Clarendon Press Oxford), 1-168
[2] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Comput. Networks ISDN Systems, 14, 25-59 (1987)
[3] Boudol, G.; Castellani, I., Flow models of distributed computations: event structures and nets, Report 1482 (1991), INRIA
[4] Bowman, H.; Derrick, J., Extending LOTOS with time: A true concurrency perspective, (Bertran, M.; Rus, T., Transformation-Based Reactive Systems Development. Transformation-Based Reactive Systems Development, Lecture Notes in Comput. Sci., 1231 (1997), Springer: Springer Berlin), 383-399
[5] Bowman, H.; Katoen, J.-P., A true concurrency semantics for ET-LOTOS, (Applications of Concurrency to System Design (1998), IEEE Computer Society Press), 228-239
[6] Brinksma, E.; Katoen, J.-P.; Langerak, R.; Latella, D., A stochastic causality-based process algebra, Computer J., 38, 7, 552-565 (1995)
[7] Katoen, J.-P., Quantitative and qualitative extension of event structures, PhD Thesis (1996), Enschede: Centre for Telematics and Information Technology: Enschede: Centre for Telematics and Information Technology Enschede, The Netherlands
[8] Katoen, J.-P.; Baier, C.; Latella, D., Metric semantics for true concurrent real time, Theoret. Comput. Sci., 254, 501-541 (2001) · Zbl 0976.68103
[9] Katoen, J.-P.; Langerak, R.; Latella, D., Modelling systems by probabilistic process algebra: An event structures approach, (Tenney, R. L.; etal., Formal Description Techniques, VI (1994), Elsevier: Elsevier Amsterdam), 253-268
[10] Katoen, J.-P.; Langerak, R.; Latella, D.; Brinksma, E., On specifying real-time systems in a causality-based setting, (Jonsson, B.; Parrow, J., Formal Techniques in Real-Time and Fault-Tolerant Systems. Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Comput. Sci., 1135 (1996), Springer: Springer Berlin), 385-404
[11] Langerak, R., Transformations and semantics for LOTOS, PhD Thesis (1992), Department of Computer Science, University of Twente
[12] Langerak, R., Bundle event structures: A non-interleaving semantics for LOTOS, (Diaz, M.; Groz, R., Formal Description Techniques, V (1993), Elsevier: Elsevier Amsterdam), 331-346
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.