Formal Semantics for Protocols

Transcript

thank you thank you ladies and gentleman I'm the last speaker I'm the only thing between all of you and a drink so I'll try to be fast thank you for inviting me I'm going to talk at a very high level about some very abstract stuff in another part of computer science which I think has relevance but probably not immediate relevance so I'm going to throw in some ideas and take with them as oh do with them what you will they they may not be relevant for a while so starting with the idea that shared Ledger's are just databases with a communication protocol it made me think that there's been lots

of work most people don't know about it a lot of work on communication protocols between autonomous intelligent agents agents if you're not aware are just objects with attitude objects that have the capability to decide for themselves whether they whether or not they will execute when invoked the goal of this research has been trying to automate communications between software agents so having automated dialogues between autonomous agents the status of that work it's still ongoing the statuses that we understand well different types of dialogues drawing on work in the philosophy of language in the philosophy of argumentation we also especially understand dialogues about beliefs their

dialogues about facts dialogues such as where one agent tries to persuade another agent of something a dialogue where agents collectively try and resolve a factual question we understand those dialogues very well and we can automate most of them we can automate negotiations in the case of simple negotiations got more complex negotiations by simple I mean things where you can define the objects of the negotiation very easily for for example negotiations over the price of something for a vote for a well defined commodity or a well defined object we can automate those very well we don't however yet understand dialogues over actions and the fundamental reason for this in my

opinion is that the philosophers have spent something like two and a half thousand years studying beliefs and only a little bit of that time studying actions we don't have good theories only recently have we started to have theories about intentionality and intentions and and their relationship to actions so therefore we don't understand dialogues over actions because we don't understand actions how's that relevant well in computer protocols we have utterances things are said messages are sent in computer protocols these utterances are a means of communication either between the people behind the programs or the programs themselves in the case of agents so linguistics is is relevant here that human natural

language linguistics is relevant because of communications but if their computer protocols then they will be defined or they'll have a defined syntax hopefully machine readable it will be formal and therefore logic is relevant mathematical logic in particular protocols computer protocols with utterances have the have may be viewed in another way and that is that the utterances themselves aim to change the state of some system so a piece of a message being sent generally has the purpose that it wants some state change or it tends to create some state change so we might imagine and we can imagine utterances as being commands in some programming language some is in the

case of suffragettes the agent is intending to do something intending to to change the opinion of some other agent or intending to pass some factual information so of relevance if you view it this way of relevance is program language theory the theory of programming languages in particular the formal semantics of programming languages so because of those three different ways of viewing utterances in protocols communication protocols we have lots of different techniques to come to use and one of those techniques comes from all three of them as that it's the concept of semantics but all three disciplines linguistics logic and program language theory use that word semantics in different ways in this field in agent communications we use it

in all those ways if we think about occurrences on the blockchain then the blockchain initially as we all know was a record of Bitcoin and still is a ret court record of Bitcoin transactions but in the last year perhaps the last six months even there's been a transformation in how people view those utterances so if we're recording Bitcoin transactions then we can easily record transactions in any currency people quickly realize that we could record transactions of any exchange of assets doesn't have to be currency then they realize we can record any information and then you people have started to realize just recently we can record promises and commitments to future action to actions so not just information about facts about the world

but actions about our intentions or the intentions of some entity and then we can have we can use the these ideas just really jur as a way to enable multiple parties to make decisions so where there's an action that requires two or more parties to act jointly we just saw an example in the previous couple of talks then this is a distributed idea or the blockchain idea is a very powerful web enabling that just just as an aside perhaps the most crucial example of actions that require multiple parties to act is the launch of nuclear missiles you need to have at least two people turn the key and those two people must be more than an arm's length away from

one another so that one can't force the other to do it okay how might we think about this so we've seen quite a few different layer stack diagrams today and there are many floating around this is the one I like to use two tickets to consider consider this idea at the bottom we have real world events things that happen in the real world real world events and actions above that we have dialogues we can think about them as being separate dialogues about those events and actions so there might be dialogues between humans there might be dialogues between machines for our purposes that matter their dialogues those dialogues and those events at the bottom in the bottom layer end up creating records on some shared some shared database so for

example the blockchain and then we might imagine inference over those records so the inferences might be smart contracts they might be reputation systems they might be some combination of both so if we can separate out the different components like this I think that helps us understand what we're modeling and where where our records being created in what's happening to those records okay so from linguistics I said linguistics was relevant here we talked about in linguists talk about syntax semantics and pragmatics so syntax is the logical form of some utterance so I have a hundred-pound that's an English sentence it has a subject an object in a verb have is the verb and we English grammar exists we have rules about how we

formulate and express sentences linguists are not agreed about the definition of the differences between semantics and pragmatics but one common approach is to say that semantics is the relationship between the syntax on the one hand and real world on the other so whether the statement is true or false for example is a semantic question a question about the meaning of the statement so do I have a hundred-pound well I would if I needed to verify that statement I'd have to show the money or point to a bank account balance that should show that I have that money so semantics is about the relationship between the statement the syntax on the one hand and the reality on the other pragmatics is about anything else

