User Manual for MCK. – DRAFT Version 0.0.3
Contents
1. 3 6 Fairness Constraints eee st The Use ot Labels ini Gen Bae m aa a a s den n ee ee 413 4 Examples 4 1 TBe Rebot examiple r lt a b nare gen BE ee ge gee dette neben Hed a 4 2 The Dining Cryptographers Bibliography A Input Script Syntax Joint Protocols and the Environment A 1 1 Environment Resolve clause 00000 A2 Agent Protocols sse i a A EXPressions 4 4 an an an da bee bbe Ahern dd a AA Specifications az AT AA AS ee eee ee li a s n a ii 13 13 14 14 14 15 15 16 17 17 18 18 CONTENTS Common Productions BB BEE AA Aa me ee y 28 Operational Semantics 29 Bl Preprocessing nan died b b Sa deta dee Bal AR A er krk ee El H 30 B 2 Expression Semantics aaao 30 B 3 Agent Protocol Semantics ee 31 B 4 Environment Resolve clause Semantics ee 32 BA RUS a m k A d el di Ss eta 33 Chapter 1 Introduction This manual explains how to use MCK a prototype model checker for temporal and knowledge specifications It assumes some familiarity with the idea of model checking 4 5 9 and temporal and epistemic logics 7 but is otherwise self contained This chapter introduces the general scenario to which the MCK system may be applie2. agent constant String C 1 VarList O VarList Var Var EnvInitCond init_cond Expr EnvFairness fairness KF A 1 1 Environment Resolve clause EnvResolve resolve ResolveBlock ResolveBlock begin ResolveStatement ResolveStatement end 25 26 APPENDIX A INPUT SCRIPT SYNTAX ResolveStatement ResolveBlock if ResolveClause ResolveClause ResolveClauseOtherwise fi if ResolveExpr then ResolveStatement else ResolveStatement skip varid Expr ResolveClause ResolveExpr gt ResolveStatement ResolveClauseOtherwise otherwise gt ResolveStatement ResolveErpr ResolveExpr ResolveExpr Var Constant constant constant ResolveErpr BoolBinOp ResolveExpr neg ResolveExpr C ResolveErpr A 2 Agent Protocols Protocol ProtocolHeader EnvVars LocalVars Block ProtocolHeader protocol String EnvVars C VarDec VarDec 9 LocalVars VarDec LocalVarInitCond Local VarInitCond where all_init Expr Block begin LabelledStatement LabelledStatement end LabelledStatement label Statement Statement Blo
3. m O r m Here the agent uses both its current observation and the current global clock value to determine what it knows Most informative is the synchronous perfect recall view defined by rif m O r 0 O r m Here the agent uses its complete sequence of observations to the current time to determine what it knows For each view x we may define a relation of indistinguishability on points two points r m and r m are said to be indistinghuishable to agent i written r m r m if the agent has the same local state with respect to the view at those two points i e if r m r m Intuitively the set of all points that are indistinguishable from a point r m is the set of all points that the agent considers to be possiblv the current point when using the information capture in that view We may therefore say that agent i knows with respect to view x that a formula holds at a point r m if holds at all points r7 m such that r7 m r m the statement that agent i knows is written as Knows i with the view indicated at the level of the larger formula of which this statement is a part The above definitions suffice to give semantics to the specification langauge of MCK In addition to the knowledge operator just defined there is a varietv of temporal logic operators These are defined in Chapter 3 In order to enable the user to describe the svstem in which a
4. False end 1 neg Robot Halt gt begin position position 1 incpos True end fi if True sensor position 1 True gt sensor position True gt sensor position 1 fi end Knowledge based program specification agrees with the implementation spec_obs_ltl G sensor gt 3 lt gt Knows Robot position in 12 4 Rule out the traces where the environment stops trying to advance fairness incpos The bike handbrake protocol In order to stop moving the robot needs to keep the brake pressed protocol robot sensor observable Pos begin do neg sensor gt 3 skip break gt lt lt Halt gt gt od while True do lt lt Halt gt gt end Figure 4 2 The robot input script 19 10 20 30 40 50 20 CHAPTER 4 EXAMPLES protocol robotbroken agent protocol mck sensor observable Pos begin while neg sensor gt 3 do skip while True do halted lt lt Halt gt gt end Figure 4 3 The modified incorrect robot protocol protocol dc agent protocol mck env paid constant Bool chan left Bool chan right Bool said observable Bool the broadcast variables coin left Bool coin_right Bool paid Bool where all_init begin The enviroment tells us whether we paid or not lt lt paid env_paid read gt gt The agent decides the coin toss to t
5. ResolveClause p 4 for each agent i st Assignment 1 p a o o Assignment in p A p Stenv o Oi sti p p ProgramlTerti ProgramTeat gt p ProgramText ProgramTezti Notes e The order of composing the Environment s and Agents state transformers st doesn t matter as their domains are disjoint e Where there are several assignments in a single action statement the variables in their right hand sides refer to the current state For example in a state where x m True y gt False the action lt Nill Action x y y x gt gives rise to a state where x m False y gt True B 4 1 Runs A run is a sequence of global states p conformant with the overall one step transition relation gt e The initial state of the system is p ProgramTerti ProgramText where p must satisfy all local and global initial constraints and ProgramT eat is the entire program for agent 2 e For each i gt 0 we have with superscripts indicating position in the run i 1 n p ProgramTezt ProgramTerti gt p ProgramTex ProgramText FL
6. Expr Val var i gt let val p var in succ type var val var i let val p var in pred type var val pilf g pi f True A p g True p neg f gt True p var p var pc val val p var vah val gt let val p var in val val V V val valn p p B 3 Agent Protocol Semantics The definition of p ProgramTert 4 RestO f ProgramT ext p Ca Cy Sequencing p C1 Co A Ci Ca If For each alternative 4 p cond True 0 if cond Ci firma Ci Do For each alternative i p cond True 0 cond od 4 Ci do od The p ProgramTert sa RestOf ProgramText relation is the reflexive transitive closure of the above definitions This relation is purposefully non deterministic The definition of p ProgramText a Action Assignment ProgramTezt p ProgramText 5 AK Action Assignment gt ProgramT eat p ProgramText a Action Assignment ProgramT ext We expect p C ma C to terminate for all C and the overall agent relation p ProgramText o A Action Assignment ProgramTezt to not get stuck Define p ProgramTezti ProgramT ext gt n Actioni Assignmentji ProgramTert Actionn Assignment ProgramTezti to be the composite of the individual transitions p ProgramTezxta a Actiona Assignment 4 ProgramTezt i for ea
7. KF AG KF EG KF muvar gfp muvar KF lfp muvar KF Knows constant CK AgentList KF CK KF KFItl is the LTL knowledge specification language KFItl Proposition KFItl BoolBinOp KFU neg KFU KFt 9 F KFH KFItl KFt U x KFH Y int KFU Knows constant CK AgentList CK KFt The basic propositions Proposition Qualified Var Constant Qualified Var Constant Qualified Var Constant Qualified Var elOp Constant Constant RelOp Qualified Var Qualified Var in ConstantList constant 28 APPENDIX A INPUT SCRIPT SYNTAX Qualified Var constant Var AgentList 0 constant constant F LabelList label label F A 5 Common Productions Assignment Var Expr BoolBinOp IN W gt lt gt xor ConstantList T Constant Constant Constant Constant F Constant int constant Type TypeAttr TupeDesc TypeAttr constant observable TypeDesc typename typename U int Y Var varid varid P self int 2 VarDec varid x Type Appendix B Operational Se
8. executed after the agents have decided which action they wish to perform and a new state is generated via their joint action At the moment only actions without arguments are implemented This mechanism is used in the robot example of Section 4 1 12 CHAPTER 2 environment environment name Types zero or more type TypeName0 elements type TypeNameT 1 elements Shared variables zero or more varDec0 Type varDecN Type Agent bindings at least one agent AgentNamel protocol for agent 1 env variables agent AgentNameM protocol for agent M env variables Environment initial conditions optional init_cond boolean expression involving env variables Resolve clause optional resolve begin statements end Specifications at least one lt specification_type gt temporal and knowledge formula Fairness constraints zero or more fairness CTL formula Protocol declarations zero or more can be in a separate file protocol first protocol name env parameters localVar0 Type localVarK Type where boolean expression involving local variables begin statements end THE INPUT LANGUAGE Figure 2 1 The structure of an input script 10 20 30 40 Chapter 3 The Specification Language There are two dimensions to the specif
9. the system Each of the agents performs these actions acccording to a protocol or set of rules which describes the allowable choices of the next action at each point of time The agents have incomplete information about the state of the system their possible information is limited by the fact that they are able to observe only part of the state at each instant of time The MCK system can be applied to the analysis of this type of setting by the use of model checking techniques The input to the MCK system consists of a file or set of files that describe 1 the environment in which the agents operate including e the possible states of the environment e the initial states of the environment e the names of agents operating in this environment e how the agents actions change the state of the environment e optionally a set of fairness conditions which constrain the infinitary behaviour of the system ensuring e g that some agent is not kept waiting forever for a requested event to occur 2 CHAPTER 1 INTRODUCTION 2 the protocol by which each of the named agents chooses their sequence of actions including e the structure of local states maintained by the agent to make such choices and record other useful information e the possible initial values of the agent s local states and e a description of what parts of the state are observable to the agent 3 a number of specification formulas expressing some property o
10. G F M1 left cs M2 trying gt F M2 in_cs protocol mutex env_turnl observable Bool env turn2 Bool in_cs Bool where neg in_cs 30 begin while True do begin while env_turnl True do trying skip Critical section in cs True do in cs skip l in cs gt in_cs False break gt skip od 40 End critical section left_cs lt lt env_turnl write False gt gt lt lt env_turn2 write True gt gt end end 3 5 Knowledge Modalities The knowledge modality is written Knows Agent formula The various semantics for this oper ator were spelt out in Section 1 2 For the clock and observational semantics a common knowledge operator is also available writ ten CK Agent Agent formula formula is common knowledge to the specified agents or CK formula formula is common knowledge to all agents 3 6 Fairness Constraints MCK supports fairness constraints in the manner described in 4 Section 7 and 5 Section 6 3 Briefly a fairness constraint filters the runs of the system by accepting only those along which a given CTL formula is satisfied infinitely often This is explained in more detail in Chapter 1 An example of using a fairness declaration to eliminate undesired runs is shown in Figure 3 2 The constraint fairness A var ensures that the runs that after some finite period of time forevermore have var false are eliminated 16 CHAPTER 3 THE SPECIFICAT
11. ION LANGUAGE environment env agent A while spec_obs AG AF A var fairness A var protocol while var Bool 10 where neg var begin do True var False True gt var True od end Figure 3 2 An example of a CTL specification While it is tempting to try to use labels to specify which branches of if and while should be treated fairlv it is not as straightfoward as one might hope The following section gives details 3 7 The Use of Labels Explication of the semantics of labels requires a distinction to be drawn between state transitions that are enabled versus those which are taken For example when control reaches the following program fragment if True 10 var 0 True 7 11 var 1 l True 12 var 2 fi we have that all branches of the if statement are enabled but only one can be non deterministically taken Concretely the proposition Agent Name label evaluates to True if and only if a statement la belled by label is enabled If there are several statements with the same label then the proposition is true if any of them are enabled The biggest trap with this arrangement is that it is not always adequate for specifying fairness constraints Consider for example the constraint that the middle branch is executed infinitely often It is tempting to write the fairness constraint like so fairness AgentName ll but this merely asserts that the branc
12. L spec obs Figure 3 1 The combinations of temporal and knowledge semantics currently implemented in the model checker 13 14 CHAPTER 3 THE SPECIFICATION LANGUAGE 3 2 Computation Tree Logic Computation Tree Logic is a well known branching time logic used for example in SMV 5 The available operators and an informal semantics are as follows f in all next states f in at least one next state on all paths f until g on at least one path f until g On all paths in some future state f On at least one path in some future state f On all paths in all future states f On at least one path in all future states f An example appears in Figure 3 2 In English the specification might be rendered as in all reachable states there exists a future state where A var is the case The set of reachable states is subject to fairness constraints see below 3 3 u calculus Constructs The calculus adds greatest and least fixed points to the branching time model that CTL uses and can indeed express all unfair CTL constructs Concretely in spec_ obs specifications the following two operators can be used gfp 2 f greatest fixed point of f wrt variable 2 lfp 2 f least fixed point of f wrt variable Z with the constraints that all relational variables such Z used in f fall under an even number of negations and that the specification as a whole is closed with respect to relational variables For exam
13. True x 3 gt False x lt 3 gt True Truncating Arithmetic r 1 gt 4 z 4 gt 0 It is envisaged that other forms of arithmetic will be useful and these will be implemented in the future 2 3 AGENT PROTOCOLS 9 2 3 2 Well tvped expressions As all types are enumerated we have very liberal overloading rules Indeed the type checker simply computes an approximation to what values an expression can take on and ensures it s a subset of Bool in the case of boolean formulas or of the type of the variable being assigned to otherwise In contrast to for example 10 there is enough information in each subexpression to uniquely determine it s type and so no backtracking is required 2 3 3 Statements The imperative language is based on Dijkstra s guarded commands 3 The only substantial deviation from his presentation is the addition of a break branch in a do statement which is executed when the do loop terminates i e when all other conditions are false Why this is important is discussed in more detail in Sections 4 1 and Appendix B Core language Alternatives The non deterministic choice statement has the form if cond cond C otherwise Co fi where each command C is eligible for execution only if the corresponding condition cond evaluates to true in the current state If for all i cond evaluates to false then Co is executed If the otherwise branch is absent then an implicit ot
14. User Manual for MCK DRAFT Version 0 0 3 Peter Gammie and Ron van der Meyden June 18 2003 ji Contents 1 Introduction 1 1 The Model Checking Scenario 1 2 Background Theory ace oe anr BiR vern ab an B dende Ae da dk oa 1 3 Installation and Invocation 2 The Input Language 21 Lexical Structure teo an nn eer eenn ie de AL a BE a a en 2 1 1 Reserved Words 22 Wy pes 001 0400000007 2 9 Agent Protocols noar 6 3 At a eee en eS ee dd BRPEESSLONS bi y b en B an 7 2 3 2 Well tvped expressions 2 2 03 07 Statements rasa ala Brin Be eee ee u het alg 2 9 4 Labels edad eee ar Ki s Beeke li m 24 The Environment a det aa a dea de ls en ei ars 2AM AR Reed a b ja eee eee ee eae bd ad 24 2 Shared Variables 223 Agent Bifidings 2 5 4 4 44 44 4 5 4 4 e Pee ei ih 214 Initial conditions e de E ee aa 2 4 5 Resolution AAA A eee R s p 3 The Specification Language The Propositional Core inicia He o B dende nd EE ALA EEn Bus 2 Computation Tree Logie vun a al al n a L R an se a Bet aen 3 0 gecaleulus Constructs ose we ee ee a 3 4 Linear Temporal Logic 3 5 Knowledge Modalities
15. ansitions which become stuck upon encountering a manifest action p ProgramText a Action Assignment ProgramTezt is the selection phase de termines what action the agent performs in this time step 29 30 APPENDIX B OPERATIONAL SEMANTICS The idea is that each agent executes as much ProgramT ect as possible until it is manifest which action is to be performed at which point the a relation gets stuck The 4 relation takes care of detaching this action and tracking where the agent is up to in its protocol The relation is the synchronous lock step aggregate of all the A agent relations The definitions of these relations are given in Section B 3 Environment Transitions 4 generates a state transformer from the resolve clause given the current state and the actions the agents have performed p ProgramTexti ProgramTeat gt p ProgramTeat ProgramTezti is the overall single step state transformation relation The definitions of these relations are given in Section B 4 B 1 Pre processing A pre processing pass is used to expand derived forms and normalise the programs 1 Append while True do skip to the original program P This ensures all programs generate infinite runs 2 Make all variable names unique by qualifying local variables with agent names 3 Eliminate derived forms using the rules in Sections B 2 and 2 3 3 4 For all if fi statements if present rep
16. ation The program is implemented in Haskell and makes use of extensions only implemented by the Glas gow Haskell Compiler http haskell org ghc It uses David Long s Binary Decision Dia gram package available from CMU http uww 2 cs cmu edu modelcheck bdd html and a Haskell binding of it that should accompany the source distribution See the file INSTALL for detailed installation instructions 1 3 INSTALLATION AND INVOCATION 5 Invocation The mck program accepts the following flags c or counter examples Generate counter examples not fully implemented d Int or debug Int Output BDD debugging info and stats This is not particularly useful for end users e or environment Output the environment information f or formula Output the BDD formulas in human readable form This is not particu larly useful for end users o File or var order File Output the variable order to a file p or protocol Output the pre processed protocol information rlslvl or reorder s w Enable BDD variable re ordering The two methods are sifting and window based sifting see the CMU Long BDD manpage for details s File or set var order File Load variable ordering from a file It expects the filename of an input script to be supplied The program will search the current directory for files matching the names of any protocols that are used in an input script but not defined there See Section 4 2 f
17. ause agents may observe some of the environment variables and use these observations in deciding what to do Note that one agent cannot directly access another agent s local variables this is a syntactically enfored constraint on agent programs Similarly the environment transition function 7 cannot make use of any agent local state Using these components we may now define a global initial state to be a global state se 1 Sn such that se Ic and s 1 for each agent i Moreover we define a global state transition re lation T on global states as follows If there are n agents sTs where s 32 81 8 and 5 5 sh S4 if there is a joint action a a1 0n such that for each agent i a P s is an action that may be selected by agent 778 protocol the state sl T a se is one of the possible outcomes of performing the joint action and for each agent i the state s M s a is the result of updating the protocol state accordingly We may now define the set of runs generated when the agents execute their protocols in the given enviroment as the set of all runs r sg s such that sg is a global initial state and for for each k gt 0 we have sp T sp 1 i e there is a transition from sp to sx 1 and the fairness conditions apo Uf are satisfied i e there exist states 54 Sf where r m sr for infinitely many m and sf af for 0 X lt 1 3 Installation and Invoc
18. ch agent A 1 n This relation is used directly by the resolution relation 32 APPENDIX B OPERATIONAL SEMANTICS Note on why do has a break branch As noted in Section 2 3 3 the protocol language is non standard in that it allows the programmer to specify what happens immediately after all guards evaluate to false in a do construct In Dijkstra s version 3 there is always an implicit skip before the programmer regains control The reason we require continuous control was set out in Section 4 1 A superficially plausible alternative semantics is to try to determine an action which will be enabled once the do loop terminates and execute that Unfortunately this leads to problems Take for example the following program do True gt do False gt lt Action gt od od under these semantics In this case there simply is no action that can be executed between the evaluation of the two guards and so the ma relation must be non terminating Given our constraint that guards should be instantaneously evaluated the most natural thing to do is to add the break branch An alternative solution would be to ban nested looping constructs or require that the first statement in the body of a do statement always produce an action i e be a non looping construct B 4 Environment Resolve clause Semantics The environment s resolution protocol is expressed as a non looping program in a subset of the language used to rep
19. ck if Clause Clause 1 10 otherwise gt LabelledStatement fi do Clause Clause 1 0 otherwise gt LabelledStatement break gt LabelledStatement od if Expr then LabelledStatement else LabelledStatement while Expr do LabelledStatement skip varid gt Expr lt lt Action Assignments gt gt Clause Expr gt LabelledStatement Action constant Var write C Expr Y varid Var read Assignments Assignment Assignment EXPRESSIONS 27 Expressions Expr 5 Constant Var Constant Var Constant Var RelOp Constant Constant RelOp Var Var in ConstantList Var ArithOp int Expr BoolBinOp Expr ArithOp RelOp lt lt gt gt A 4 Specifications EnvSpec spec_clock KFltl spec_obs KF spec obs 161 KFltl spec_pr KFltl KF is the CTL mu calculus knowledge specification language KF Proposition KF BoolBinOp KF neg KF C KF 9 KF EX KF AD KF U KF Y ET KF V KF 7 AF KF EF
20. d Sec tion 1 1 and describes an abstract model that underlies the system Section 1 2 The semantics of the constructs of the MCK systems is most easily understood with repsect to this model The MCK system itself uses a more concrete syntax designed to facilitate the encoding of examples The remainder of the manual describes this concrete syntax and its associated semantics Chap ter 2 discusses the language used to model a scenario in MCK The language used to describe the specifications that MCK checks in these scenarios is discussed in Chapter 3 Chapter 4 presents a number of examples that can be analysed using the system The description of syntax and seman tics in these chapters is semi formal a formal abstract syntax for the inputs to MCK is presented in Appendix A and Appendix B provides a formal operational semantics for MCK programs 1 1 The Model Checking Scenario The overall scenario that can be analysed using the system has the following general structure We consider that we are modelling a situation where some number of agents which might be players in a game actors in an economic setting or processes programs or components in a computational setting interact in the context of an environment A state of the system consists of a state of the environment together with a local state for each of the agents The agents have the capacity to perform certain actions in this environment The effect of actions is to change the state of
21. e user to check the model by navigating through executions of the scenario and presenting counterexamples when specification formulas are found to be false 1 2 Background Theory This section describes an abstract mathematical model that underlies the MCK system It is closely related to models used in works including 12 13 14 which present some of the algorithms and data structures that underlie the analysis performed by the MCK system These papers themselves use a variety of formal modellings and the differences between these papers and the model described here is largely a matter of mathematical presentation The remainder of the manual provides a more concrete syntax and semantics for the model developed here 1 2 BACKGROUND THEORY 3 We first present an abstract view of the semantics of MCK programs that is adequate from the point of view of the main constructs of the specification language used in MCK From this perspective as svstem comprised of a set of interacting agents is at each point of time in some global state Write G for the set of all possible global states of the svstem A run is a possible history of such states and can be modelled by an infinite sequence r sg 81 32 where each sk G We write r m for the m th state in this sequence The behaviour of a system is typically non deterministic as agents may have a choice of what actions to perform at any given point of time and the environment may also m
22. f the way that the agent s knowledge evolves over time Both the possible state changes described in the environment and the agents choices of action may be non deterministic which means that the system may evolve over time in a potentially large number of different ways The output produced by the MCK system is for each of the specification formulas an answer to the question of whether for the scenario modelled the agents knowledge is in fact guaranteed to evolve according to the specification for every possible evolution of the system The MCK system currently allows several different approaches to the description of the tem poral and epistemic aspects of the specification formulas In the epistemic dimension agents may use their observations in a variety of ways to determine what they know One way the observa tional interpretation of knowledge is to make inferences about the state based just on their latest observation Another way the clock interpretation of knowledge permitting more information to be extracted is to compute knowledge using both the current observation and the current clock value Finally even more information can be extracted by the agent if it uses a complete record of all its observations to date to determine what it knows this is called the synchronous perfect recall interpretation of knowledge In the temporal dimension the specification formulas may describe the evolution of the system along a single com
23. formula is to be checked MCK provides a svstems modelling language that consists of two parts The set of runs of a system is taken to be generated by the agents each running a protocol by which they choose actions available to them in a given environment The global states G are made up of two components a state of the environment and a protocol state for each of the agents Abstractly we model the environment as a finite state transition system with the transitions labelled by the agents actions For each agent 1 n let A be a set of actions associated with agent i A joint action consist of an action for each agent i e the set of joint actions is the cartesian product A A x x An Define a finite environment for n agents to be a tuple of the form Se Le T Q fo Oz Where the components are as follows 1 Se is a finite set of states of the environment Concretely these are given in MCK by specifying a set of typed variables 2 1 is a subset of Se representing the possible initial states of the environment Concretely 4 CHAPTER 1 INFRODUCTION this is specified in MCK by a constraint on the environment variables 3 Te is a function mapping each joint action a A to a nondeterministic state transition function Sc P S Intuitively when the joint action a is performed in the state s the resulting state of the environment is one of the states in T a s Concretely this is given i
24. h is enabled infinitely often and does not rule out runs where it is never actually taken The simplest solution is to add an auxiliary variable that tracks when a branch is taken and re formulate the constraint in terms of it fairness var Chapter 4 Examples This chapter illustrates the kinds of properties the model checker can verify and some of the subtleties that may arise when formalising a system 4 1 The Robot example PAN R goal region 0 1 Figure 4 1 Autonomous Robot This example is taken from 1 To quote the summation found in 6 A robot travels along an endless corridor which in this example is identified with the natural numbers The robot starts at 0 and has the goal of stopping in the goal region 2 3 4 To judge when to stop the robot has a sensor that reads the current position See Figure 4 1 Unfortunately the sensor is inaccurate the readings may be wrong by at most 1 The only action the robot can actively take is halting the effect of which is instantaneous stopping Unless this action is taken the robot may move by steps of length 1 to higher numbers Unless it has taken its halting action it is beyond it control whether it moves in a step A sound and complete solution to this problem is to do nothing while the sensor has a value of less than 3 and halt as soon as it takes on a value of 3 or more The naive solution of halting iff the sensor reads 3 is sound but not complete In orde
25. he concrete syntax can be found in Section A 1 Lexically the type name and elements are Constants and elements do not have to have a unique type Note that this ad hoc overloading of constants restricts the allowable structure of expressions see Sections 2 3 1 and 8 CHAPTER 2 THE INPUT LANGUAGE The canonical ordering on the elements is the textual order in which they are defined For example in the context of the declarations type Int3 0 7 x Int3 y Int3 init_cond x 3 y 4 we have z y in all initial states The only primitive pre defined type is Bool which behaves as if it were defined like so type Bool False True Arrays Environment variables can be given an array type using the standard C syntax Their main utility is in abstracting a protocol from the concrete number of agents present in a given scenario See Section 4 2 for an example of where this is useful 2 3 Agent Protocols A protocol defines an agent s behaviour and as such is a program written in an imperative language reminiscent of Dijkstra s guarded commands 3 The basic structure of such definitions is illustrated in Figure 2 1 and is more formally spelt out in Section A 2 In essence a protocol has a name a list of environment parameters a list of local variables an initial condition and a statement block As such it looks like a C or Pascal style function definition and indeed it behaves as if the env
26. he right if True gt coin_right True True gt coin_right False fi lt lt chan right write coin right gt gt lt lt coin_left chan left read gt gt lt lt _said self write coin_left xor coin_right xor paid gt gt end Figure 4 4 The Dining Cryptographers protocol file dc agent protocol mck 10 20 4 2 THE DINING CRYPTOGRAPHERS 21 environment dining_cryptographers paid constant Bool 3 chan Bool 3 said Bool 3 Agents are numbered in the order they appear agent Cl dc agent protocol mck paid 0l chan 0 chan 1 said agent C2 dc agent protocol mck paid 1 chan 1 chan 2 said agent C3 dc agent protocol mck paid 2 chan 2 chan 0 said 10 init_cond neg paid 0 neg paid 1 neg paid 2 paid 0 neg paid 1 neg paid 2 neg paid 0 paid 1 N neg paid 1 meg paid 0 AA neg paid 1 paid 2 This talks about the knowledge of the first agent spec_pr X 6 neg paid 0 gt Knows C1 neg paid 0 A neg paid 1 20 neg paid 2 Knows C1 paid 1 paid 2 A neg Knows C1 paid 1 neg Knows C1 paid 2 Figure 4 5 The Dining Cryptographers environment file dcenv mck 22 CHAPTER 4 EXAMPLES Bibliography 10 11 12 13 14 Ronen I Brafman Jean Claude Latombe Yoram Moses and Yoav Shoham Applications of a logic
27. herwise skip is introduced This construct consumes no time steps Repetition The non deterministic iteration statement has the form do cond C cond C otherwise gt Co break C Jod where each command C is eligible for execution only if it s corresponding condition cond evaluates to true in the current state a process which is repeated until all conditions evaluate to false At this time the Cy statement is executed if the break branch is present otherwise the system implicitly executes the skip command This construct consumes no time steps Sequential Composition An arbitrary number of statements Ci C to be executed in se quence can be aggregated by writing begin Ci Cn end This construct consumes no time steps Actions An action captures the essence of how an agent can contribute to a state update it both sends a signal to the environment and specifies how the local state of the agent should change This select resolve model is detailed in the introduction Chapter 1 and the corresponding environment declarations are described in Section 2 4 5 An action has one of two forms lt lt Action gt gt lt lt Action vari expri ara expry gt gt Note that var var must be distinct local variables In the future it is expected that the implementation will support actions parameterised by variables and constants In the interim shared variables primitives a
28. ication language the temporal logic semantics leading X LTL CTL and the knowledge semantics observational clock perfect recall The combina tions of the two that are implemented are shown in Figure 3 1 and the various operators are described in the following sections Note that the leading X semantics simply signifies taking n steps before evaluating the rest of the formula which must not contain temporal operators 3 1 The Propositional Core Basic propositions in this language can be formed in several ways Boolean variables can be used directly environment variables are denoted by their names and agent variables can be accessed as AgentName variable Note that labels also use this syntax see Section 3 7 for details Equality between a variable of arbitrary type and an element of that type is denoted as var Constant The negation of this is written variable Constant Relational expressions between variables and constants are permissible for example var gt 3 4 var and var in 3 5 7 are all valid propositions provided var is given a type that has at least 3 4 5 7 as elements The usual boolean connectives Section A 5 can be used to combine propositions Note the absence of arithmetic operations the form in which they can appear in expressions Section 2 3 1 is significantly less useful in specifications Observational Perfect Recall leading X spec_obs spec clock spec pr CTL spec obs LT
29. ironment parameters are passed by value This is spelt out in more detail in the following section on expressions The local variables are simply identifier type pairs and the initial condition is either a boolean expression mentioning only local variables or the special form all_init which indicates that all variables should be initialised to the first value in their type which is False for boolean variables 2 3 1 Expressions The expression sub language is used to define conditions in the if and do constructs and the right hand sides of assignment statements The full syntax is spelt out in Section A 3 and what follows is an overview The only operators that are fully recursively general are the boolean constructs and or gt implication lt gt bi implication and zor All other operators are used to either construct propositions or basic arithmetic formulas Expressions can mention any subset of the local variables and environment parameters that are flagged observable Section 1 2 explains what the observable attribute means and Figure 3 2 gives an example of their use in expressions In the context of the definitions in Section 2 2 involving Int3 and x Int3 with value 3 basic expressions of the following forms are valid and have the specified value Enumeration x in 1 2 4 gt False x in 3 7 gt True Equality xz 2 gt False x 3 gt False Relational x gt 3 gt False x gt 3
30. lace an otherwise C branch with A cond C or add a A cond skip branch if it is absent Note this expansion also applies to a resolve clause if present 5 For all do od statements if the break branch is absent add break skip B 2 Expression Semantics Assume the following e The notion of var val is primitive The standard boolean algebraic identities hold f Vg uf A g f 4 nf 0 feg f gt g A g gt f f xor g z Ay V z A ey The expression is vvell typed e There is a map type Identifier Constant taking variables to sequences of constants e There are two operators on sequences pred a a a which returns the predecessor of an element in the sequence or the element if it is the first and succ a a a which returns the successor of an element in the sequence or the element if it is the last These operators simply implement truncating arithmetic as noted in Section 2 3 1 e Derived forms in the expression have been expanded using the following rules z gt elt x in elements of type x to the right of elt B 3 AGENT PROTOCOL SEMANTICS 31 x gt elt x in felt elements of type x to the right of elt lt elt in felt elements of type x to the left of elt x x lt elt in elements of type x to the left of elt elt x elt The definition of the function State
31. mantics The motivation for providing a detailed operational semantics is to make the timing model precise There are two major constraints on the design of the language 1 The agents need to have control over which action they emit at all times see the Robot example in Section 4 1 for further details 2 Automata must be naturally expressible Also arbitrary nesting of constructs and a simple regular timing model are very desirable In the following description let e Var be the type of variables Val be the type of values p Var Val be a global state gives values to all variables elt elt be sequences of arbitrary objects x val Var Val Var Val Var Val be a state transfomer _ val t y r val p y py otherwise e fog be function composition fog z f g x A summation style O is also used where Oo id and O O atail o head where headltail are a list of composable functions m order to implement the select resolve model Chapter 1 the overall state transition relation is split into two sets of relations agent local and environment Both rely on another relation to give meaning to expressions Expression Semantics 0 Expr Val is the expression evaluation function described in Section B 2 A gent local transitions For each agent A tvvo relations are defined p ProgramText ssa ProgramText are agent internal tr
32. n MCK by writing a nondeterministic program that computes this state transition function 4 each a in afo a is a subset of Se used to model a fairness condition Intuitively for each there is a state s a that occurs infinitely often in every run The behaviour of agents is given concretely in MCK by writing a program that describes their choice of action at each point of time Each such program defines a set of states S given concretely by means of a set of variables which includes the program counter a special variable whose value is the position in the program at which control resides at the given point in time Together the states of the environment and these protocol states determine the set of global states G these consist of tuples se 81 8 comprised of a state se in Se and a state s in S for each agent i Abstractly agent is program defines not just the protocol states S but in fact a tuple Si Ii Pi Ui where 1 I is the set of possible initial states of the protocol Concretely this is given by means of a constraint on the program variables 2 P G P A is a function mapping global states to a set of possible actions for the agent 3 mi Q x A P S is a function that describes how the protocol state including the program counter is updated when the agent performs an action We remark that the functions P and mu depend on global states rather than just protocol states bec
33. odel non deterministic events such as communication links failures and delavs We may model this non determinacy by representing the system as a set R of runs intuitively all the possible ways that the history of the system may evolve In general agents are not able to observe the entire state of the system We model this by means of a function G for each agent i where O is the set of observations made by agent i Intuitively O s is the information that is visible to agent when the system is in the global state s Based on their observations agents are able to make inferences about the situation in which they find themselves i e the particular state time and past and future history We model such a situation as a point represented as a pair r m where r is a run and m E Nisa time In order to determine what they know agents may make use of their observations in a variety of ways We capture the specific way that the agents use their observations for purposes of computing knowledge by assigning them a local state with respect to a view at each point of the system We write r m for the local state of agent i at the point r m where z is the view The simplest view is the observational view obs where the agent uses just its current observation to determine what it knows The local state in this case is defined by r2 m O r m Somewhat more informative to the agent is the clock view clock defined by ril F m
34. of knowledge to motion planning under uncertainty JACM 44 5 1997 D Chaum The dining cryptographers problem unconditional sender and recipient untrace ability Journal of Cryptology 1 65 75 1988 Edgar W Dijkstra A Discipline of Programming Prentice Hall Englewood Cliffs N J 1976 E Clarke O Grumberg and D Long Verification Tools for Finite State Concurrent Systems In J W de Bakker W P de Roever and G Rozenberg editors A Decade of Concurrency Reflections and Perspectives volume 803 pages 124 175 Noordwijkerhout Netherlands 1993 Springer Verlag E Clarke O Grumberg and D Peled Model Checking MIT Press 1999 Kai Engelhardt Ron van der Meyden and Yoram Moses A program refinement framework supporting reasoning about knowledge and time In Jerzy Tiuryn editor Foundations of Software Science and Computation Structures volume 1784 of Lecture Notes in Computer Science pages 114 129 Springer Verlag March 2000 R Fagin J Y Halpern Y Moses and M Vardi Reasoning about Knowledge The MIT Press 1995 Gerard J Holzmann The model checker SPIN Software Engineering 23 5 279 295 1997 M Huth and M Ryan Logic in Computer Science modelling and reasoning about systems Cambridge Universitv Press 2000 A Mvcroft and R A O Keefe A polvmorphic tvpe svstem for Prolog Artificial Intelligence 23 3 295 307 August 1984 Simon Pevton Jones John Huges et al Haskell 98 A non stric
35. onment var write erpr gt gt lt lt environment var write expr var expry UQTn expr gt gt provides a way for an agent to assign a value to a shared variable 2 4 3 Agent Bindings The next set of declarations bind distinct agent names to the protocols they run and instantiate each protocol s environment parameters There must be at least one agent in the system Note that this binding mechanism introduces the possibility of aliasing having multiple names for the same variable This is not an issue as the usual problem of interference doesn t arise agents can only write to a single environment variable per time step and conflicting writes are resolved at the memory location level 2 4 4 Initial conditions If an init_ cond declaration is present then the environment variables are constrained to satisfy it in the first state of the system Every such solution leads to a distinct initial state 2 4 5 Resolution An alternative communication mechanism is to provide a resolve clause which implements the second part of the select resolve model described in the introduction Chapter 1 In essence this clause is identical to a statement block in a protocol definition except that e Only non looping constructs are allowed no do or while loops e Guards are in terms of agent qualified actions and environment variables and are of a constrained form see Appendix A Informally this statement block is
36. or an example of this 6 CHAPTER 1 INFRODUCTION environment Robot Env There are 8 positions in the world If the robot is really at position p then the sensor will have a value p 1 p p 1 for a truncating interpretation of arithmetic type Pos 0 7 position Pos sensor Pos 10 agent Robot robot sensor init_cond position 0 sensor 0 At each time step the environment moves the robot one step to the right and generates a new sensor reading resolve begin if neg Robot Halt gt position position 1 fi 20 if True gt sensor position 1 True gt sensor position True gt sensor position 1 fi end spec_obs_ltl G sensor gt 3 lt gt Knows Robot position in 12 4 The bike handbrake protocol In order to stop moving the robot needs to keep the brake pressed 30 protocol robot sensor observable Pos begin do neg sensor gt 3 skip break gt lt lt Halt gt gt od while True do halted lt lt Halt gt gt end Figure 1 1 A simplified version of the robot example Chapter 2 The Input Language This chapter provides an informal description of the language used to describe the model checking scenario Section 1 1 which is more formally described in Appendix A syntax and Appendix B semantics An input script consists of a bunch of environment declarations one o
37. ple the unfair CTL operator EG f can be written as lfp 2 f VAX 2 Note that the evaluation of fixpoints is quite naive at the moment as the Emerson Lei algorithm or a more recent refinement isn t implemented See 5 Chapter 7 for details 3 4 Linear Temporal Logic Linear Temporal Logic is a well known linear time logic used for example in SPIN 8 Informally the available operators and semantics are as follows eventually f always f f until g f in the next state f in int steps LTL can directly encode fairness conditions but it is also possible to use CTL fairness con straints Section 3 6 An example of using LTL specifications is the following simple not fully correct mutual exclu sion algorithm environment mutex turnl Bool 3 5 KNOWLEDGE MODALITIES 15 turn2 Bool agent M1 mutex turnl turn2 agent M2 mutex turn2 turnl Non deterministic choice of who goes first init_cond turnl xor turn2 10 Safety spec_obs_lt G neg M1 in_cs M2 in_cs Non blocking FIXME spec_obs_ltl G F M1 left cs neg M1 in cs gt F Ml trying spec_obs_ltl G F M2 left_cs neg M2 in_cs gt F M2 trying Non strict sequencing fails spec_obs EF Ml in_cs E M1 in_cs 20 U neg Ml in_cs Elneg M2 in_cs U M1 in esl Liveness need to consider fairness spec_obs_ltl G F M2 left_cs M1 trying 7 F M1 in_cs spec_obs_ltl
38. putation i e using linear time temporal logic or LTL or it may describe the branching structure of all possible computations i e using the branching time or computation tree logic CTL The system currently supports different combina tions of all these parameters to different degrees in some cases this is because the implementation remains to be undertaken in others because there are inherent computational reasons why the problem is difficult or impossible to implement Figure 1 1 presents an example of the input file to the system modelling a scenario in which there is a single agent in the environment a robot called Robot running the protocol robot operating in an environment consisting of 8 possible positions and sensing the position using a noisy sensor whose values are recorded in the variable sensor which is observable to the agent The example contains a single specification formula indicated by the construct spec obs 111 which indicates the formula uses linear time temporal logic operators and that the knowledge operator Knows is to be interpreted using the observational interpretation for knowledge A more elaborate version of this example is discussed at greater length in section 4 1 In addition to determining whether a specification formula is true or false in a given scenario it is intended that future versions of the system will provide additional forms of support for the analysis of such scenarios such as permitting th
39. r discussed in Section 3 7 2 4 The Environment This section describes the environment declarations that specify how the agents communicate and which protocol they execute Discussion of the other declarations appearing under the environ ment section header specifications and fairness constraints are deferred to Chapter 3 Note that the declarations must appear in the script in the same order as they are presented here 2 4 1 Types The first set of declarations introduce zero or more types as specified in Section 2 2 24 THE ENVIRONMENT 11 2 4 2 Shared Variables The only communication medium currently implemented is a shared variables abstraction In essence such a variable has a particular value that persists unless it is written to The model checker resolves concurrent reads and writes to a variable by exploring all possible interleavings of these actions Shared variables are declared in the same fashion as agent local variables There are two specialised forms of actions used in protocols to access the shared variables The first lt lt local var environment var read gt gt lt lt local var environment var read vary expri varn expr gt gt assigns the value of an environment variable to a local variable taking into account concurrent writes Note that the environment variable need not be observable in this case in constrast to Section 2 3 1 The second form lt lt envir
40. r more specifications and zero or more protocols as illustrated in Figure 2 1 We proceed by describing the lexical con ventions the role of types the structure of agent protocols and finally the variety of environment declarations deferring specifications and fairness constraints to Chapter 3 2 1 Lexical Structure The lexical structure of the language follows Haskell 11 closelv Specificallv Comments begin with and terminate at the end of the line they appear on Constants start with an upper case letter and can be followed by any number of a mix of alphanumeric characters and underscores These are used in enumerated types Section 2 2 actions and agent names Variables start with a lower case letter followed by any number of a mix of alphanumeric char acters and underscores Program variables and labels belong to this class Relational variables start with an underscore followed by any number of a mix of alphanumeric characters and underscores These are used in p calculus specifications Section 3 3 2 1 1 Reserved Words The reserved words in the MCK input language of which there are many are spelt out in the formal syntax given in Appendix A 2 2 Types All types are finite enumerated totally ordered objects and so can be used in relational and arithmetic expressions in the natural way Types can be introduced by either explicitly enumerating their elements or by specifying a range of integers T
41. r to model check an implementation of the robot s control policy we need to restrict the environment to a finite number of locations We have arbitrarily chosen to have 8 distinct locations but any number greater than 4 is sufficient An input script implementing such a policy in such an environment is shown in Figure 4 2 Note that timing is critical in this example the robot must have continuous control over the emitted Actions and must be able to register it s intention to halt with the environment before the environment decides to move it any further These two constraints mean that using a while construct with the implied skip on exit is not sufficient for correctness This timing gap is illustrated via an alternative incorrect protocol shown in Figure 4 3 The sequence of position sensor robot action values 17 18 CHAPTER 4 EXAMPLES 0 0 Nill 1 0 Nill 2 1 Nill 3 2 Nill 4 3 Nill 5 4 Halt is an example of a run where the robot decides it wants to stop when it receives a sensor reading of 3 but doesn t manage to assert the halted action until it has moved past the goal region 4 2 The Dining Cryptographers The problem solved by this protocol is framed as follows 2 Three cryptographers are sitting down to dinner at their favorite three star restu arant Their waiter informs them that arrangements have been made with the maitre d hotel for the bill to be paid anonymously One of the cr
42. re provided as described in Section 2 4 2 An action costs 1 time step to execute 1 With the exception of bare constants 10 CHAPTER 2 THE INPUT LANGUAGE Derived forms This section gives the expansion of the various derived forms in terms of the core language skip The do nothing statement that consumes 1 time step The expansion is as follows skip lt lt Nill Action gt gt assignment A protocol can assign the value of an expression to a local variable in 1 time step The expansion is as follows var expr lt lt NillAction var expr gt gt Multiple variables can be assigned to in the same time step lt lt vary expry Var expr gt gt lt lt NillAction vari expr vara ELDTn gt gt This is also termed an atomic or parallel assignment if then else A choice construct derived from if The expansion is as follows if cond then Ci else C2 if cond C l neg cond Co fi while A repetition construct derived from do The expansion is as follows while cond do C do cond C break skip od Intuitivelv C is executed until cond becomes false The break skip branch means that it takes 1 time step to exit the while loop 2 3 4 Labels All statements can be given a not necessarily unique label which is written like so label C where label belongs to the Variable lexical class Labels may only be used within specifications and are furthe
43. resent protocols The most significant departure is that guards can mention agent qualified actions As mentioned in Section 2 3 3 the system currently provides shared variable read and write actions as primitives distinct from the mechanism described here A semantics for these primitives is omitted The definition of p 4 Statement State Action Var Val Var Val giving meaning to a resolve clause in terms of state transformers Ci 0 C1 Colpa C2 pra o C1 0 4 For each alternative 7 p A E cond if cond gt C filo Ci p a skip pa id var val Var Val p expr val z expr p a 2 gt val where id Var Val Var Val is the identity function for the specified type This function is purposefully non deterministic Conditions are evaluated with respect to a set of actions A and a state p The base cases are as follows Action A p A Action B 4 ENVIRONMENT RESOLVE CLAUSE SEMANTICS 33 p Var True p A E Var and the recursive cases for the logical connectives are similar to those in Section B 2 The definition of p ProgramTexti ProgramText gt pl ProgramTexti ProgramT ext taking states and program counters in one state to the next p ProgramTezti ProgramText gt n Actioni Assignmentji ProgramTert Action Assignment n ProgramTezti sten
44. t purelv functional language http haskell org definition February 1999 Ron van der Meyden Knowledge based programs on the complexity of perfect recall in finite environments extended abstract In Proceedings of the Conference on Theoretical Aspects of Reasoning about Knowledge Renesse Netherlands mar 1996 Ron van der Meyden Common knowledge and update in finite environments Information and Computation 140 2 1998 Ron van der Meyden and Kaile Su Symbolic model checking the knowledge of the dining cryptographers As yet unpublished 2002 23 24 BIBLIOGRAPHY Appendix A Input Script Syntax This section describes the abstract syntax of an input script in EBNF The convention is that UpperCase production names denote non terminals and lowercase names denote lexemes There are the following lexical classes see Section 2 1 constant and typename are Con stants label and varid are Variables and muvar are Relational variables The class int signifies integers A l Joint Protocols and the Environment JointProtocol Environment Protocol Environment EnvHeader TypeDec EnvVarDec EnvAgentDec EnvInitCond EnvResolve EnvSpec EnvFairness EnvHeader environment string TypeDec type typename 42 Enumeration F Enumeration Constant Constant int int EnvVarDec VarDec EnvAgentDec
45. yptographers might be paying for the dinner or it might have been the NSA US National Security Agency The three cryptographers respect each other s right to make an anonymous payment but they wonder if the NSA is paying Assuming that at most one cryptographer is paying the protocol shown in Figure 4 4 will allow all cryptographers to discover whether the NSA or one of their fellows is paying The details of the model checking of this protocol are given at length in 14 Prosaically this protocol illustrates the utility of arrays of environment variables in this case simply to implement a broadcast Unfortunately the environments become increasingly baroque to define as the number of agents increases due mainly to a blow out in the length of the initial condition and so it is not a complete solution to this problem 4 2 THE DINING CRYPTOGRAPHERS environment Robot Env There are 8 positions in the world If the robot is really at position p then the sensor will have a value p 1 p p 1 for a truncating interpretation of arithmetic type Pos 0 7 incpos Bool position Pos sensor Pos agent Robot robot sensor init cond incpos position 0 sensor 0 At each time step the environment might move the robot one step to the right and always generates a new sensor reading resolve begin if neg Robot Halt gt begin position position incpos
Download Pdf Manuals
Related Search