<TITLE: Weakest Congruences, Fairness and Compositional Process-Algebraic Verification
ACADEMIC DOMAIN: technology
DISCIPLINE: information technology
EVENT TYPE: doctoral defence discussion
FILE ID: UDEFD060
NOTES: presentation UDEFP060 in Finnish, not transcribed

RECORDING DURATION: 92 min 21 sec

RECORDING DATE: 27.5.2004

NUMBER OF PARTICIPANTS: unknown

NUMBER OF SPEAKERS: 4

S1: NATIVE-SPEAKER STATUS: Finnish; ACADEMIC ROLE: research student; GENDER: male; AGE: 31-50

S2: NATIVE-SPEAKER STATUS: French (Belgium); ACADEMIC ROLE: senior staff; GENDER: male; AGE: 31-50

S3: NATIVE-SPEAKER STATUS: Finnish; ACADEMIC ROLE: senior staff; GENDER: male; AGE: 51-over

S4: NATIVE-SPEAKER STATUS: Finnish; ACADEMIC ROLE: unknown; GENDER: male; AGE: unknown

SS: several simultaneous speakers>


<S1> appointed by the department council i would i'd like to ask you to make such remarks about my thesis as you see appropriate </S1>
<P:16>
<S2> well the <COUGH> thesis being defended today is about concurrent reactive systems , (about er several of the questions) in the thesis the argument is made that these systems are important and more and more common and that is undoubtedly so , indeed we are surrounded by devices which contain er software and this software is reactive because it's interacting with its environment it's concurrent because it has to be designed so in order to handle multiple tasks concurrently , and the next argument made in the thesis is that such software is hard to design correctly and hard to keep up , and this is also undoubtedly true because when we use such software we realise that , <SS> [@@] </SS> [@too many microphones@] , when we use such software we realise that it often has errors and because how the device is embd- er embedded reactive software that (has) some cons and (xx) correct , but the message of the thesis is that there's hope in this for this problem because you can model such software and er take these (xx) to analyse the software and maybe verify that it is free of problems . notice you get software for your problems but the methods are not free of problems because there's the famous state-based explosion problem , i want to discuss this explosion problem , where the idea is that it er this concurrent reactive software is hard to analyse because it has lots of possible behaviours , and of course looking at (through their hands) you cannot sort of analyse all the behaviours you hope that the er computer can do the job for you and analyse all the behaviours but even for a computer the number of possible behaviours is so large that it quickly becomes impossible and this is the state-based explosion and so an explosion of number of states and behaviours that is really making these techniques very difficult to apply , maybe tonight this is somewhat more concrete we're talking about er a large number in common language it's often referred to as an astronomical number because distances in astronomy are are huge , but i think we have to realise that astronomical numbers compared to the size of states bases are really very small so maybe we should start introducing a new expression which is a states-based number <SS> @@ </SS> . now confronted with such a problem what can you do , well in the thesis which are defended being defended today a stress has been made to the modelling formalism and this modelling formalism is a var- variety of process algebra , need i say why process algebra is it er good formalism , er well i guess the defendant's merely er said some things about that to leave room for discussion but i'll give you a few ideas about why process algebra is really an important topic , it was (xx) (by the way you) sort of examined the definitions but it has something which a lot of othe- others do not have it is really a lot of of programs so it really allows you to model you know what you (write) as programs and indeed if it is an algebra it's because its emphasis is on alterations which lets you compose programs simple (project) to get more complicated programs that's where the algebra er name comes from , and of course with the alterations of things like concurrent compositions put two things together let them work (xx) concurrently as you have to be able to analyse what happens . and the fact's that process-algebra lets you compose these gives us maybe some hope of being able to handle this state-based explosion problem and the hope is that you can sort of divide to con- to control because , if you can sort of analyse the (class) and maybe simplify the (class) before composing them you have get er much better handle of the total behaviour without having the state-based explosion . so , er the thesis being defended today addresses problems related to the use of process algebra and it deals with really two topics the first being a semantical er topic , and the second one sort of er also sort of semantic but er linked to what you need to actually use process algebra to verify some problems (of these systems) let's first go to the the semantics topic . at the semantics topics really addresses a very simple and natural question it says it asks when are two components the same , there are lots of programs and say when are two components the same , well you might think this is completely obvious i mean if they're the same they are the same but s- sameness does not have to be identity , let me maybe make this concrete and most of you in the room i'm sure have used a laptop it's a component has lots of software , now this phone interacts with a network . and to the network , if you change your phone you throw out the phone buy a new one of another model does it look the same it's not the same phone but in some ways to the network it has to look the same because it's providing the same functionalities , so the question of when two components in the system can be exchanged one for the other is not an obvious one and even to be to to be careful about in how to decide that things are indeed the same or not , and the thesis here deals with the question in a very rational and very <SIC> methodoligical </SIC> methodoli- methodoli- sorry methodical way what it says is to decide if things are the same you need to know first what are the properties you interested in seeing when you put things together , what you need to look at when you put things together , i'm going to (xx) that if i want to make sure that some things are preserved when i look at the global system i need usually to preserve more on the components because the interactions can sort of affect the global behaviours in ways that are not really captured if you just look at the behaviours of the components as if they were the global system . so the way you define this notion of sameness is to say let's look at what we need to check globally let's see let's look at what alterations are that lets us combine things and from there let's try and define a suitable notion of identity or sameness of equivalence , and if the notion the title of thesis was not talking about equivalence but congruence it's simply because congruence is a mathematical word to say that this equivalence is preserved by the composition alterations . and what the thesis does is looks at two very special cases of properties you want to design to to verify globally and gives the corresponding se- semantics in a very precise way in the sense that it uses it gives a weakest semantics and why is it important to have something er weak semantic because we don't want to say that things are different when they're not really when whe- that when they don't really need to be different so we want to be able to say things are the same and save save as much as possible compatible with the (goal of) checking properties (there) . same issue that when the the- in the thesis is fairness , now fairness is is a word you know you all know in in common language but here it has sort of a a more precise and er <COUGH> er <COUGH> definite meaning , the problem is that if you look at models of components of a system given in process algebra combine these models and then look at the system globally and see if it satisfies some properties you will notice that it does not . of course it depends on the property you look at but it does not especially whether you're looking at properties that imply progress on the system , properties that imply that the system actually does something reaches the goal not just that it behaves in a safe way but that it actually does what it's it's intended to do , and the reasons for this is that when you look at your system globally well it can get caught in some sort of loops . but when you do a more careful analysis you see that these loops do not really happen , because er things are not going to be implemented in a way that is going to allow these loops , that means you're not as (probably) close enough to the implementation that's true to some <SIC> extents </SIC> but you don't want to be you know that close to implementation that you're very specific in your model and also that you make things (unmanageable) so what you do is you (ought) to say well the model is constrained but in a limited way that reflects what any reasonable implementation would do and that is sufficient for allowing you to check these properties and this is what is called a fairness assumption and in the thesis there's quite a bit of work big part of the thesis devoted to how to model these fairness assumptions and how to use them in order to verify properties and this is essential because without that a lot of things cannot be verified . finally there's a last point of the thesis that deals with parametric systems in some ways er parametric in the sense that when you're looking at a very complex er network well you don't know exactly what its configuration's going to be i was talking about mobile phone networks of course i didn't (talk about) someone (gets) switched on an additional phone in the network . so how do you check a system which is so dynamic so changing well one way to do this is to say well i have a model and in the model there's a parameter that says how many components there can be and i want to check that the system works correctly whatever the number of components is , and this is docum- you know there's a problem this is a little bit this type of (xx) not exactly (xx) to describe but works in this direction by being able to check systems where the number of components here i'm just (spotting er) (xx) transmitting er data can vary and er checking that indeed the system is correct independently of the size of the number of components in the system . so we have the thesis dealing with a lot of i would say very important and interesting topics on which there has been quite a lot of work previously and on which contributions are being made here and this is the conclusion of my opening statements and i think i leave the rest of my remarks to the debate </S2>
<P:22>
<S2> okay so we have here er sort of given a (survey) of the topic of which you working and the , some of the results in your in your thesis but i think it would be good to start our debate by hearing your opinion on of the motivations of what you're doing and er i think in the one way to to s- introduce the debate is to look at the words in in the title of your thesis which is quite long and and start with the last word which is verification . so i've so- given some motivation for for you know analysing concurrent and reactive systems but you imply by the title of your thesis that the goal is to verify , and i've two basic questions about this word , one what is exactly verification when you consider the system is verified and we have some examples in the protocols (xx) in your thesis you consider that you've verified them , and two for situations where the examples are not you know reasonably small and let's say academic is it possible </S2>
<S1> mhm well i would say that verification means that we try to obtain a very high er level of confidence in the system that is er , something better than just having a some reasonable probability that the system is correct but that we have such a complete picture of the behaviour of the system that we can with very high confidence believe that the system is working correctly and the way that we intend to </S1>
<S2> how do you know that what you intend to have as a system is actually the correct behaviour </S2>
<S1> er that is a very difficult question with er formal modelling er </S1>
<S2> that's why i ask it </S2>
<SS> @@ </SS>
<S1> erm , there's always the possibility that that our idea how the system should behave is is somehow flawed in itself but , er , er , well first of all we should perhaps make the distinction that er . er , well the system can be verified in the sense that it , it er complies with our definition of how it should behave and </S1>
<S2> but let's be let's be concrete i mean in your thesis you handle the examples of of protocols altering basic variants of this er protocol and there i mean you're operating under the the basic assumption that the the be- correct behaviour is send-receive and then peat- repeating the sequence of events <S1> mhm </S1> of course in your model sequence you've extracted from the values of the data being transmitted <S1> yes </S1> now okay even if you check that under this assumption the behaviour globally is going to be a sequence of sends one side and receive on other side how do you know that the extractions you made are adequate </S2>
<S1> well i have to say that er er without the modelling of the data values it's not entirely appropriate yet er if it were a real protocol that we were verifying i would like to see a more thorough analysis that involves also the er the data values and and well of course we can model also the data values but er i think this simple model er serves more as an example than than than a shall we say a verification at the at an industrial level </S1>
<P:05>
<S2> okay , should we move one word back in the title @@ </S2>
<SS> @@ </SS>
<S2> so process-algebraic well er i think i get myself some justification for , you know the use of process algebras which is the emphasis on on program er composition alterations (which) (xx) gives the er both the (xx) programs and also gives us some hope to compositionality , but a question that i you know always have when i'm er looking at process algebras is that okay some some ways process algebra is a a very limited programming language , now , is this realistic because people don't write don't write programs in process algebra , they write you know in other languages java or whatever </S2>
<S1> yes well er i think the goal is a bit different in in process algebra than in in in ordinary programming with java and or other programming languages i think in a in a sense in process-algebraic approac- approach we have abstracted away er a lot of what is involved in in common programming and we just look at look at certain features of the of the system er which is mainly the the interaction between the components rather than the the the the internal behaviour of a component or how it is programmed and and for example in process algebra we can mod- model non-deterministic choices whereas in real programs we we don't have non-deterministic choices but we can er build a simple model of of a program which has non-deterministic choices so i think process algebra can be used as a kind of </S1>
<S2> er i think that is a good topic non-deterministic choices , i mean the world is not non-deterministic or maybe you believe it is i don't know , so when you have a non-deterministic choice in the program what does it really represent </S2>
<S1> er i think it represents that , we don't want to or er we cannot model what is exactly going on but we just give our alternatives how it's good to behave and we we then by giving these alternatives take er the count of the different possibilities that can can happen without modelling in detail how how this choice happens or what er the details (level) is going on in the system so that is also useful abstraction </S1>
<S2> mhm , yes that also maybe but i i think non-determinism as as (xx) absence of knowledge about the detailed behaviour and being a (good) abstraction for the topic so i completely agree on that aspect . right if i may move one word further compositional . the motivation for doing compositional you know reasoning is quite clear you know you want to to divide a system verify parts and put things back together , but you have examples of verifications in your thesis , and my question is are they compositional </S2>
<S1> mhm , well , for example the , invariant example that i (was) working with in a in the last paper i would say that compositionality is is a requirement for for doing that that kind of analysis so , i think com- compositional- well so compositionality is a pre- prerequisite for for doing that that analysis so our our approach has to be compositional </S1>
<S2> you meaning on the technical point of view because clearly i mean technically you have to have the the properties of the relations to compare the processes and so on which are you know preserved by the (operating system) so that way there is compositionality but from methodological point of view </S2>
<S1> well i would say that from a methodological point of view the this our (xx) that we have obtained here are also compositional in the sense that we have , i- modelled of the behaviour of the protocol from external point of view and we can we can use this model further if we like we can use it as a component in another system </S1>
<S2> that's right so so if you take that er <COUGH> the cases of the transmission protocols . in some ways what you've done is is check that in the (xx) conflict could be replaced by something more simpler which (will allow) compositional verification of something using this protocol but the verification itself is not compositional , or is it </S2>
<S1> mhm well can be in in the sense that you have freedom in for example how you compose the protocol from the subprocesses so you could even if you were using invariance or thing like that you can you have freedom in composing the system in any order you like and </S1>
<S2> but <S1> [i mean] </S1> [in your] in your examples you abstract before composing </S2>
<S1> er , yes yes in a sense erm , well for example in invariant example when you had a component and and you and you you hide away or abstract away the intermediate actions and then you redu- reduce the system so and also in the other verification examples that has been done and parts of the system are put together and the , the internal actions are abstracted away and the the that part of the system is reduced </S1>
<S2> right . i think i won't go into about the word and <SS> @@ </SS> @that could be a topic of (xx) debates@ , fairness , again i i agree with the use of fairness i mean it's a topic i've i've worked with f- with for many years as you know and and indeed if you don't have fairness assumptions th- they are are you cannot do some verification decent verification er er so the verifications of some properties is not possible but er in some of your examples you use fairness to model the fact that some channel does not use it do not lose definitely it is a message . but are channels fair or probabilistic </S2>
<S1> erm , i would say that fairness is a weaker requirement than than being probabilistic so er <S2> in what sense </S2> er fairness doesn't really imply anything about the distribution of the er of the of the well whatever we are observing so i think fairness is something weaker makes a weaker assumption so we are using fair fair models and and in a way this also then covers probabilistic systems </S1>
<S2> so you're saying that probabilistic system is fair at least under some er [a reasonable probabilistic system is going to be fair] </S2>
<S1> [yes yes yes] yes </S1>
<S2> actually i agree i think indeed <COUGH> i mean fairness is a is a sort of a of a limit of of probabilistic systems to to say so the minimum requirement on of the er er probabilistic system but another problem with fairness is that you know fairness does not correspond to any implementation you cannot implement fairness as is , so what does it mean when you've verified a fair system </S2>
<S1> well er as you said it is a kind of limit of of , of s- well we could say there's a limit of of systems that are implementable so in a by using a fairness assumption we sort of cover all those systems that can represent real implementations to verify them so again this is kind of a useful abstraction more than an implementation </S1>
<S2> quite (agreed) . if i maybe can finish this line of questioning before giving the floor to the other opponent , well i take both the the first two words together . just to make things a bit quicker and also because congruence you know is such a nice mathematical concept that it's hard to argue about it but weakest congruence , i mean the motivation for your your the first two papers which are on the the body of your thesis that you really want you know to have the best possible notion of of of congruence as equivalence preserved by (operations) and say when you can be as weak as possible but from a practical point of view of analysing systems , the fact that you can actually check equivalence congruence effectively is sometimes more important than having the most precise notion , because , you know you can lose in both ways if you don't have if you have a notion which is not you know the weakest then you might decide that two components are different whereas they really could be considered to be the same . but on other hand if it costs you a lot to check that or it makes it impossible it costs you so much to check this notion of equivalence that you cannot do it (xx) it's much better to check a more approximate notion for which you have efficient congruence so can you comment on this issue </S2>
<S1> yes er you're right that it's always not er er that it can be difficult more difficult to check the weaker congruence than the stronger one and in some cases it might be the case that er it's not worth the effort to to use the weakest but i think it is still nice to have the freedom of choice whether we take the weaker or the stronger as it were it never hurts to know what is the weakest congruence and how how weak or how weak a equivalence we can use and within that limit we can we can choose the the practical approach </S1>
<S2> er are there notions you have defined practical or the algorithms that correspond to them </S2>
<S1> erm i have to say that i don't have algorithms for checking my the weakest congruences i have developed here [but of course] </S1>
<S2> [but they exist right] i mean the the problem at least f- f- for of course for finite states er systems you could check those notions </S2>
<S1> yes yes they i'm sure they could be checked but i don't have here any specific algorithms for </S1>
<S2> so you have no idea of the complexity of the problem or </S2>
<S1> er well to be honest i i can only make guesses at that but </S1>
<S2> what's your guess </S2>
<SS> @@ </SS>
<S1> er i would say that er most of those er equivalents i've presented they their (xx) is complete </S1>
<S2> it's a good guess <SS> [@@] </SS> [@so that was guessing@] okay we have exhausted the words of the title so we have to go to something different but maybe @@ let's go to </S2>
<S3> yes , i think the last piece was quite important er the algorithm- algorithmic solvability of of of those questions because because in general (xx) they are , well they can be infinite state and then the question whether whether the language is equal to another language it's , it's even undecidable so so you may have to make like strong restrictions on the number of states and other things but , i would for my part first ask you the question whether , i think that er this er state explosion problem it has been studied quite a while now and er some fifteen years ago i think that er somehow somehow researchers they had a very optimistic view of the solution to to , about the solution to state explosion problem in general , how well do you think that our international scientific community has been able to answer this question </S3>
<S1> well er , a lot of work has been done to study this problem and i think there have been ma- important advances that have been been made in this area so i think er we have come quite a way forward in this in this issue whether that will be enough to to to make the the state state space methods and shall we say an everyday everyday to- tool for engineers that that still remains to be seen so the the question is far from from solved </S1>
<S3> yes , and how about then er of these methods er what do you think about their practical use i mean that the er how largely are these methods applied for instance in industrial er such methods that er that er capable engineers are are are already , erm or or they can use them that they are are able to use them them just in their work in in in the in the industry </S3>
<S1> well i the meth- methods such as these are are used to to some extent already in in the industry er but of course one of the main problems is that their use still requires quite a lot of expertise that they're not for every engineer </S1>
<S3> yeah yes because , because somehow somehow if one one considers the state explosion problem on the complexity vertical the kolmogorov complexity point of view then then one can fairly say that we can always build so complex systems that that the that the state explosion problem to some extent remains unsolvable but but er of course it's important to know what we are (xx) and then then then the er the the most er the properties that are interesting so so in these respects these problems i think one could se- progress can be can be made , this was my </S3>
<S2> okay so maybe in the second round let's have a closer look at some of your contributions and i first turn to the the semantics . and so in your first paper on semantics your goal is to preserve at a global level livelocks or or divergences by the way did you see a difference between livelocks and divergences or do you use both words in the same meaning </S2>
<S1> er well i don't make that distinction i i use those both words for the same meaning </S1>
<S2> do some people make a difference between the two </S2>
<S1> er yes i have , i have seen some people who make a a distinction for example that er a livelock would be a divergence that cannot be exited or something like that but yeah i've not made that distinction </S1>
<S2> yes so so right divergence is just a loop for internal actions and livelock could be a loop within the possible and and and livelock would be would be such a loop without any exits <S1> mhm </S1> i think both are reasonable but anyway that's just er the use of words but er compared to this erm (invariant) you wanted at a global level to be able to to to check livelocks you know implies that your semantics you know has to include traces er divergence traces and eventually divergent traces right that's the <S1> yes </S1> three things you check in your equivalence , er the the thing i was worrying about is that okay this is one formulation of the equivalence but since you prove that it's it's the weakest congruence you know which preserves the the divergent divergences at the global level and compatible with concurrent composition and further along you don't even need hiding to or you have hiding but not as does not make a difference right so or is that correct at all correct </S2>
<S1> mhm er . you need hiding for the general infinite case </S1>
<S2> in the finite case it is it's </S2>
<S1> you don't need hiding </S1>
<S2> right . so is there , there's only one possible weakest congruence it's a unique <S1> [yes] </S1> [equivalence] but what are the other ways of formulating this equivalence , in the sense here you formulated in the sort of semantical way , that would it be possible to maybe formulate it as er an equivalence you know on the structure of the the processes to label transition systems the same way that for instance er observation equivalence is defined </S2>
<S1> erm </S1>
<S2> so so what i'm saying is this is a semantical definition now what i'm asking is really what does this mean if i look at you know labelled transition systems </S2>
<S1> well these are semantical sets are of course mappings from an LTS <S2>  mhm </S2> to these these sets so , well in a way i i'm directly (xx) look at the the structure of the LTS although it's not given so so directly in terms of the structure such as er a bisimulation equivalence </S1>
<S2> right n- n- now i understand that that's you know looking at the structure the way bisimulation observation equivalents do erm probably it's going to er give you problems with really getting the weakest congruence <S1> yeah </S1> because by by focusing on the structure you're going to add the the extra information and and you're going to to make yourself a little bit more too restrictive in in or at least if you're making the notion of equivalence rather er strong , but eventually you take er observation equivalence could you extend this in such a way to get the semantics or the equivalence notions which would be a congruence and which would indeed you know satisfy the fact that at a global level you are (xx) preserving </S2>
<S1> er , yeah you can extend the observation equivalence to preserve divergences but of course er it preserves so much more information about the structure of the system that </S1>
<S2> it it it preserves information about the branching structure <S1> yes  </S1> that i agree that's why i say it's not possible to add the weakest equivalence in this notion but but i'm trying to get a er i'm trying to get a feeling of what exactly you know you need to add to to observation equivalence in order to preserve livelocks . so imagine that i don't worry so much about the branching structure but i'm really focusing that the divergence structure , okay , and if i just use observation equivalence well i i i i lose this information <S1> mhm </S1> so maybe you can help me get a intuitive understanding of what i need to add to observation equivalence in order to get a semantics that's going to preserve livelocks </S2>
<S1> well you would have to add the requirement that that that states which can diverge cannot simulate state which do not diverge </S1>
<S2> that will take care of the divergent traces part how about about eventually divergent traces </S2>
<S1> erm . er </S1>
<P:14>
<S2> see what i mean <P:22> so i'm reading i'm reading theorem one on page 80 okay your theorem one says . there's the T-R that's trace div trace that's divergent trace and endi-trace i guess that's eventually divergent traces right <S1> yes </S1> so we're saying okay we use observation equivalence now that takes care of the trace equivalence in the stronger way but it takes care of that . if you say states er a divergent state cannot simulate a non-diverging one that takes care of the divergent trace <S1> mhm </S1> okay and how would how will you take care of the third component </S2>
<S1> erm i suppose we should add some <SIGH> requirement about er infinite sequences of simulation between states , or <P:09> perhaps that simply that the , er infinite sequences of of i mean infinite execution that that represents a a non-divergent infinite or eventually non-divergent infinite trace would be only allowed to simulate the an infinite sequence that also represents a , eventually non-divergent infinite </S1>
<S2> could you formulate something on the the st- the strongly connected components of the systems and and the divergence (theorem) , components that are related or something like that i don't know i'm just [(xx)] </S2>
<S1> [er but if if we allow] the systems well , first of all if we assume that the systems are finite <S2> mhm </S2> then we don't have to take care of the eventually non-divergent infinite traces er then and it suffices to have the , simpler requirement that that the divergent states are only allowed to simulate divergent states [and] </S1>
<S2> [okay so] that that would be enough for finite systems okay yes <P:06> and of course if you're dealing with infinite systems , okay then then my suggestion is not it's not erm , adequate , okay but the reason i'm going in this direction is because from a practical point of view i mean the checking simulation is more efficient than checking the something based on trace equivalence . so so it might be interesting just to be able to say well look we have the semantics which is based on simulation for which we have better algorithms . which is a congruence which has all the right properties it's not the weakest , but in many practical cases it might just work and if you can check equivalence w- with that semantics then you know there's sem- that goes to your semantics </S2>
<S1> yes that is right er divergence preserving observation equivalence would be a </S1>
<S2> so maybe that's a er you know interesting er concept to explore (xx) <S1> mhm mhm </S1> especially if you if you want to make this you know to to use this </S2>
<S1> yes </S1>
<S2> okay </S2>
<P:05>
<S3> yes i </S3>
<S2> i can carry on if you </S2>
<SS> @@ </SS>
<S3> after a moment you can i will still return a bit backwards maybe i was a bit vague in my thoughts here abo- just about the in fact about the the , to return a bit because we have been returning quite a lot up to now <SS> @@ </SS> so so so so you er you are using LTS and and my i myself i would be very interested to model this congruen- congruency on on a on a hierarchical al- on a hierarchical automata for instance and and er and er what what what are the general disadvantages that that you could se- er that you er you can see not to model the congruency on for instance hierarchical automata because because on the other hand i i think that very many times when when we model the system we could we could start from a very simple one and then continue to a me- more complicated one just splitting splitting the system and and and somehow going from upwards to downwards and and and in in er in in er process algebras you mostly go to in in opposite direction and and and this is why i i i would like to know what er what really you think about about have you ever considered hierarchical automata do you know i'm talking about </S3>
<S1> er well , this approach does have a have the feature that it is , it is quite clearly a bottom-up type of construction <S3> yes </S3> that there is no , no , er shall we say direct obvious method by which you could take a a process and and produce components that produce that process so , so , perhaps that is a drawback of this approach but now perhaps it would be possible to to develop some results that would extend this this idea put this approach in in that that direction </S1>
<S3> yes <P:10> okay then then mostly it is so that that when choosing these operations there are er well y- y- you use the parallel composition and then hiding and again for me the , i always always think i think automata er (it way) way and and and then then then you have <SIC> intersectioning </SIC> it i myself always have the idea of intersection and a certa- certain kind of (xx) there and , so i connect in a way the operations and er , have you have you ma- made any research on on on on taking taking in more operations and and then then considering the i mean i mean this composition s- system more more maybe than than only paralle- parallel composition and hiding and and what are those er results possibly possibly (xx) </S3>
<S1> yes er i have i have been doing research on on other other operators than the ones that are that are presented here although that that resu- those results are not presented here and er if i remember correctly all of these results remained more or less the same with the much larger set of [operators] </S1>
<S3> [yeah] okay because then then one really could see that the like from er classical language family theory op- er theory operators would not lack so much and then then one could have some nice connections to to old theories that are nowadays even considered dead by by some some some researchers er , okay okay this was </S3>
<S2> okay . so you have two papers on the topic of of semantics , <S1> yes </S1> now does the second s- subsume the first <S1> er [no] </S1> [since that's] that's you know why would you want to use the the the erm livelock preserving semantics and not any-lock preserving semantics </S2>
<S1> well er , well , it would still give the user the or whoever needs this theory the choice of whether that person wants to er preserve just any-lock or whether for some reason there's a reason to er to preserve the information whether there are divergences or not so er i don't know if there's a a shall we say universal truth in that wha- what what should be preserved but </S1>
<S2> but the- the this is it right that the semantic (during) the second paper here is stronger than the one you've written in the first one </S2>
<S1> er no the semantic in the second paper is weaker than , oh sorry ah , semantic in the second paper is in- incomparable <S2> [incomparable] </S2> [to] to the first </S1>
<S2> you you have the diagram about (what this er , issue) , right and how come it's incomparable , can you can you sort of try to explain why because you think that you know any-lock would imply a a stronger semantics than than just divergent traces it's just that er er yes . so was it surprising that it's incomparable </S2>
<S1> er well , in a sense these are two distinct pieces of information the system , er . can , can either deadlock or diverge but we might not know which , and , mhm </S1>
<P:07>
<S2> so you mean i- is the am i understanding y- you right to say that in the any-lock you don't distinguish between the two types of problems which is deadlock and livelock <S1> yes </S1> and so you get a different results for to get another case where you you are you have livelocks that are distinguished and you know it's that it is a livelock as in other cases so a problem might be a livelock or a deadlock , is that sort of the explanation </S2>
<S1> yeah yes </S1>
<P:05>
<S2> but in practice maybe you'd just be happy to know there is a problem whether it's a deadlock or a livelock <P:07> and if i ask you the same question as i did earlier for the first paper that's another formulation of the semantics of the any-lock case </S2>
<S1> er sorry </S1>
<S2> if i ask you the same question as i did for the the first paper <S1>  mhm </S1> it's let's take er er you know observation equivalence point of view of the semantics what do you need to add to have the any-lock any-lock semantics </S2>
<S1> er yes erm <P:33> i think we well again if we , restrict ourselves to finite systems , then , er if we modify the observation equi- equivalence so that it's the divergent st- state only er simulate divergent states then this would also , be comparable to this this equivalence </S1>
<S2> mhm-hm so that was the that's the same answer as for the first case so you're saying that there you cannot really make the difference between the two because anyway deadlocks are captured by observation er equivalence , and so this sort of the putting together lumping together of deadlocks and livelocks is not possible in that context , is that am i interpreting inte- interpreting quite correctly what you say </S2>
<S1> erm well as far as i can see now yes i , i can't see if there's a difference </S1>
<S2> so how would you explain to someone you know why you should use deadlock semantics </S2>
<S1> well , because it allows er more reduction er in the systems than using some stronger semantics , so </S1>
<S2> right but then from an algorithmic point of view you don't have to do the reductions </S2>
<S1> well shall we say it's an open question but you can use of course any any reduction technique that preserves some equivalence that is stronger than this but </S1>
<S2> because as far as i know the the the techniques used for actual reduction are all based on simulation algorithms right </S2>
<S1> yes but they they don't necessarily preserve the branching structure of systems so that can be , er , sort of abstracted away at that level so , erm . this is still a , well shall we say it (xx) strong semantics this is a very weak semantics </S1>
<S2> (i know) certainly i'm giving you a maybe somewhat of a hard time but <S1> @@ </S1> i think that the @@ that's the code of the opponent or of the the role of the opponent first and i think you know the the if i (xx) you such hard times it's because there's lots of material in your thesis and lots of of good work so i want to make that clear also to to everyone and i think independently of the practical aspects of of you know how you do it it's important to know the basic facts the the scientific you know er basis of what you're doing and even though if you decide in practice to do something different because you get a better algorithm a thesis having a contribution like yours which gives a reference to really what you need is important . okay . so how about turning to fairness <P:13> you know <COUGH> , fairness has been er used quite extensively and er as you probably know i've worked a fair amount on temporal logic er in my research and when you're dealing with temporal logic you know fairness is not really a problem because you can express it quite naturally in the language , so why is it such a problem in in process algebra </S2>
<S1> well i think it's a problem because er of the compositionality of this approach er so it in a sense fairness is often a global property of the system or it's er presents itself at the at the behaviour at the global level but if we er make a fairness assumption concerning a single component in the system and this this component interacts with the other components then er the way that the other components interact with this component and may not er allow this component to do do just anything this component likes it er this essentially can confuse the the idea of of fairness in this system , so , it's a i think the problem is is the compositionality and and interaction </S1>
<S2> but , it , is fairness something local or something global or can it be both </S2>
<S1> erm yes </S1>
<S2> yes <SS> @@ </SS> it was two options yes to which one </S2>
<S1> er well . mhm , well in some cases the fairness may represent something that is decided on the local level but at other times it it can refer to something that is global that er for example affects the progress of of all the processes in the system , so . erm in ts- to some extent it can be both but it has the potential of being a global property </S1>
<S2> okay let's take a erm an example okay we've been dealing with communication protocols and there's clearly a fairness assumption necessary with (xx) the channels right the fact that the channels do not produce messages indefinitely . now , i think that there's a local requirement <S1> mhm </S1> . and . you say well local requirements can be sort of made erm , er well un- un- impossible when you compose a system <S1> yes </S1> but then i'm i'm wondering if if that the notion of fairness er to present as local is really local . let me make my my thoughts more precise erm , my point of view a fairness requirements on the components is something that should only constrain the internal choices of that component . and hence not be sensitive to composition with other components . and actually you have a a definition i think of s- somewhat in that direction it's on page 139 in your thesis it's definition 22 <S1> yes </S1> and you're talking about you know fairness constraints which are compatible with the LTS <S1> yes </S1> . now , does this definition that you give imply indeed that if the fairness requirement is compatible with an LTS then you can sort of make the fairness requirement true just by op- by making internal choices </S2>
<S1> yes yes i think what you said er , er quite clearly expresses the idea that i had that er the component alone must be able to to er to implement that fairness requirement that one way or the other it can internally internally behave in a way that that <S2> [mhm] </S2> [complies] with that fairness requirement regardless of the environment </S1>
<S2> i mean the the reason i'm asking this is that quite a few years ago i had a paper with these erm <NAME> and <NAME> on realisable specifications and , part of the results of this paper (are same here) imagine you have a system represented by LTS and you have the the requirements like a type of temporal formula when is this requirement realisable and realisable means that you can sort of find an implementation of the system so another LTS which is related to the original by implementation relation such that it satisfies the requirements , and basically it means satisfactory (xx) including some internal choices and what i was wondering is was that whether the notion given in definition 22 of an er LTS compatible with the fairness constraint was indeed something identical or s- at least very similar to that , in a sense could you formulate definition 22 by saying erm an LTS is compatible with the fairness constraints if there is some implementation of the LTS so something which is the er related by the the the er implementation relation to the LTS that satisfies the fairness requirement </S2>
<S1> well </S1>
<S2> (xx) </S2>
<S1> the way i see it it it in a sense er demands a bit more that it demands that that this fairness requirement is implementable in a way that is er in a sense er independent of the behaviour of the environment that this fairness assumption must be implementable no matter how the environment behaves <S2> mhm-hm </S2> so it is a similar idea but erm in this compositional setting we we perhaps er demand even something more </S1>
<S2> okay i i i don't quite understand your answer you see what is is your notion stronger than the one i've presented or is it the other way round </S2>
<S1> erm . well i i don't know the details of the of the notion you were referring to but [my idea was that] </S1>
<S2> [well er can we can we define it] i mean let's let's think about it for erm a minute okay , you have an LTS now you have a semantics of your LTS <S1> yes </S1> and since you're specialist in semantics i'll (xx) semantics , now your semantics (is going to be) implementation relation right er that's saying equality of the traces or the divergency or whatever y- it's inclusion right , i'm saying okay i'll give you the formal definition an LTS is compatible with fairness constraints , if there is some implementation of the LTS that means another LTS (N prime) which implements N and that satisfies the fairness constraints </S2>
<S1> mhm well , in this case i would say that this this is a stronger requirement it demands more than just , being able to implement it </S1>
<S2> so your requirement is stronger than the possibility to implement it <S1> yes </S1> why </S2>
<S1> well , er because the , er , LTS has to furthermore be such that er er . any any behaviour by the environment does not er , er . destroy this fairness assumption that environment cannot block actions in a way that . that would make it impossible to , to implement this fairness assumption </S1>
<S2> right but then it's in my definition it's the same thing , because if i can implement it by just choosing between internal actions , then i can realise the fairness requirement independently what the environment does </S2>
<S1> yes if you can implement it by using just internal actions but er well </S1>
<S2> then the question is what is the corresponding semantics to doing this </S2>
<S1> mhm </S1>
<S2> you see what i mean , here we have this this problem of implementing as i say but my intuitive notion is implementing by choosing between internal actions <S1> yes </S1> and i guess my question to you now is that in the semantics you've studied is there semantics that corresponds to this </S2>
<S1> mhm <P:06> well </S1>
<S2> i i feel that that's you know er something like like fairness semantics basically to to give you something similar right i mean there's no there's no operations , so they don't need a congruence . i s- wou- wou- would that be the case that's in the fairness semantics you have fairer traces they tell you whether you whether you if if that implementation that you just (showed me) that's something that has less failures than the the specification </S2>
<S1> mhm-hm , well </S1>
<S2> now if i implement by just putting internal choices i'm going to have less failures </S2>
<S1> yes er , if well if the process is such that you can er implement the fairness requirement just making er internal choices er by using invisible actions then then that process is compatible in the sense which is defined here <S2> mhm-hm </S2> with the fairness requirement </S1>
<S2> but your requirement is stronger </S2>
<S1> well . in the sense that if you would implement the fairness requirement in in some other way other than just by using the the internal actions </S1>
<S2> but how can you do that </S2>
<S1> well er , well you cannot necessarily do it if you want to to remain comp- to be compatible with the </S1>
<S2> okay , basically what i'm trying to get to is that , is it possible to have indeed something which is compatible and not implementable in the sense i've defined </S2>
<S1> mhm <P:22> well mhm </S1>
<P:05>
<S2> well we can take an example . i mean the the typical example is (i'll be using a topic) which goes something like this okay <DRAWS ON BLACKBOARD> imagine i have a transition system that's like this A-B and i have a fairness requirement always eventually A or something like that but this would not be realisable <S1> mhm </S1> and i guess it would not be compatible <S1> yes , that's right </S1> okay now of course if you have internal choices <DRAWS ON BLACKBOARD> then it becomes realisable <S1> yes </S1> and it also becomes compatible <S1> yes </S1> do you have an example which shows that compatible is not realisable or the other way around </S2>
<S1> well if you mean by reali- realisable that it's realisable by using the internal actions then then i would say that it's much the same but of course even in the left-most case it is , it is , er </S1>
<S2> er let me put this rephrase the question otherwise take take the left picture <S1> yes </S1> is there a fairness constraints compatible with this </S2>
<S1> no well er you mean for example er <S2> (xx) </S2> infinite often A implies infinite often B </S1>
<S2> something like that i mean the fr- i mean the er along with the fairness constraints you can naturally think about for this this system you know are there any s- would any fairness constraint be compatible as as far as i see no but but er </S2>
<S1> no er that that is not compatible with that that system but er if i take the word implementable then of course it would be implementable in that sense that i can transform that to a to a process that does fulfil that </S1>
<S2> but the implementable with respect to which semantics . <S1> [yes er] </S1> [if you if you] implement if you (xx) some implementation then you have to preserve some semantics </S2>
<S1> yes well you could well at least you could preserve all traces er and implement that , [because] </S1>
<S2> [traces] yes if you just look at traces of course but but erm i guess a lot of your work is is devoted to show to f- the fact that traces are not sufficient here because if you compose and this is a local requirement i mean the components then you wanted to be you want to be able to compose and so trace semantics is not is not sufficient <S1> mhm </S1> well i think we've probably exhausted the the the topic that's maybe if you know if you if you're looking for things to investigate to s- look at the the relation between this notion and the fact that erm a fairness constraint is in some sense implementable for the component <S1> yes </S1> because the (xx) you're developing is that you know i think fairness constraints in some ways are always local either they're local to components or they appear on the global point once you've done the composition you say well in the composed component things happened in a sort of fair way but then again it appears like you know set of constraint on the internal choices , but that at that time it's a different level <S1> mhm yes </S1> so , some ways this leads me to to another you know sort of question i have concerning the way you handle fairness because , i- i- it's , somehow strange to to handle fairness which is expressed you know on visible events , and is jus- is really a constraint on internal events . and that maybe explains why the topic is difficult . and why it it pre- see when you're dealing with temporal logic you know usually what you're doing is dealing with a global model . and then you have the full information and expressing the fairness constraints is is (xx) <S1> mhm </S1> in process algebra you're hiding things and so you quickly (arrive at) the problem that you have to to express fairness constraints on things that are hidden and of course that becomes impossible . so another idea that i would suggest is that when you're looking at er fairness constraints take a local fairness constraints okay well let's say you have to do A infinite often or B infinite often or whatever well , if you just look at external events , then you go to usually do reductions that are going to make it impossible to represent this , so maybe you need to to er you know when you're doing your reductions keep more state information to make it possible to still express with fairness requirements . <S1> [yes] </S1> [but anyway] that's just a thought on another difficult topic . i can carry on but i don't want to , keep the floor (forbidden) with the [(xx)] </S2>
<S4> [maybe maybe we should] , maybe we should give <NAME S3> a chance for some er </S4>
<S2> yes that's why i'm stopping @@ </S2>
<SS> @@ </SS>
<S4> yes </S4>
<S3> okay so so yes this conversation it was very interesting but er still i want to return return to the first chapter to just to say some few words about , well then er basically i have an education in in mathematics and and i have to admit that then that er when , i appreciate a lot of these results that are , in the semantics papers what you (sent out) they are very very sharply and and cleverly cleverly written and expressed and then even if we are in the situation that we do not know anything or or know well let's say that the questions began hard to solve , it's er a problem in the (edge) but but when when some borders to the theory are given given given with the situations as as as you have been doing so so i think it somehow it somehow . mhm gives really really boundaries to the problematics that we are we are considering and and they are important from from that point of view i mean mathematically and , and theoretically but then <P:15> yes okay if we are still still going to these er <P:10> congruences so so <P:06> so so for instance in in the first paper there is this proposition 11 which says that where you prove that er that er when you have a pro- a set of er process operators and and equivalence and then you define the relation <P:08> in the in the process context then then you er you er you you have a congruence that preve- preserves the se- the relation do you find this er this er [proposition er hard to hard to prove] <S4> <FOREIGN> [sivu 34,siinä johdannossa] ,sivu 34 </FOREIGN> </S4> okay so it is er perfect for (xx) </S3>
<P:05>
<S1> mhm sorry er [what was the] </S1>
<S3> [okay the question is] that er that you have proved that er weakest cong- er congruence always exists <S1> yes </S1> and was it er ha- er hard to prove er this er this er did you er to find a proof for the proposition </S3>
<S1> erm well <DISC CHANGE> in my mind why that is <S3>  yeah </S3> that is the case so , it was not awfully hard but quite quite interesting to work out the [except except proving that] </S1>
<S3> [yes because the from er yeah] er of course from practical point of view and you find the weakest congruences itself er just to find it it is enough from on the other hand theoretical point of view that they exist this is an quite an important issue and and and when i first first looked at the theorem to my my my my mind for for algebraic to i- well i had the algebraic approach in my mind because because to really really if you have a have a congruence that er you have a relation that is a part of an er subset of another relation and and then then it's possible to it's quite generally possible to prove that this con- congruence always exists and and then an- another question , concerns these er process contexts that you are defining in here i again i find it very , well very very nice for me to read the text because of your er your sharp er constructions but but er but you you you you have a notion of process context and er and er then you are using it i think only in the in fact in the proof of the proposition 11 and i would like to ask you is this er process context necessary at all i i i i mean er a- as a concept because because normally if you you start to start to be in the so-called er well-formed formula formulas you could i think er quite easily begin begin as it is becoming in in in in process algebra from the basic elements and and then continue to inductively to to define the concept and er somehow i feel that this er this er process context er con- er , concept could be left out totally what do you think </S3>
<S1> mhm perhaps er but i i found it useful for the definition of of congruence property because er you have to somehow erm quantify over the set of contexts and over different sets of contexts because the sets set of contexts depends on on which operators you are using so , i did did find it useful to [define the concept] </S1>
<S3> [okay but yeah] but did you first be- for instance take only a or a arbitrary set of operators and then then start this inductive constructions so so i think you should get all the then all the all these process contexts by the with the </S3>
<S1> yes yes you could do that yes definitely <S3> mhm </S3> so this is mainly just a a tool in in helping the definition of the congruence property [er in] </S1>
<S3> [okay okay] okay , yes okay this is i have at this stage i don't have anything else </S3>
<S2> okay so that was very (xx) maybe kind of few last questions again on on fairness and the way you model fairness , well the way you model fairness is by introducing er infinite states components . and if i look picture on page 137 er it's a very pretty picture . er i don't know how you managed to draw that @although@ that is very nice of course there's dots in the picture , i guess the dots mean it carries on its infi- infinite states er <S1> yes </S1> now my question is you know do you really need this because you know later you talk about büchi automata and you know that one way to model fairness , is you know to have a finite state system with the constraint on different behaviours in the form of a büchi condition or (operated) condition the (evaded) condition or (xx) condition whatever <S1> yes </S1> and my question here is you know why didn't you immediately use you know components with let's say büchi (xx) conditions </S2>
<S1> yes that's a very good question er </S1>
<S2> i try to ask good questions </S2>
<SS> @@ </SS>
<S1> er , er , what i wanted was to in a sense er not make changes to the formalism er so in a sense keep everything same just use the ordinary LTS formalism (xx) very simple semantics and er cannot be a lot of argument what it what it means for an LTS to behave so in this way by using these infinite er LTS's and parallel composition with these i was able to maintain that that simple , er LTS formalism er whe- if we start to use er , other kinds of of of restrictions on directly on the finite system such as büchi automata we can er , end up with problematic situations where it might be difficult to interpret how the system behaves for example if the the büchi automaton might be in a state where you cannot reach a accepting state and it's then somehow difficult to interpret the semantics of how that system should behave and that kind of si- situation can come out of er for example parallel composition with other other processes even if if there's no problem in the original processes <S2> [and] </S2> [so] in this way i </S1>
<S2> maybe not if you dealing with realisable systems </S2>
<S1> erm perhaps @i@ <S2> @@ </S2> couldn't say immediately but <S2> [(xx)] </S2> [there are at least some some] restriction there [(xx)] </S1>
<S2> [typically of course] i agree with you if you if you add büchi conditions to this component and you compose (xx) büchi conditions <S1> yes  </S1> but maybe if your the büchi conditions are in the same ways as your fairness requirements compatible or realisable that's the idea behind it , then you avoid that difficulty </S2>
<S1> yes it might be possible to develop a theory on that basis but on the other hand you might use this theory as a as a sort of background for that theory or you could use this model and then show how how those büchi er automata or LTS's are used to represent <S2> mhm </S2> er certain infinite ordinary LTS's so i think in that way it would be possible to still maintain the the the simple straightforward formalism and perhaps still have the benefits that you have [(xx)] </S1>
<S2> [yes that's a good] idea basically we just view the the the transition system with büchi conditions as a representation and and this has to do with semantics or something like that <S1> yes </S1> which makes sense yes <S1> mhm </S1> it's probably a safe way to do <S1> yes </S1> okay </S2>
<S4> uh-huh <P:06> are you both ready , we still have time for questions if you have still , er </S4>
<S2> i think we have discussed the questions er i don't think the goal is to exhaust er @the candidate@ so </S2>
<S4> there's there's no obligation to continue but if you feel that there is still some issue that needs to be discussed </S4>
<S2> i think we've covered a lot of different topics and </S2>
<S4> so <NAME S2> is happy with questions and <NAME S3> you still have questions </S4>
<S3> no i'm er satisfied </S3>
<S4> okay then i think it's er . erm , yes </S4>
<S3> yes so . so i think it's er , time to read our final statement of <NAME S1>'s thesis weakest congruences fairness and compositional process-algebraic veric- verification , and this is as follows <READING ALOUD> the author of the thesis has made a remarkable contribution to the difficult and largely studied verification theory of concurrent and reactive systems , the theoretical results are achieved by applying skilfully and soundly a highly theoretical mathematical apparatus which to great extent is developed by <NAME S1> himself , main part of the results have been already been published on high-level international forum undoubtly the whole work will be positively accepted by the internation- national research community , to pick up some pa- particularly impressive scientific outcomes one can mention the elegant weakest congruence results concerning the livelock and any-lock preserving equivalences modelling of fairness properties before this this subject was rarely studied in the context of process algebras and applicational theory developed to n- to non-triva- trivial communication protocol case studies , <NAME S1>'s work is written in fluent english and it's is particularly precise and error free the mathematical reasoning is correct and meticulous the author shows bright scientific intellect and is indisputably capable to independent research work this thesis clearly exceeds the standards of a normal doctoral dissertation it of of its own part strengthens the reputation of tampere university of technology as a high level interna- national academic research centre , the candidate has with expertise defended his thesis during this examination we warmly recommend that the work of <NAME S1> is accepted as a thesis for the degree of doctor of technology </READING ALOUD> </S3>