related to the meaning of the statement that's not about the truth or falsity so pragmatics is often about how is a statement correctly used so a statement such as I promised to give you 50 pound that's a promise that has no truth value there's no no sensible way to say that's true or false who knows what what's inside my head you can't verify what's inside my head promise requires we'll see in a moment I promise requires some participation from the from the audience from the person to whom the promise is made and in many situations in many real-world situations the pragmatics the rule under which statements might be made and the rules under which they are turned into commitments become very important

so why do we look at semantics and pragmatics well I thought I might have to justify this but we had a couple of talks today really good talks about formal semantics and formal verification here we're talking about communication protocols in any communication we want the entities that are doing the communicating are their agents or people we want them to have a shared understanding of what they're communicating about that's not necessarily as as easy as I make it sound but we need if there are agent communications the agents involved have to think that meaning the same thing when they make utterances to one another in computer protocols they typically different entities in the system are developed by different development teams so they too need a shared understanding

they need the same hopefully the same shared understanding of what they're saying so this is linguistic semantics what a common meaning for for statements it turns out that having a good formal semantics for communication protocols also helps with the specification design and the coding of those protocols so one of the talks this morning we we heard about formal verification where there's proof by construction so just by doing the design in the appropriate formal language it automatically you could automatically generate the code similar thing happens here we want also to verify properties of protocols so questions like fairness and termination

that the protocol terminates or ends or doesn't end if you don't want that or that no gridlock state comes about so formal verification as in the top two or three talks ago we want that generally we want that for communication protocols as well and if we're going to do automated inferences if we're going to go if I go back to this picture if go to the top layer if we want those inferences at the top layer to be themselves automated then we need a formal semantics typically we need a formal semantics for the protocol so that a machine can read those and make sense of those so quite often there's often a tension between developers on the one hand you just want to go a code and people come along later can us computer scientists to come along later

and say hey do it hey wait a minute you need to you need to formalize what you're doing and people in AI are particularly keen on formalizing because that's how we do automation how we do anything automated in program language theory we talk about semantics as well and there are three main types of semantics so this is I'm just giving you a very brief overview this is a whole subject in itself we talked about axiomatic semantics for in this case our instance so those are the preconditions and the post conditions for each type of utterance there's a common agent language called the FIFA ACL and in the FIFA ACL one agent cannot tell a fact to another agent unless the first agent

believes that fact so the first agent has to believe it to be true this is supposedly to prohibit agents lying to one another but it prevents any negotiation you don't want to give away your price before you start the negotiation so the axiomatic can be quite tricky can be quite subtle to get an operational semantics is basically thinking of the utterances as being commands in some language and that language acts on the state of some big virtual machine the machine doesn't exist in reality but it can it's a conceptual trick to help us understand what the impact of an utterance is and what its impacts its consequences might be so it occurred to me during the talks today that if we have a true global

state if we adopt this policy that we were hearing about earlier in the day about sharding where we have a true global state at the top level but within each shard there might be local states then it will be interesting to see what operational semantics how that would play out because the commands at the local level may not be operated on the global state until they have started to go all the way up and then a denotational semantics is a semantics that map's the syntax to some mathematical objects why do we want to map things to map mathematical objects well one reason is that we've got a couple of thousand years of experience of reasoning about mathematical objects we know how to manage mathematical objects we humans and by doing this we are then able to reason about the

and the formal verification talked about there this afternoon was an example of that one type of mathematical object we have used a lot in agent communications is games particular games so we map utterances to games and study the properties of those Dame's an example of this is with promises so promises require an audience you can't make an effective promise to yourself it makes it philosophers have looked at this and they say it makes no sense so if personname promises to wash the car of person b then there has to be an audience b has to hear this promise or has to learn about this promise there's a concept called up take this in most cultures English in particular a promise doesn't become a

commitment on the person making the promise in this case a commitment only created when B accepts the promise so B says okay yes you can wash my car I accept that promise so the promise in in the jargon of the field is said to be up taken that's taken up by B so notice that the promise was made by person a but the uptake was by person B two parties involved there now if we want to revoke the promise or cancel it then typically in most cultures a promise can only be cancelled by the party who took it up so if I make a promise to wash your car and you say yes please do then I can come to you later and say sorry I don't want to make that promise anymore

so in many social situations I can but there'll be a consequence to me you might no longer trust me you might think I'm not going to take promises from him anymore in legal or legal or financial domains there might be other consequences more severe consequences so this is an example where there's an option about an action there's two parties involved here a and B one is doing the promising a party B can up take it and revoke it at any time and may also have the power tool to say it's fulfilled for some utterances about action there might be three parties involved one party has the power to promise or to make their utterance another party has the power to update and a third party has the power to revoke and quite often with legal

domains that's the situation we have multiple parties involved there might be a regulator involved once a commitment has been made only the regulator can cancel it once a trade is executed on the New York Stock Exchange for example it can be canceled and can be revoked but only the New York Stock Exchange itself can revoke it can cancel it and apparently they do cancel them about one a week under special circumstances so we can represent this particular situation because there's two parties involved we can represent it as a game a two-party game and we can study the properties of that game and that's an example of a denotational semantics so we understand what's going on between those two parties in a particular way that actually helps us with the implementation with coding it so that's

the end thank you