Quantitative and Qualitative Extensions of Event Structures
Joost-Pieter Katoen · 1996
An important application of formal methods is the speci cation, design, and analysis of functional aspects of (distributed) systems.Recently the study of quantitative aspects of such systems based on formal methods has come into focus.Several extensions of formal methods where the occurrence of actions can be assigned a ( xed) probability and/or the time of occurrence of actions can be constrained are known from the literature.An important reason for enhancing formal methods with quantitative notions is to facilitate the analysis of performance characteristics of system designs.In this way the eciency of design alternatives can be assessed such that in early design stages designs can be rejected because of unsatisfactory performance characteristics, thus avoiding costly redesign at later stages.A formal speci cation incorporating quantitative aspects can also be very useful for establishing a well-understood and eective way of developing performance models, such as Markov chains and queuing networks, from system speci cations.Quantitative extensions of formal methods that are based on interleaving of causally independent actions have been amply investigated.Interleaving models abstract from the fact that a system is actually composed of a set of (partly) independent subsystems.The global system state is considered without due regard of its distributed nature.The system's behaviour is modelled in terms of sequences of actions that are totally ordered by precedence and in which actions of one independent subsystem are merged with actions of others.This dissertation deals with quantitative and qualitative extensions of event structures, a prominent branch of partial-order, or noninterleaving, models for concurrency.Example extensions are the incorporation of issues like time, both real-time and stochastic of nature, urgency (timeouts), and probability.Nowadays the treatment of these concepts in noninterleaving models has only been scarcely addressed.Noninterleaving models do not abstract from the fact that a system consists of a set of (partly) independent subsystems.The notion of global state does not play a central rôle in these models.The systems' behaviour is modelled in terms of sequences of actions that are not required to be totally ordered, but that are partially ordered.The causal dependencies between actions are re ected in this partial order.Interleaving and noninterleaving models are complementary in the system's design process.In this dissertation we basically deal with noninterleaving models, but also provide the ingredients to obtain corresponding interleaving models.This facilitates the use of both types of models in a coherent way and enables a comparison with existing approaches.Starting points for this dissertation are extended bundle event structures, an adaptation of the traditional event structures of Winskel to t the speci c requirements of multi-party synchronization and disruption, and iii iv Summary process algebras, abstract description formalisms for distributed systems that consist of powerful composition operators.Summary v currence times of actions is constrained by exponential, or the more general and practical, phase-type distributions, and a probabilistic variant that contains an (internal) probabilistic choice operator.For each variant a denotational semantics in terms of the corresponding quantitative extension of extended bundle event structures is provided.This is performed in a modular way such that combinations (like time and probability) can be made in a rather straightforward way.In addition, for most aforementioned process algebras an event-based operational semantics is presented.This operational semantics keeps track of the occurrence of actions, rather than the actions themselves (as usual in structured operational semantics), and provides a basis for comparison with existing quantitative extensions of interleaving models.The operational rules obtained for the real-time case are a novel (and minimal) extension to the untimed case; for the urgent case the rules strongly resemble a proposal of Bolognesi, Lucidi and Trigila; for the stochastic exponential case the rules resemble that of several existing stochastic process algebras, and for the probabilistic case we obtain rules that are related (but simpler) to work of Hansson and Jonsson.The relationship between these operational semantics and the denotational semantics is thoroughly investigated.The incorporation of recursion in all extensions of process algebras in this dissertation is treated in Chapter 10.Using standard domain theory the denotational semantics of the quantitative extensions of PA is extended in order to cover recursively de ned processes.The same is done for the event-based operational semantics.It is shown that the consistency results for the nite case carry over to the recursive case.Chapter 11 contains a retrospective view on the work presented in this dissertation, summarizes the main technical results and provides some overall conclusions.vi Summary \Abandonment of causality as a matter of principle should be permitted only in the most extreme emergency" Albert Einstein, 1924 1 This chapter highlights the main topics of this dissertation and sketches its context.The chapter brie y introduces the aspects of using formal models for concurrency in the design of distributed systems, and motivates the need for integrated formal and quantitative methods to eectively support this design process.The importance of the notion of causality for distributed systems' design is described.A synopsis is given of the contents of this dissertation. Chapter 2: Extended bundle event structuresNotice that init(E) equals the set of enabled events after the empty trace, i.e., en(").Successful termination events are events that are labelled with , the successful termination action. Definition. (Successful termination events)The set of successful termination events of E is de ned by exit(E) , f e 2 E j l(e) = g.E[ [ ] ] is de ned recursively according to the following de nitions.We suppose there is an in nite universe E U of events.In the rest of this section let E[ [ B i ] ] = E i = (E i ; i ; 7 !i ; l i ), for i=1; 2 with E 1 \ E 2 = ?. (If E 1 \ E 2 6 = ?then a suitable event renaming can be applied extended to , 7 !and l.) 2.35.Definition.(Semantics of 0, p , a ;, and +) E[ [ 0 ] ] , (?; ?; ?; ?)E[ [ p ] ] , (f e g; ?; ?; f (e ; ) g) for some e 2 E U E[ [ a ; B 1 ] ] , (E; 1 ; 7 !; l 1 [ f (e a ; a) g) where E = E 1 [ f e a g for some e a 2 E U n E 1 7 != 7 ! 1 [ (f f e a g g init(E 1 )) E[ [ B 1 + B 2 ] ] , (E 1 [ E 2 ; ; 7 ! 1 [ 7 ! 2 ; l 1 [ l 2 ) where = 1 [ 2 [ (init(E 1 ) init(E 2 )) [ (init(E 2 ) init(E 1 )): The semantics of 0 and p is self-explanatory.In E[ [ a ; B 1 ] ] a bundle is introduced from the new event e a (labelled a) to all initial events in E 1 as e a causally precedes these events.E[ [ B 1 +B 2 ] ] is equal to E 1 [ E 2 extended with mutual con icts between all initial events of E 1 and E 2 such that in the resulting structure only either B 1 or B 2 can happen.2.36.Example.Let Figure 2.5 (a) through (c) depict the event structures corresponding to B 1 through B 3 , respectively.Then Figure 2.5 (d) and (e) depict E[ [ a ; B 1 ] ] and E[ [ B 2 +B 3 ] ], respectively.2.37.Definition.(Semantics of n, [ ], >> and [>) E[ [ B 1 n G ] ] , (E 1 ; 1 ; 7 ! 1 ; l) where (l 1 (e) 2 G ) l(e) = ) ^(l 1 (e) 6 2 G ) l(e) = l 1 (e)) E[ [ B 1 [H] ] ] , (E 1 ; 1 ; 7 ! 1 ; H l 1 ) E[ [ B 1 >> B 2 ] ] , (E 1 [ E 2 ; ; 7 !; l) where = 1 [ 2 [ f (e; e 0 ) j e; e 0 2 exit(E 1 ) ^e 6 = e 0 g 7 != 7 ! 1 [ 7 ! 2 [ (f exit(E 1 ) g init(E 2 )) l = ((l 1 [ l 2 ) n (exit(E 1 ) f g)) [ (exit(E 1 ) f g) E[ [ B 1 [> B 2 ] ] , (E 1 [ E 2 ; ; 7 ! 1 [ 7 ! 2 ; l 1 [ l 2 ) where = 1 [ 2 [ (E 1 init(E 2 )) [ (init(E 2 ) exit(E 1 )): Chapter 3: Disjunctive causality and interleaving) f calculus g (e 2 # < e ^e0 2 # < e 0 ) _ e = e 0 ) f # < e 2 men([] ; e) ) e 6 2 # < e g e = e 0 .2. We prove that < is transitive; this implies that < is transitive.e < e 0 ^e0 < e 00 , f De nition 3.12 g e 2 # < e 0 ^e0 2 # < e 00 ) f De nition 3.13 g e 2 # < e 0 ^#< e 0 # < e 00 ) f calculus g e 2 # < e 00 , f De nition 3.12 g e < e 00 .3.15.Example.Consider again the dual event structures of Figure 3.4.The maximal operational lposets of Figure 3.4(a) are e a !e c e b and e a e b !e c .Figure 3.4(b) has the following maximal operational lposets: e a !e c !e d e b , e a !e c e b !e d , and e a e c % e b !e d .Note that e a e b !e c !e d is not obtained as an operational lposet while it is an intensional lposet.Finally, Figure 3.4(c) has the following maximal operational lposets: e