Home

MONA Version 1.4 User Manual

1. The following formula is additionally allowed in linear mode Q prefix The following formulas are additionally allowed in tree mode o root t univs instatespace t s variant t P E V tree CP type t E sometype t T First order terms in linear mode EE p Ct I t 1T t I ty I to t I te maxT minT Second order terms in linear mode T f Je XD elems empty pconst I Ty unionT TiinterT AND T I T I First order terms in tree mode tS uw te t succ t root Cu treeroot T succ t E V C Second order terms in tree mode T elems T Il Ti union T5 Ti inter T5 IBN T suc T const tree t E consttree 54 MONA 1 4 A 1 MONA grammar Other dems t Ego Sees dto univs u u suco OPL exp t T 6 params C par par varO b 9 vart varwherel var2 varwhere2 universe u var b p P guidearg s gt s2 83 univarg ul suc E varwherel p where q varwhere2 P where 6 consttree V consttree Restrictions and comments b is a name of a boolean variable which we also regard as a zeroth order variable p P are names of first and second order variables respectively A name can be any string of letters digits underscores dollar symbols and single quotes I is an constant integer expression e g 2 4 k 7
2. P gt is a r r pred is a star ab star varl p vari q exi r is a star p r amp is ab star r q is a star ab star 0 max 1 Figure 9 Regular expression over ASCII alphabet 38 MONA 1 4 7 Tree logic and tree automata Those readers only interested in MONA applied to linear structures may skip this section The MONA tool can also be used to decide logical theories based on trees This section describes the WS2S logic the Guided Tree Automata used in the decision procedure and the various MONA specific tree mode constructs Also an extension of WS2S called WSRT adding explicit support for recursive types is described 7 1 The WS2S logic WS2S the Weak monadic Second order theory of 2 Successors is the logic obtained by gener alizing WS1S to the domain of elements generated by two successors left and right instead of one 1 In WSIS interpretations correspond to strings and in WS2S to finite labeled trees In WSI1S a first order variable is interpreted as a natural number and in WS2S as a position in the infinite binary tree MONA runs in either linear mode or tree mode corresponding to the logics WS1S or WS28 The mode is chosen with the keywords wsis the default or ws2s in the header Also in tree mode MONA uses three valued logic see Section 3 2 Restrictions can be defined using where and defaultwhere just as in linear mode and an evaluation can lead to either true false or do
3. Pj inter P dfaSetminus int i int j int k p Py Pk dfaMax int 7 int 7 max P dfaMin int 7 int 7 min P dfaBoolvar int 7 dfaPresbConst int i int n pconst n dfaSingleton int 1 singleton P dfaLastPos int 7 see p dfaAllPos int i see p dfaFirstOrder int i see p 1 1 Figure 13 Basic DFAs been met in an accept state if the first 1 was met on the previous transition and in a reject state otherwise This automaton is used for the m compatibility option see Section 6 5 Constructing automata explicitly Constructing automata like those listed in Figure 13 is done using the following functions void dfaSetup int n int len int indices prepares construction of a DFA with n states and variable indices given by the array indices of length Lem void dfaAllocExceptions int m prepares construction of the next state allocating room for n exceptions i e n calls to dfaStoreException void dfaStoreException int s char path stores an exception on the transitions 63 MONA 1 4 given by path array of 0 s 1 s and X s of length Len given by dfaSetup go to state s instead of the default destination void dfaStoreState int s sets the default destination state to s for the state currently being constructed DFA dfaBuild char statuses constructs the DFA prepared by the previous functions using statuses array of s s and 0 s re
4. defaultwhere2 P alli p p in P gt alli r r lt p gt r in we declare a string of 8 bit vectors var2 bitO where bitO sub bit1 where biti sub bit2 where bit2 sub bit3 where bit3 sub bit4 where bit4 sub bit5 where bit5 sub bit6 where bit6 sub bit7 where bit sub macro consecutive in set varl p vari q var2 P p lt q amp pinP amp qinP amp allir p lt r amp r lt q gt r notin P ASCII a is 97 which is 01100001 macro is a varl p var q q p 1 p in bitO amp p notin biti amp p notin bit2 amp p notin bit3 amp p notin bit4 amp p in bitb amp p in bit6 amp p notin bit7 f ASCII b is 98 which is 01100010 macro is b vari p vari q p 16 notin bitO amp p in biti amp p notin bit2 amp p notin bit3 amp notin bit4 amp p in bitb amp p in bit6 amp p notin bit7 we concatenate by guessing the intermediate position where the string parsed according to the first regular expression in this case a ends and the string parsed according to the second in this case b starts pred is ab vari p var q exi r is a p r amp is b r q a star expression is handled by guessing the set of intermediate positions pred is ab star varl p var q ex2 P pin P amp q in P amp alli r r consecutive in set r r P gt is ab r r pred is a star vari p vari q ex2 P pin P amp q in P amp alli r r consecutive in set r r
5. filename amp which evaluates to the same minimal automaton as but has the side effect of writing the automaton to the designated file If allpos p see Section 6 5 has been specified for instance using the m21 str declaration the variable p will be projected away from the automaton being exported It is often the case that export is used for the side effect only and that a MONA file contains several exports T he top level construct execute q can then be useful with being an export formula It translates q for side effects only and evaluates to true In other words the automaton is thrown away after being exported The automaton is stored in external format also called dfa format Appendix C describes this format and shows how automaton files in this format can be used in other applications Automata in external format can be imported using the construct import filename ni n na n5 4 RAPT which evaluates to the automaton stored in the designated file where the free variables N1 N2 n from the variables list in the dfa file see Appendix C have been substi tuted by n4 n5 n respectivly It is checked that the type of each n is the same as that of ni Also the substitution must be order preserving in terms of variable indices If one wants to import an automaton in one variable order into a MONA program with another variable order the variables need to be reordered man
6. Essentially the same data structure arises in the MONA description we now formulate We are modeling queues of arbitrary length that contain elements in 0 1 2 3 To do so we describe a queue Q with second order variables Qe and Q1 Q2 e Qe denotes the used positions so we assume it is an initial subset of the natural numbers e The four possible membership status combinations that a position p has relative to Q1 and Q2 encode the value stored at position p 15 MONA 1 4 2 7 Example Reasoning about queues In Figure 6 we have described the encoding The predicate Queue stipulates that the queue has length 1 and that it is ordered Another predicate LooseOne expresses the removal of some element from a queue The formulas of the program hold if there is a queue Q of length 4 and a queue Q such that Q contains the value 3 and is the same as Q with one element removed We can indeed recognize such a situation from the MONA output below where the bit pattern notation comes in handy A satisfying example of least length 4 is Qe X 1111 Q1 X 0011 Q2 X 0101 Qe X 1110 Q1 X 001X Q2 X 011X Qe 0 1 2 3 Q1 2 3 Q2 1 3 Qe 0 1 2 Q1 2 Q2 1 2 For other practical examples visit our Web site or see the references in Section 16 MONA 1 4 2 7 Example Reasoning about queues Qe describes the valid indices of queue pred isWfQueue var2 Qe alli p pinQe amp p gt 0 in Qe isx holds
7. F Structure of a GTA and a guide A GTA is defined by the following typedef struct State initial initial state unsigned size number of states unsigned ls rs dimensions of behaviour matrix incl unused bdd handle behaviour behaviour ixrs j BDD ptr for state pair i j bdd_manager bddm BDD manager StateSpace typedef struct int final final status vector 1 reject O don t care 1 accept StateSpace ss array of state spaces GTA It is assumed that a GTA guide named guide of type Guide has been declared globally This guide is shared for all automata The following functions are associated the guide void makeGuide unsigned numSs SsId muLeft SsId muRight char ssName unsigned numUnivs char univPos char univName int ssType SsKind ssKind creates a guide with numSs state spaces The arrays muLeft and muRight define the mappings from state space identifiers to left and right state space identifiers respectively numUnivs is the number of universes univPos defines their positions as 0 1 strings representing paths and univName defines their names The array ssType contains for each state space the type number associated to that state space or 1 if the state space is not associated any type The array ssKind contains for each state space the kind of the state space which is one of the SsKind constants in gta h If
8. FIDO language and is also reminiscent of the LISA language ABP98 It can be reduced to WS2S and thus provides no more expressive power but utilizing the guide a more efficient decision procedure is often possible Example output When one or more recursive types have been declared the output format of satisfying exam ples and counter examples is essentially the same as the format of constant tree expressions For instance MONA generates the following satisfying example for the program shown above 49 MONA 1 4 7 9 Recursive types and WSRT satisfying example is x u RED right BLUE GREEN NULL r u RED right This is read as follows The root of the x tree is at the RED right successor of the root of the u universe The root of x is labeled BLUE its x successor is labeled GREEN if BLUE had more than one component we would also get a successor for the other components here and its successor is labeled NULL The set denoted by r is a singleton set containing the RED right successor of u that is the same position as the root of x Implementation WSRT is reduced to WS2S extended with a few extra constructs using a technique called shape encoding introduced in DKS99 We omit the details here but describe the basic ideas central aspect is that extra nodes are added to the trees such that they become binary trees This allows a guide to be constructed from the recursive types The resulting state spaces can be divide
9. In Trees and algebra in programming CAAP 96 volume 1059 of LNCS 1996 Jean Paul Bodeveix and Mamoun Filali Quantifier elimination technics for pro gram validation Technical report IRIT 97 44 R 1997 David Basin and Stefan Friedrich Combining WS1S and HOL In Frontiers of Combining Systems 2 volume 7 of Studies in Logic and Computation Research Studies Press Wiley 2000 Jean Paul Bodeveix and Mamoun Filali FMona a tool for expressing validation techniques over infinite state systems In Tools and Algorithms for the Construc tion and Analysis of Systems TACAS 00 volume 1785 of LNCS 2000 David Basin and Nils Klarlund Automata based symbolic reasoning in hardware verification Formal Methods In System Design 13 255 288 1998 Extended version of Hardware verification using monadic second order logic CAV 95 LNCS 939 Morten Biehl Nils Klarlund and Theis Rauhe Algorithms for guided tree au tomata In First International Workshop on Implementing Automata WIA 96 volume 1260 of LNCS 1997 Kenneth M Butler Don E Ross Rohit Kapur and M Ray Mercer Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams In ACM IEEE Design Automation Conference DAC 91 1991 Randal E Bryant Graph based algorithms for boolean function manipulation IEEE Transactions on Computers C 35 8 677 691 Aug 1986 Randal E Bryant Symbolic boolean manipulation with ordered binar
10. called the indez to each variable MONA 1 4 uses a simple choice of ordering All explicitly declared variables are ordered consecutively in ascending order of declaration Implicitly declared variables that is those created internally during the translation process are placed after the explicitly declared vari ables in the order they are allocated which is somewhat arbitrary Although this ordering usually is sufficient we plan to extend MONA with heuristic meth ods for obtaining more efficient orderings as explained in Section To avoid confusion note that each variable is also assigned a variable number used for internal references within MONA In the current index assignment these numbers are the same as the indices however this will change in future versions 2 6 Predicates and macros MONA provides two methods for parameterizing and reusing formulas Macros are instanti ated by syntactical expansion where actual parameters replace formal parameters Predicates are compiled into automata that may be reused Both macros and predicates may refer to global variables 14 MONA 1 4 2 7 Example Reasoning about queues var2 P Q P Q 0 4 union 1 2 pred even var1 p ex2 Q p in Q amp alli q 0 lt q amp q lt p gt q in Q gt q 1 notin Q amp q notin Q gt q 1 in Q amp O in Q var x varO A A amp even x amp x notin P Figure 5 even with pred mona In Figure 5 ev
11. defaultwhere1 p p in defaultwhere2 P P sub The idea is the same as for M2L Str A special variable is used as a skeleton to which all other explicitly declared variables are restricted 7 9 Recursive types and WSRT In order for the GTA based decision procedure for WS2S to be efficient a proper guide must be constructed a task that requires knowledge about the application domain However for applications that are based on recursive types an efficient guide can often be constructed automatically from the recursive types being used Note that this MONA feature is just one example of extending WS2S We plan to add more high level support of this kind in future versions This section is not essential for the understanding of tree mode in MONA The logic WSRT Weak monadic Second order logic with Recursive Types is a variant of WS2S where recursive types are made explicit WS2S was introduced in EMS00 based on an encoding technique from DKS99 When applicable WSRT has some benefits compared to pure WS2S e it allows structures for which the number of successors to a given tree position is not fixed to two e it provides more high level structural primitives and e generated examples and counter examples are provideed in a more high level format Current applications of WSRT include the tools described in EMS00 and DKS99 47 MONA 1 4 7 9 Recursive types and WSRT Recursive types recursive type is
12. performs the prefix close operation on a see Section 6 2 DFA dfaProduct DFA aj DFA a2 dfaProductType mode performs product construc tion on a and ag The value of mode defines which boolean operation is performed according to the table in Figure 64 MONA 1 4 Boolean function dfaAND dfa0R dfaIMPL dfaBIMPL Figure 14 Product operation modes DFA dfaProject DFA a unsigned index projects away track index from a and de terminizes the resulting automaton void dfaRightQuotient DFA a unsigned index performs the right quotient opera tion described in Section DFA dfaMinimize DFA a minimizes a that is constructs an automaton with the min imal number of states and BDD nodes accepting and rejecting the same languages as the original automaton Analysis and printing The following functions generate information about automata char dfaMakeExample DFA a int kind int num unsigned indices generates a shortest satisfying example if kind 1 or a counter example if kind 1 to the formula represented by a using the technique described in Section 2 3 The array indices of length num contains the free variables The resulting char array is the concatenation of the rows of 0 s 1 s and X s of the example string void dfaAnalyze DFA a int num char names unsigned indices char orders int treestyle analyzes the automaton a and prints the results as shown in Section
13. which is read w satisfies if the interpretation defined by w makes true wE 9 iff wkd wed amp o iff wkd and wE wFex2P iff Jfinite M C N w P M F g wFP subP iff w Pi C w P vERPA if w P w Pi w Pk vER PH if wB 41 jcu P where we use the notation w P M for the shortest string w that interprets all variables Pj j 4 i as w does but interprets P as M Note that if we assume that w is minimum then w decomposes into w w w where w is a string of letters of the form 0 Oxo aS pa 0 where the ith component is the only one that may be different from 0 It has been shown that the complexity of the decision problem for WS1S is non elementary Mey75 Our decision procedure described next exhibits this worst case behavior However in practice KMSOQ the situation is often not that unfavorable 19 MONA 1 4 3 1 The classical approach The semantics allows quantification over only finite sets of naturals Without this re striction the logic is simply S1S monadic Second order theory of 1 Successor which is also non elementary decidable B c60a although no practically useful decision procedure is known Automaton construction For a formula define its language L as the set of satisfying strings 9 tw wE 9j We now formulate the automata theoretic calculations that allow us to conclude that any L 0 is a regular language Thus we will sho
14. 2 3 The arrays names indices and orders are for the free variables These arrays have length num The array orders contains Os 1s and 2s representing boolean first order and second order respectively If treestyle is non zero examples are written in GTA style void dfaPrintVitals DFA a prints the number of states and BDD nodes in a void dfaPrint DFA a int num char names unsigned indices prints a tex tual description of a as shown in Section 2 4 The arguments num names and indices are the number of free variables their names and their indices respectively void dfaPrintGraphviz DFA a int num unsigned indices prints a in dot for mat as illustrated in Figure B void dfaPrintVerbose DFA a prints a verbose textual description of a as illustrated in Section 5 1 65 MONA 1 4 D 1 Examples Presburger arithmetic and transduction Exporting and importing Importing and exporting as described in Section 6 1 is done using the following functions void dfaExport DFA a char filename char names int orders exports a to the file named filename in the format described in Appendix C T The null terminated array names contains the names of the variables of a and orders contains the orders 0 boolean 1 first order 2 second order DFA dfaImport char filename char names int orders imports an automaton from the file named filename and makes names and orders poin
15. 7 n Disable analysis of resulting automaton If analysis is enabled default MONA prints valid unsatisfiable or a satisfying example and a counter example See Sec tion t Print the time spent computing See Section 5 1 s Print statistics for each automaton operation See Section 51 i After each automaton operation the resulting automaton is printed See Section 5 1 d Dump the abstract syntax tree symbol table contents the guide in tree mode and the code DAG See Section 5 1 q Disable progress information Default is to enable See Section e Enable separate compilation The directory designated by the environment variable MONALIB is used as base for the automaton library If MONALIB is not set the current working directory will be used instead See Section oN Set code optimization level Currently only 0 and 1 are allowed 0 means disable optimization 1 means enable all optimization described in Section 4 2 Default level is 1 See Section 1 2 f Force normal tree mode output style of satisfying examples and counter examples in stead of linear mode or WSRT output style m Use alternative M2L Str emulation v1 3 style See Section 6 5 h Analyze inherited acceptance status on resulting automaton See Section 7 7 u Unrestrict output automata See Section 6 4 gw Output resulting automaton in graphviz format if in linear mode See Section gs Output satisfying example tree in
16. An example application A simple application of dfalib is located in the Lib directory as dfa2dot c It takes two command line arguments the name of a source dfa file and the name of a destination dot file It simply reads the dfa file using mdLoad and dumps it in dot format to the dot file This dot file can then later be processed with the dot tool The following graph is generated for the P sub Q example above The complete structure of the BDD representation is shown larger example is shown in Figure See Kla98 for a description of the use of BDDs in MONA The graphviz tool is also used in Section 5 2 C 2 Using GTA files Format of GTA files Running MONA on the following program ws2s var2 P Q export test gta P sub Q generates the file test gta which illustrates the format of a gta file MONA GTA number of variables 2 state spaces 3 59 MONA 1 4 C 2 Using GTA files universes 2 State space sizes 22 1 final 1 1 guide hat 1 2 univ 1 1 dummy 2 2 universes univ 0 dummy 1 variable orders and state spaces P2 1 Q2 1 state space 0 initial state 0 bdd nodes 2 behaviour end The GTA file library Similar to the DFA file library described in the previous section a small GTA file library is available in the MONA package as Lib gtalib ch so that the GTAs generated by MONA can be used in other applications The foll
17. Concur rency EXPRESS 00 State College USA August 21 2000 August 2000 vi 130 pp Bernd G rtner Randomization and Abstraction Useful Tools for Optimization February 2000 106 pp Peter D Mosses and David A Watt editors Proceedings of the Second International Workshop on Action Semantics AS 799 Amsterdam The Netherlands March 21 1999 May 1999 iv 172 pp Hans Hiittel Josva Kleist Uwe Nestmann and Ant nio Ravara editors Proceedings of the Workshop on Semantics of Objects As Processes SOAP 99 Lisbon Portugal June 15 1999 May 1999 iv 64 pp
18. are A B Booleans XX AN VAS UN EST IN PI IN ATR ZN GA Again we see 5 occurences of 1 in the A track and 7 occurences of 1 in the B track Outputting minimal GTAs Executing mona w ab2 mona first prints Guide d0 0 1 2 a 1 gt 1 1 b 2 gt 2 2 45 MONA 1 4 7 7 Inherited acceptance analysis which shows how numbers are assigned to the state spaces The number 0 is always the number of the boolean state space i e the state space in the root of the binary tree It then prints GTA for formula with free variables A B Accepting states 1 Rejecting states O State space O d0O size 2 Initial state O Transitions 0 0 XX gt 1 6 7 XX gt 0 6 8 XX gt 0 State space 1 a size 7 Initial state 2 Transitions 0 0 XX gt 3 0 1 XX gt 3 0 2 0X gt 0 0 2 1X gt 3 6 6 XX gt 3 State space 2 b size 9 Initial state 2 Transitions 0 0 XX gt 5 0 1 XX gt 5 0 2 X0 gt 0 0 2 X1 gt 5 8 8 XX gt 5 The format resembles the one described in Section 2 4 As an example the very last transition shown here defines that 62 8 8 XX 5 in the notation used on p For a method for visualizing GTAs see Appendix C 2 7 7 Inherited acceptance analysis For GTAs the notion of acceptance status of states is only defined in the root state space as described in Section For some applications however it is useful t
19. associated to the free variables GTA gtalmport char filename char names int orders SSSet ss int set guide imports an automaton from the file named filename and makes names orders and ss point to newly allocated arrays as those described at gtaExport If set guide is non zero the global guide is set to the guide defined in the file If zero it it checked that the global guide and the guide in the file are the same An example application A small example dummy application is located in Examples gta example c It uses the functions gtaImport gtaCalcInheritedAcceptance and various BDD functions 72 MONA 1 4 F TheMONA BDD package The MONA BDD package has been written for maximum speed of the BDD operations needed for the BDD represented automata in the MONA tool The package achieves a factor 6 speed up over David Long s original BDD package for the specialized task of MONA calculations but at the expense of a storage model that may make it hard to use correctly In the MONA tool an automaton with n states is represented by a shared BDD with n roots and n leaves It is assumed that when an automaton is calculated there is not a large proportion of it that can be retrieved as part of an already calculated automaton This is in contrast to usual BDD packages which use facts such as 1 to calculate certain specialized products in unit time by pointing to an already calculated subresult This strategy hinge
20. c where k and c are constants declared by the const declaration i denotes an integer c name s and u denote the names of a constant a predicate or macro a state space or a name of universe respectively In general a variable can be used in place of universe or state space name denoting the universes or state spaces associated to the variable E V and C denote the names of a recursive type a type variant and a variant component respectively v denotes the name of a variable in an external file Variables macros and predicates must be defined before they are used If defaultwhere declarations are used they must be placed before all predicate and macro declarations For macro and predicate invocations the argument types must match In tree mode the formal arguments inherit the universe declarations from the actual arguments but the associated restrictions are given by the predicate declaration 55 MONA 1 4 A 2 Precedence and associativity e Anything related to guides universes and recursive types only makes sense in tree mode There can be at most one guide header and one universe header The guide must be declared before the universes Universe positions must be specified if and only if an explicit guide is declared An explicit guide cannot be made if recursive types are used Recursive types require tree mode The root term requires an argument if universes are explicitly declared The argument must denote a
21. describes some examples where the DFA package has been used to construct operations for Presburger arithmetic One of the examples also illustrates how to make automaton transductions Structure of a DFA The following struct defines a MONA DFA typedef struct bdd_manager bddm manager of BDD nodes int ns number of states bdd_ptr q transition array int s start state int f state statuses 1 reject O don t care i accept DFA This representation of automata is described in detail in Kla98 The whole DFA structure can be illustrated as in Figure The array q corresponds to the thick pointers from the boxes labeled 0 to 10 in that figure The bdd_manager is described in Appendix For most operations the functions described below which do not expose the BDD level should be sufficient Predefined basic automata The functions in Figure 13 construct basic automata P p and b denote second order first order and boolean variables respectively and n denotes an integer constant In functions with a 2 in the name the variables denote second order variables A 1 means first order variables As described in Section B first order variables are encoded as second order variables in the following way the value of a first order variable is the smallest element in the set belonging to the variable interpreted as a second order variable First order variables are implicitly restricted to b
22. expressions do The automaton for a formula can be calculated by a simple induction scheme where logical connectives correspond to classic automata theoretic operations such as product and subset constructions Validity and unsatisfiability of the formula can be determined and satisfying examples and counter examples can be constructed by analyzing the associated automaton Despite its name WS1S is a simple and natural notation Being a variation of first order logic WS1S is a formalism with quantifiers and boolean connectives Its interpretation however is tied to arithmetic somewhat weakened to keep the formalism decidable In WSIS first order variables denote natural numbers which can be compared and subjected to addition with constants WS1S also allows second order variables while remaining decidable each such variable is interpreted as a finite set of numbers WSIS and its generalization WS2S Don70 which is interpreted over the infinite binary tree can be used to express problems ranging from hardware verification to formal lin guistics Unfortunately the space and time requirements for translating formulas to automata have been shown to be non elementary i e bounded from below by a stack of exponentials whose height is proportional to the length of the formula Mey75 Thus the decidability property has for many years been considered intractable for practical use Nevertheless the MONA tool shows that an efficient implementat
23. if p contains an x pred isO vari p var2 Qe Q1 Q2 in Qe notin Q1 amp p notin Q2 pred isi varl p var2 Qe Q1 Q2 in Qe notin Q1 amp p in Q2 pred is2 vari p var2 Qe Q1 Q2 in Qe in Q1 amp p notin Q2 pred is3 vari p var2 Qe Q1 Q2 in Qe in Q1 amp p in Q2 lt compares the elements at positions p and q of a queue pred lt vari p q var2 Qe Q1 Q2 isO p Qe Q1 Q2 amp isO q Qe Q1 Q2 Gsi p Qe Q1 Q2 amp is2 q Qe Q1 Q2 is3 q Qe Q1 Q2 is2 p Qe Q1 Q2 amp is3 q Qe Q1 Q2 isLast holds if p is the last element in the queue pred isLast vari p var2 Qe p in Qe amp alli q q in Qe gt q lt p f an ordered queue of length 1 pred Queue var2 Qe Q1 Q2 vari 1 isLast 1 1 Qe amp alll p q p lt q amp p in Qe amp q in Qe gt 1t p q Qe Q1 Q2 eqQueue2 compares elements in two queues pred eqQueue2 var1 p q var2 Q1 Q2 Q1 Q2 p in Q1 lt gt q in Q1 amp p in Q2 lt gt q in Q2 LooseOne holds about a queue Q and a queue Q if queue Q is the same as Q except that one f element denoted by p below is removed pred LooseOne var2 Qe Q1 Q2 Qe Q1 Q2 exi p p in Qe amp alli q isLast q Qe gt q in Qe lt gt q in Qe amp isLast q Qe gt q notin Qe amp alll q q lt p amp q in Qe gt eqQueue2 q q Q1 Q2 Qi Q2 amp alll q q gt p amp q in Qe gt eqQueue
24. in FMona BF00b and FIDO 52 MONA 1 4 A Syntax The grammar below describes the full MONA syntax in a BNF like notation with the follow ing meta syntax either X or Y an optional X zero or more occurrences of X zero or more occurrences of X separated by commas one or more occurrences of X and one or more occurrences of X separated by commas A 1 MONA grammar MONA program program header declaration header wsis ws2s m2l str m2l tree Declarations declaration q guide guidearg universe univarg include filename assert q execute q const c I defaultwherel p defaultwhere2 P o varo b vari univs varwherel var2 univs varwhere2 tree univs varwhere2 macro name params pred name params allpos P type E V C C E 53 MONA 1 4 A 1 MONA grammar Formulas true false 4 b un di amp do 1 do di gt Q2 di lt gt 9 name exp name ty to ti t ti lt t2 ti gt t2 ty lt to ti gt t T T5 Ti T Ti sub T tinT t notin T empty C T restrict 9 export filename import filename v gt var exo b allo b ex1 univs varwherel q alli univs varwherel ex2 univs varwhere2 q a112 univs varwhere2 leto b 9 ing let1 p t ing let2 P T in
25. is 1 if the meaning of the conjunction of all restrictions of variables in the formula is not otherwise the semantics is the standard one The automata theoretic approach As in the case of WS1S we can show that the semantics can be represented by finite state automata So we need to demonstrate automata Ag that calculate o w Naturally the states of these automata are characterized according to the three valued domain that is as accepting rejecting or don t care 1 We write A w to denote the value calculated by A on word w this value is the acceptance status of the state that A reaches when reading w basic observation is that any automaton by a simple relabeling of acceptance status can be transformed into an automaton R such that gus f if A w l if Aw A 24 MONA 1 4 3 2 The MONA approach Then it is not hard to see that an atomic formula like 9 P sub P can be represented by the automaton where A is the classical automaton for P sub P as already presented and x is the automata product with product states characterized according to the three value truth table for amp Note the use of the recursion in arguments p P and p P It can be shown that the automata theoretic calculations of the three inductive cases in the classical approach can be generalized to the three valued semantics In fact only the case of existential quantification requires careful consideration The transformat
26. not occur for strings where the first thing that the automaton encounters is the assignment of values to the booleans We would like tree mode to use the same idea in a future version of MONA 8 4 Support for user definable predicates and functions Many applications of MONA would benefit from the possibility of defining automata and automata operations and incorporate these in the syntax To some extent this is currently possible using the interfaces to the DFA GTA and BDD packages see Appendices DI E E What needs to be done is a rewrite of the front end so that user defined automata and automaton operations easily can be plugged into it in a modular way Also the current syntax only allows predicates and macros as syntactic abbreviations It is often convenient to also allow functions evaluating to first or second order values to be defined 8 5 Higher level notation Although based on mathematical logic the current MONA notation has many similarities with machine code To manually encode systems and properties as booleans natural numbers sets of numbers and binary trees can be a tedious process To alleviate this burden we plan to integrate a higher level symbolic language as syntactic sugar on top of the basic language The recursive types described in Section 7 9 is one step in this direction Other useful features include enumeration types and composite types arbitrary fanout in the tree mode guide and more features found
27. orders 2 2 states 3 initial 0 bdd nodes 4 final 0 1 1 behaviour 0 1 3 bdd 1 10 002 130 1 20 end The behaviour array assigns a BDD node to each state Each line following bdd corresponds to a BDD node If the th line contains 1 val 0 BDD node i is a leaf with value val If it contains x r where x 1 node i is an internal node with index x left low successor l and right high successor r The DFA file library A simple C application programming interface for DFA files is available in the MONA package as Lib dfalib ch It allows the user to load manipulate and store DFAs in the external file format and to run a given string on the DFAs completely independent of MONA The interface file dfalib h contains the following functions 58 MONA 1 4 C 2 Using GTA files mdDfa mdLoad char filename loads a DFA file into memory int mdStore mdDfa dfa char filename stores a DFA in a file If the stored au tomaton is modified and used in MONA using import the user must ensure that the content is consistent and that the BDD is properly reduced and ordered void mdFree mdDfa dfa deallocates the memory used by the DFA mdState mdDelta mdDfa dfa mdState s mA a represents the transition function Q x X gt Q of the automaton The parameter a refers to an array of 0 1 chars which denotes an alphabet symbol l he array has one entry per variable in declaration order
28. recursive types are not being used ssType and ssKind may be set to 0 void makeDefaultGuide unsigned numUnivs char untvName creates a default guide as described in Section as method 2 void freeGuide deallocates the memory used in the guide void printGuide prints a textual description of the guide int checkAllCovered checks that the guide is covered with universes as described in Section 7 3 int checkDisjoint checks that the universes cover disjoint state space sets int checkAllUsed check that all state spaces are reachable from the root 68 MONA 1 4 GTA function MONA formula gtaTrue true gtaFalse false gtaLess int int j SSSet s SSSet sj Pi pj gtaLesseq int 7 int j SSSet s SSSet sj j lt pj gtaEqi int 4 int 7 SSSet s SSSet sj p ps gtaEq2 int 4 int 7 SSSet s SSSet sj p Py gtaEmpty int 7 SSSet s empty gtaln int i int 7 SSSet s SSSet sj in Pj gtaSub int 4 int 7 SSSet s SSSet sj Sub P gtaUnion int int j int k SSSet s SSSet sj SSSet sx Pj union Pi gtaInter int i int j int k SSSet s SSSet sj SSSet sp inter P gtaSetminus int 2 int j int k SSSet s SSSet sj SSSet sp gtaDotO int 4 int j SSSet s SSSet sj gtaDoti int 4 int j SSSet s SSSet sj gtaUp int i int j SSSet s SSSet sj P gtaRoot int 2 SSSet s SSSet u 4 root u gtaBoolvar int 2 i gtaSingleton int 2 SS
29. single universe e Therecursive type constructs succ tree type sometype variant const tree tree root are only allowed if recursive types are declared e most one allpos declaration is allowed A in a line causes MONA to treat the rest of the line as a comment Alternatively a whole block can be treated as a comment by delimiting it with and A 2 Precedence and associativity The table below shows the precedence and associativity of the MONA operators If for instance the operator op has higher precedence lower precedence number than the operator op then the expression E op E opo Es is interpreted as E op E2 opo Es If the precedences are equal then the interpretation is decided by the associativity e g if op is right associative then E op E op Es is interpreted as Fj op E2 op E3 The default rules can be overridden with parentheses Associativi 1 non associative 2 3 4 5 6 7 8 9 10 11 See ee oF CS N h ds inter union max min gt lt lt in notin sub 56 left associative left associative left associative left associative left associative non associative non associative non associative non associative left associative left associative right associative right associative non associative MONA 1 4 B Usage The usage of the MONA tool is mona options filename The options are w Output a description of the resulting automaton See Section 2
30. 0 10 0 11 1 gt state 2 State 1 8 0 10 1 11 0 gt state 2 State 1 8 0 10 1 11 1 gt state 1 State 1 8 1 411 0 gt state 2 State 1 48 1 411 1 gt state 1 2 State gt state 2 The format resembles the one from Section The only difference is that the transitions are written more explicitly For example 8 1 means that the variable with index 8 has the value 1 5 2 Visualization of automata In WS1S mode a graph representation of the program automaton can be generated with the gw option The format of the output is readable by the graphviz tool dot property of AT amp T Example mona gw even mona gt even dot dot Tps even dot o even ps generates the graph shown on page 13 to the file even ps The graphviz tools can be found at http www research att com sw tools graphviz Appendix C T describes another kind of automaton visualization which shows the full BDD structure 32 MONA 1 4 6 Advanced constructs This section describes features for exporting and importing of automata performing prefix closing of automata controlling formula restrictions and emulating monadic second order logic on strings M2L Str and Presburger arithmetic 6 1 Exporting and importing automata If MONA is used as an automaton generation tool two features are available for exporting automata The first is using the w option as described in Section 2 4 The other is the formula level construct export
31. 2 q q 1 Q1 Q2 Qi Q2 var2 Qe Q1 Q2 the queue Q var2 Qe Q1 Q2 the queue Q assert isWfQueue Qe the primed variables denote a queue of length 3 containing three of the elements 0 1 2 3 in that order and the element 3 Queue Qe Q1 Q2 4 f the queue Q is a queue of length 3 containing the elements 0 1 2 3 LooseOne Qe Q1 Q2 Qe Q1 Q2 4 Q is Q except for one element exi p is3 p Qe Q1 Q2 Q does contain the element 3 Figure 6 lossy_queue mona 17 MONA 1 4 3 Theautomaton logic connection The beginning MONA programmer may skip this section but it is necessary for a thorough understanding of the tool Since the MONA notation is a logic interpreted over natural numbers it is not difficult to define its formal semantics But a programming notation also has a compilation semantics which details how the source code is transformed Usually an exact description of the compi lation such as the source code for a compiler is neither available nor useful to a programmer With MONA however we need to carefully explain the compilation since the process may involve heavy or even infeasible symbolic calculations Our explanation is in two parts first we explain the classical WS1S approach B chi and Elgot Elg61 next we in troduce a version of WS1S where restrictions are syntactically manifest and we explain the semantic and automata theoretic consequ
32. AG can be thought of as being constructed from the tree using a bottom up collapsing process This process is based on a formula equivalence relation signature equivalence Two formulas and amp are signature equivalent if there is an order preserving renaming of the variables in with respect to the indices of the variables such that the code trees of and become identical A property of the BDD representation is that the automata corresponding to signature equivalent trees are isomorphic in the sense that only the node indices differ This property is used by MONA for automatic reuse of intermediate results For example consider the formula exi q p lt q amp q r where the variables p q r have the indices 1 2 3 respectively The automata for the sub formulas p lt q and q lt r are isomorphic so their tree nodes are collapsed The edges of the resulting DAG are labelled with the renaming information DAGification o 1 q p r q Experiments show that significant time improvements using DAGification are possible typically a factor 2 to 4 The contents of the DAG can be shown as a graph as above using the gd option and the graphviz dot tool See Section 5 2 for more information about visualization using graphviz 27 MONA 1 4 42 Formula reductions 4 2 Formula reductions Formula reduction is a means of optimizing the formulas in the DAG before translating them into automata The reductions ar
33. Set s singleton Pi gtaInStateSpace int 4 SSSet ss SSSet s in state space P ss gtaFirstOrder int i SSSet s see below gtaAllPos int SSSet s see below gtaWellFormedTree int 2 SSSet s tree P gtaSomeType int SSSet s type P Figure 15 Basic GTAs Predefined basic automata Figure 15 shows the functions that construct basic automata The notation used is the same as for the basic automata in the DFA package see p 62 The SSSet arguments contain sets of state space identifiers Each variable P has an associated a state space set s The automaton constructed by gtaFirstOrder 5 accepts the trees which have a 1 at index 4 at a position belonging to a state spaces in s and that there are not two such positions that are incomparable This automaton is used as the implicit restriction associated to all first order variables The automaton constructed by gtaAllPos s accepts the trees which have a 1 at index 4 at every position belonging to a state spaces in s This automaton is used for the allpos construct Constructing automata explicitly GTAs can be constructed explicitly using the following functions 69 MONA 1 4 void gtaSetup unsigned rootsize prepares construction of GTA with rootsize states in the root state space void gtaSetupDelta SsId d unsigned lsize unsigned rsize unsigned indices unsigned num prepares construction of transitions in state space d w
34. Tenuen J9SN p UOA VNOIN HUSN V PUNNEIY T T0 SN SOTAA BRICS Basic Research in Computer Science MONA Version 1 4 User Manual Nils Klarlund Anders M ller BRICS Notes Series NS 01 1 ISSN 0909 3206 January 2001 Copyright c 2001 Nils Klarlund amp Anders M ller BRICS Department of Computer Science University of Aarhus All rights reserved Reproduction of all or part of this document is permitted on condition that it is unmodified includes this copyright notice and distributed for free See back inner page for a list of recent BRICS Notes Series publications Copies may be obtained by contacting BRICS Department of Computer Science University of Aarhus Ny Munkegade building 540 DK 8000 Aarhus C Denmark Telephone 45 8942 3360 Telefax 45 8942 3255 Internet BRICS brics dk BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs http www brics dk ftp ftp brics dk This document in subdirectory NS 01 1 MONA Version 1 4 User Manual Nils Klarlund Anders M ller amoeller brics dk January 2001 Copyright c 1997 2001 Nils Klarlund amp Anders M ller BRICS Department of Computer Science University of Aarhus All rights reserved Reproduction of all or part of this document is permitted on condition that it is unmodified includes this copyright notice and is distributed for free The MONA tool is available unde
35. a Presburger arithmetic first order value corresponds to a WS1S second order value The MONA second order term construct pconst J encodes the natural number I into a second order value using least significant bit first en coding This encoding has the property that is is closed by concatenation with Os which is required by the WS1S decision procedure see Section 3 1 All other Presburger constructs can be expressed using predicates Appendix D 1 contains some examples of using Presburger arithmetic 6 4 Restriction As described in Section 3 2 MONA allows restrictions to be associated with the use of vari ables Where quantifications and global declarations of first order and second order variables vari a112 etc occur it is possible to specify where p which makes p the user defined restriction of the variable See Section 3 2 for a discussion of the semantics of restrictions Note that restrictions must always be satisfiable for MONA to calculate correctly MONA does not check this requirement As an example in the program var2 R var2 W where W sub R Q the variable W is associated the restriction W sub R This program will evaluate to don t care if W is not a subset of R no matter what q is As another example the formula ex1 p where p in Q evaluates to true if there exists a position p in Q such that q is satisfied to don t care if p in Q cannot be satisfied i e if Q is empty and to false otherw
36. ates that are not don t care states are those that are reached by strings containing at least one occurrence of a 1 in the x track Variables are indexed from 0 P in the first track to 3 A in the fourth track To see how the transition table is represented consider state 2 and the letter 1 oS 13 MONA 1 4 2 6 Predicates and macros Figure 4 The BDD based representation of even mona The next state is gotten as follows follow the pointer out of the description of state 2 in the array to the BDD node which has index 0 corresponding to variable P The value of the P component is 1 so we go to the high successor which in turn is marked 1 denoting the Q component Then since this bit is 0 we take the low successor to the next node That node corresponds to x which is 0 so we end up at a leaf mark 4 That is the value of the next state The graph shown in Figure 4 was generated using the features described in Section 6 1 and Appendix C 1 Variable indices The BDD representation depends on an ordering of the variables Theoretically any ordering will work however the choice of ordering can have a strong impact on the the number of nodes required to represent a given automaton and thus also on the execution time see Section 8 1 The ordering is defined by assigning a unique natural number
37. ays true or not valid sometimes formula is false alternatively and equivalently the algorithm can classify formulas according to whether they are satisfiable sometimes true or unsatisfiable always false MONA 1 4 12 MONA applications automaton A MONA program consists of a number of declarations and formulas The two line WS1S program below contained in a file simple mona declares two free second order variables P and Q and postulates that the set difference of P and Q is the union of the sets 0 4 and 11 2 var2 P Q P Q 0 4 union 1 2 Clearly this formula is not always true but there is an interpretation that makes it hold for example the one which assigns 0 1 2 4 to P and 5 to Q This interpretation usually written as P 0 1 2 4 Q 5 can also be represented by Os and 1s in a string OO where letters are bit vectors Each variable is described by a track along the string Here the P track is 111010 and the Q track is 000001 The positions in the string correspond to natural numbers a 1 in a position means that the number is in the set a 0 that it is not We can define the language associated to simple mona as the set of such finite strings that define satisfying interpretations It is a fact see Section B that for WS1S this language is regular i e it can be recognized by a finite state automaton MONA is able to analyze simple mona automatically by translating it into the min
38. can be verified The implementation is based on the DFA part of MONA PAX PAX is yet another tool for verifying parameterized systems using MONA The contribution of PAX is a heuristic based technique for abstracting parameterized systems in WSIS into finite state systems for model checking PVS MONA has been integrated into the PVS theorem prover ORO00 Properties express ible within WS1S can then be verified without user interaction ISABELLE The combination of WS1S and higher order logic has been investigated using MONA as a WSIS oracle in the ISABELLE system BF00al MONA 1 4 13 Concepts and algorithms Program verification In JJKS97 the MONA logic is used to encode the effect of executing loop free code with pointer operations on list shaped structures The approach is based on KS94 which employs transductions a form of predicate transformation expressible by an automaton and is extended to code containing loops using classical Hoare logic This technique is generalized to recursive data types in Elg99 To overcome the increased complexity a new logic WSRT Weak monadic Second order logic with Recur sive Types see Section 7 9 is introduced This logic is reminiscent of FIDO and LISA WSRT permits a more efficient decision procedure based on a technique called shape en coding DK S99 an efficient guide can automatically be deduced The newest version of the YakYak tool also uses the WSRT part of MONA In MS00 the t
39. can give an exponential decrease in state space size Experience shows that positional knowledge often arises naturally MS00 7 6 Tree mode output format In the following the format of output of automata satisfying examples and counter examples etc for tree mode is described WS2S formula analysis Executing mona ab2 mona generates amongst other output the following satisfying example which illustrates the WS2S output format A satisfying example is Booleans XX Universe ua 1X 1X 0 1X 0 1X 0 1X 0 000 0 Universe ub X1 X1 X1 X1 0 41 0 1 0 1 0 00 2 02 00 0D First the values from the boolean state space is written in a string None of the free variables in this example are boolean so the string just contains Xs Next for each universe a tree is printed An empty subtree is written as O and a node of the form a lt t1 t2 gt see p 40 is written as o 11 19 s one can see A is assigned a set with 5 elements and B is assigned a set with 7 elements as requested by the MONA program 44 MONA 1 4 7 6 Tree mode output format The satisfying examples and counter examples can be shown graphically using the graphviz tool dot see Section 5 2 For instance executing mona gs ab2 mona gt ab2 sat ex dot dot Tps ab2 sat ex dot o ab2 sat ex ps generates the following output in the file ab2 sat_ex ps which shows the satisfying example from before SATISFYING EXAMPLE Free variables
40. ch is associated the type and variant t r E V which is true iff the tree denoted by the tree variable x at the position denoted by t has type E and is labeled with the E variant V Second order terms are built from second order variables and the set operations union in tersection and difference as in WS1S and WS2S First order terms are built from first order variables and the special WSRT functions tree root r which evaluates to the root of the tree denoted by x and succ t E V C which provided that the first order term t denotes a node of the E variant V evaluates to its C component and is undefined otherwise Tree constants can be expressed using the second order term construct const tree t E consttree where a consttree has the form V Cconsttreey consttreem V is a variant of E and recur sively there is a consttree for each component of V Continuing the example above consider the following extension tree root x root u var2 r alli p p in r lt gt variant p x Tree BLUE amp variant succ p Tree BLUE next x List GREEN empty r First it is stated that the root of x is not located at the root of u Then a second order variable r is declared A position p is in the set denoted by r if and only if its x label is BLUE and the next successor is GREEN for x Finally r is required to be non empty For the full WSRT syntax see Appendix A This logic corresponds to the core of the
41. curs Depending on the parity of x the latter event brings the automaton either into an accepting state or into the universally rejecting state Related issues Section 5 2 explains how to generate drawings of automata as graphs In Section 6 T it is shown how to export automata to be used in other applications 12 MONA 1 4 2 5 What are MONA automata really Ox xx Figure 3 The even mona automaton 2 5 What are MONA automata really The automaton above has 16 24 letters and 10 states Therefore its transition table has 160 entries The MONA representation is a lot more concise than this number would indicate In fact the actual data structure for this automaton depicted in Figure M is an acyclic directed graph with only 35 nodes The graph shown is essentially a multi terminal shared BDD Bry92 HJJ 96 where the leaves are the boxes at the bottom Every MONA variable is associated a unique variable index used for the BDD representation as explained below The internal BDD nodes are round and contain variable indices Each node has a low successor denoted by a dashed arrow and a high successor denoted by a solid arrow In the internal representation automata have three kinds of states accepting denoted with 1 rejecting here denoted with 1 and don t care here denoted with 0 see Section 3 2 All states are described with their accept status in the array shown at the top In this case the only st
42. d 1 of 37 DAG nodes after reduction 103 Time 00 00 00 01 AUTOMATON CONSTRUCTION 100 completed Time 00 00 00 05 Automaton has 11 states and 43 BDD nodes ANALYSIS counter example of least length 0 is 30 MONA 1 4 5 1 Verbose processing satisfying example of least length 4 is Total time 00 00 00 08 The completion percentage shows how many of the automaton operations that are completed along with the number of automata currently in memory and the amount om memory being used All progress information can be disabled using the q option Dumps The d option causes the following information to be printed e the main formula and assertion see Section 3 2 the variable restrictions and all macros and predicates e the contents of the symbol table mainly used for internal debugging purposes e the contents of the code DAG see Section shown expanded as a tree and e in WS2S mode see Section 7 the guide is also printed Statistics The s option makes MONA print some statistics about each automaton operation It prints e the type of the current operation e the location in the source code where the operation originates and e the sizes of the input and the resulting automata if either a product a project or a minimization operation The output looks like Product amp even mona line 12 column 3 amp O in Q 4 4 x 7 14 gt 12 26 Minimizing 12 26 gt 6 11 Right quotie
43. d into five groups e universe branches located in the top of the infinite binary tree with a leaf for each universe variant branches for each type these state spaces form a subtree with a leaf for each variant variant leaves which are the leaves of the variant subtrees component branches for each variant these form a subtree with a leaf for each compo nent and e dummies which act as dummy universes variants and components to ensure a binary fanout In the terminology of DKS99 the variant branches and leaves form the OR trees and the component branches form the AND trees To enable an efficienct encoding of WSRT two special constructs are used tree P which is true iff the second order variable P denotes an instance of a recursive type and sometype 7 which is true iff all positions in the set denoted by T correspond to variant leaves These constructs are also explicitly available in the MONA syntax The d option see Section 5 1 shows the desugared code corresponding to the actual automata operations performed by MONA Furthermore the normal WS2S output style for counter examples and satisfying examples can be forced with option f 50 MONA 1 4 8 Plans for future versions This section describes the major ideas and plans for future work on the MONA project Users of the MONA tool are encouraged to participate in the further development both by contributing with implementation and by suggesting usef
44. ddress is 15 Acknowledgments The following people have contributed to the MONA project either by helping making it or by providing us with useful feedback Abdelwaheb Ayari David Basin Nikolaj Bj rner Morten Biehl Christiansen Rowan Davies Jacob Elgaard Mamoun Filali Jesper Gulmann Henrik sen Jakob Jensen Michael J rgensen Doug Mclllroy Frank Morawietz Mogens Nielsen the late Robert Paige Paritosh Pandya Andreas Potthoff Theis Rauhe Harald Ruess Anders Sandholm Michael I Schwartzbach Tom Shiple Kim Sunesen and Ralf Treinen MONA 1 4 2 Basic features MONA syntax is essentially that of WS1S or WS2S augmented with lots of syntactic sugar and miscellaneous ways of defining the parameters of the compilation The MONA tool runs in either linear mode using the WS1S logic and DFAs or in tree mode using the WS2S logic and GTAs In this section the basic syntax and features concerning linear mode are introduced Tree mode is described in Section 7 A MONA program consists of a number of declarations and formulas which are all ter minated by semicolons The MONA program itself is valid if the conjunction of all formulas is valid In Figure I below an extension of the program simple mona from the introduc tion is shown This program imposes additional constraints on P and Q it also introduces a first order variable x which denotes some natural number and a boolean variable A We write varO A to declare A since boolea
45. defined by a set of recursive equations of the form type Ej Vi C14 Eja yaua Cimi Ejim 5 Va Ch MES TENE Cn mn DES n mn Each E is the name of a type each V is called a variant and each C is called a component type contains a number of variants each containing a number of components and each component is associated a type An instance of a recursive type E is a finite labeled tree its root is labeled with a variant V from E and it has a successor for each component C in V such that the successor recursively constitutes an instance of the type of C The WSRT logic Formulas in WSRT are interpreted over a set of tree structures each universe declaration of the form universe u E corresponds to a tree Each node in such a tree is associated a type The type of the root is given by the universe declaration Each outgoing edge corresponds to a component of a variant of the type of the node T he type of a non root node is the one associated to the component corresponding to its incoming edge In other words the tree is given by unfolding the recursive type Such a tree is infinite if the type contains recursion As in WSIS and WS2S a WSRI first order variable denotes a single node and a second order variable denotes a finite set of nodes tree variable declared by tree u1 uk P optionally with a where formula denotes a non empty subset of nodes in the universes Uis uk and a labeling of these
46. e In Computer Science Logic CSL 97 volume 1414 of LNCS 1998 Nils Klarlund A theory of restrictions for logics and automata In Computer Aided Verification CAV 99 volume 1633 of LNCS 1999 Nils Klarlund Anders M ller and Michael I Schwartzbach MONA implementa tion secrets In Fifth International Conference on Implementation and Application of Automata CIAA 00 LNCS 2000 77 KNS96a KNS96b KR 96 KS93 KS94 KS99 Lon98 MC97 Mey75 MS00 Nil99 ORO0 Pan99 Pan00 Nils Klarlund Mogens Nielsen and Kim Sunesen Automated logical verification based on trace abstraction In ACM Symposium on Principles of Distributed Computing PODC 96 1996 Nils Klarlund Mogens Nielsen and Kim Sunesen case study in automated verification based on trace abstractions In M Broy S Merz and K Spies editors Formal System Specification The RPC Memory Specification Case Study volume 1169 of LNCS pages 341 374 Springer Verlag 1996 Nils Klarlund and Theis Rauhe BDD algorithms and cache misses Technical re port BRICS Report Series RS 96 5 Department of Computer Science University of Aarhus 1996 Nils Klarlund and Michael I Schwartzbach Graph types In 20th Symposium on Principles of Programming Languages POPL 93 ACM 1993 Nils Klarlund and Michael I Schwartzbach Graphs and decidable transductions based on edge constraints In Trees in Algebra and Prog
47. e based on a syntactic analysis that attempts to identify valid subformulas and equivalences among subformulas Formula reductions are by default enabled option 00 causes this translation phase to be skipped MONA performs three kinds of formula reductions 1 simple equality and boolean reductions 2 special quantifier reductions and 3 special conjunction reductions The first kind can be described by simple rewrite rules only some typical ones are shown X X true p amp o true amp q 770 o false amp false false true These rewrite steps are guaranteed to reduce complexity but will not cause significant im provements in running time since they all either deal with constant size automata or rarely apply in realistic situations Nevertheless they are extremely cheap and they may yield small improvements in particular on machine generated MONA code The second kind of reductions can potentially cause tremendous improvements As men tioned the non elementary complexity of the decision procedure is caused by the automaton projection operations which stem from quantifiers The accompanying determinization con struction may cause an exponential blow up in automaton size The basic idea is to apply a rewrite step resembling let reduction which removes quantifiers ex2 X O T X provided that q gt X T is valid and T is some term satisfying FV T C FV where FV denotes the set of free variabl
48. e sets can be expressed For instance one could not have specified the set of even numbers as EVEN in var2 EVEN 0 in EVEN amp alli p p in EVEN lt gt p 1 notin EVEN 10 MONA 1 4 23 Analyzing formulas A few constructs need further explanation e The value of t I where t is a first order term and I is a constant integer expression is 0 if the value of t is less than that of I The value of t I to and t I to where ty and to are first order terms and I is a constant integer expression is not defined if tj gt tg So in that case the MONA programmer should not assume anything about the value of the term otherwise the result is the expected one Allowing arbitrary modulo calculation would make the logic undecidable The value of min T and max T where T is a second order term is 0 if T denotes the empty set 23 Analyzing formulas When MONA is run on even mona the following analysis is printed counter example of least length 1 is P XX Q X X X X1 A OX P Q x 0 A false A satisfying example of least length 7 is P X 1110100 Q X 000X0XX x X 0000001 A 1 XXXXXXX P 0 1 2 4 Q 0 x 6 A true Let us look deeper into the issue of example generation MONA calculates a program au tomaton which is the minimum deterministic automaton whose language is the set of strings that interpret the global variables such that the conjunction of all formulas in the prog
49. e used in two ways e to model parameterized systems and verify a whole family of finite systems at once or e to model discrete time and verify safety properties or synthesize controllers Similarly the tree logics WS2S and M2L Tree can be used to model tree shaped systems or branching time instead of linear time These ideas have led to a whole branch of research Another kind of application is to reduce other logics to the MONA logics Hardware verification One of the first MONA applications was hardware verification In BK98 the ideas of modeling parameterized systems or discrete time were introduced In this verification technique is further described and generalized to trees Many of the applications mentioned below also build on these ideas Controller synthesis As mentioned M2L Str can be viewed as a temporal logic that is as a logic modeling the occurrence of events over time In Tho90 it is shown how PLTL Propo sitional Linear Time Logic can be encoded in M2L Str To synthesize run time controllers MONA turns requirements of Web services or Lego robots into automata which may act as programs Whenever a process a Web session or a Lego robot wishes to pass certain checkpoints it is ensured that doing so is allowed by the automata in the sense that reject states are not entered FIDO FIDO is a high level language built on top of MONA It helps the programmer overcome the low level bit encoding usually required whene
50. echnique is further generalized to cover the whole class of data structures that can be described as graph types KS93 As an example the technique is used to verify that an implementation of the insert procedure for red black search trees preserves the non arithmetical part of the red black invariant This manual describes two additional example applications In Section it is shown how the MONA representation of certain queue structures specializes to those suggested elsewhere in the literature and in Section 6 6 it is explained how regular expressions over the ASCII alphabet can be effectively encoded in MONA making WS1S a much more versatile notation for patterns than regular expressions 13 Concepts and algorithms For more information about the development of MONA we suggest the following papers which describe the concepts and algorithms applied in the tool Mona Monadic Second Order Logic in Practice The first paper on the imple mentation of monadic second order logic on finite strings Data structures algorithms and an application to verification of safety and liveness properties of a parameterized distributed system are discussed BDD Algorithms and Cache Misses KR96 A description of techniques for speeding up BDD operations By rethinking data structures for BDD algorithms random memory access can be reduced Algorithms for Guided Tree Automata BKR97 Introduction of Guided Tree Automata as a technique for co
51. ed manually in the MONA programs Preliminary experiments have shown that useful ordering rules often are of the form P should have a higher index than Q or the indices of P and Q should be close to each other perhaps more reasonable approach is to attempt to find a good variable ordering auto matically using heuristics Many such techniques are known for other applications of BDDs see e g BRKM91 We plan to investigate whether these or similar techniques could be useful for MONA 8 2 Heuristic reductions The formula reductions carried out by the current version of MONA are chosen such that they cannot have a negative impact on the automaton sizes see Section 4 2 This technique gives a predictable behavior but it also precludes a number of interesting optimizations For instance in the formula Pi amp do amp da 51 MONA 1 4 8 3 Encoding of boolean variables in tree mode the sizes of the intermediate automata vary significantly according to whether the first or the second product operation is performed first In general the best choice cannot be determined without trying both of them however a heuristic approach might be usable We will examine this in a future version 8 3 Encoding of boolean variables in tree mode The boolean variable encoding in trees often leads to exponential explosions since the tree automata can work under no assumptions about what the boolean values are in the top This phenonomen does
52. ee 48 counter example Bl DAG 26 29 debugging 29 decidable logic declaration 8 defaultwhere DFA 11 61 dfalib discrete time 4 don t care 21 33 execute 32 export 32 bi external format 80 FIDO 4 first order variable flattening 7 formula graph representation 26 BI 44 58 graphviz 58 GTA Guided Tree Automaton 67 gtalib guide 42 import 32 57 in state space index 12 13 26 inherited acceptance integer constants 9 language let 9 linear mode 8 38 local variable M2L Str 35 m21 str 35 M2L Tree m21 tree 46 macro 13 max 9 min 9 10 minus modulo 9 10 negation operators 9 55 parameterized systems parameterized verification 4 precedence 55 predecessor predicate 13 prefix Presburger arithmetic 33 65 product operation program program automaton project operation 20 quantification Queue BDD 14 quotient operation 20 recursive types 46 reduction regular expression 35 regular language restrict restriction 22 24 33 38 root SIS T9 satisfying example second order variable semantics 9 separate compilation 28 signature equivalence sometype 49 source code 7 succ 48 successor 38 temporal logics 4 terms 9 timing translation I7 tree 47 49 tree logic 38 tree mode tree roo
53. eing non empty i e a string which assigns an empty set to a first order variable is categorized as don t care This is enforced by the automaton constructed by the function dfaFirstOrder and by the function dfaRestrict described below The initial state in any basic automaton is a don t care state which reflects the property that at least the first string symbol representing boolean variables must be read to determine acceptance The function dfaAllPos constructs an automaton which is in an accept state unless a 0 has been met on the track belonging to P in which case it is in a don t care state This automaton is used for the allpos construct see Section 6 5 The function dfaLastPos constructs an automaton which while reading a string encoding the value of P is in a don t care state if a 1 on the track belonging to P has not 62 MONA 1 4 DFA function MONA formula dfaTrue dfaFalse dfaConst int n int i dfaLess int 2 int 7 dfaLesseq int int j dfaPlusi int int j int n dfaMinusi int 7 int 7 int n dfaEqi int 7 int 7 dfaEq2 int 7 int 7 dfaPlus2 int int j dfaMinus2 int 7 int 7 dfaPlusModuloi int 2 int j int k 1 Pk dfaMinusModuloi int int j int k pj 1 pe dfaEmpty int 1 empty dfaIn int 7 int 7 in Pj dfaSubset int 7 int 7 Sub P dfaUnion int 2 int j int k Pj union P dfaInter int i int j int k
54. elonging to the chosen variable decodes the base 2 encoded value and prints it As an example running MONA on the following program var2 X export test dfa X pconst 42 and then executing presburger analysis test dfa X gives the following reply satisfying example X 42 66 MONA 1 4 D 1 Examples Presburger arithmetic and transduction The example program Examples presburger transduction c illustrates the use of the functions dfalmport dfaProduct dfaMinimize dfaRightQuotient dfaProject dfaRe placeIndices and dfaPrintGraphviz It also illustrates the first method mentioned above for constructing automata and shows how to perform automaton transductions iteratively The program constructs the automaton for a Presburger encoded constant by starting with an automaton for the relation P 1 and then iteratively performing a transduction which adds one to the constant a given number of times The resulting automaton is the same as the one explicitly constructed by dfaPresbConst the purpose of this program is merely to illustrate the techniques The Presburger addition automaton used in the transduction is made using the MONA program Examples presburger mona See the source of the program for further description 67 MONA 1 4 E The MONA GTA package This appendix describes the GTA package of the MONA source The interface is contained in the file gta h The package depends on the BDD package described in Appendix
55. en Rasmussen Symbolic model checking using monadic second order logic as requirement language Master s thesis Technical University of Denmark DTU 1999 IT E 821 SK99 Mark A Smith and Nils Klarlund Verification of a sliding window protocol using IOA and Mona 1999 Submitted for publication SKR98 Thomas R Shiple James H Kukula and Rajeev K Ranjan A comparison of Presburger engines for EFSM reachability In Computer Aided Verification CAV 98 volume 1427 of LNCS 1998 S898 Anders Sandholm and Michael I Schwartzbach Distributed safety controllers for Web services In Fundamental Approaches to Software Engineering FASE 98 volume 1382 of LNCS 1998 Tho90 Wolfgang Thomas Automata on infinite objects In J van Leeuwen edi tor Handbook of Theoretical Computer Science volume B pages 133 191 MIT Press Elsevier 1990 TW68 James W Thatcher and Jesse B Wright Generalized finite automata with an application to a decision problem of second order logic Math Systems Theory 2 57 82 1968 Several of the articles are available from http www brics dk mona papers html 79 Index d 30 e f 49 gd gu BI h i 31 o q s E u w XW allpos analysis IO 43 assert associativity automaton BDD binary decision diagram boolean variable 8 22 cache 6 command line usage 56 comments 8 complement operation 20 conjunction const tr
56. en mona has been rewritten such that the even property is expressed as a predicate MONA is sometimes able to reuse the automaton for a predicate During compilation MONA simplifies predicate invocations so that each actual parameter always is represented by a single variable For example even x 1 is internally rewritten to ex1 t t x 1 amp even t where t is a fresh variable If a predicate is used twice where the variable indices of the actual parameters and free variables are ordered similarly then MONA is able to reuse the automaton In even with pred mona we could add more uses of the even predicate while no recompilation of it would be necessary since the predicate has only one free variable so the variable ordering is trivially unchanged Semantically there is no difference between macros and predicates but the automata theoretic calculations performed during their compilation may be very different As a rule of thumb Use a macro if the formula to be parameterized is small and a predicate otherwise Related issues Section A 1 describes the general technique for automatic reuse of intermedi ate results Section 4 3 shows how predicates can be used for managing automaton libraries 2 7 Example Reasoning about queues In this example we show how MONA can be used to carry out parameterized verification The example is inspired by GL96 where a data structure that is a hybrid between an automaton and a BDD was proposed
57. ences 3 1 The classical approach The central idea in the classical approach is to recursively translate each subformula of a main formula do into a deterministic finite state automaton that represents the set of satisfying interpretations The approach can be presented as follows Simplifying the language Before the actual translation takes place some syntactic transformations of dp are performed e First order terms are encoded as second order terms since a first order value can be seen as a singleton second order value Also we may encode booleans in a variety of ways but for simplicity we assume here that strings start with position 0 as opposed to the actual encoding explained previously All second order terms are flattened by introducing variables that contain the values of all subterms Example A B union C inter D is reduced to ex2 V A V inter D amp V B union C where V is a fresh variable e The subformulas are rewritten to involve fewer kinds of operations Example a112 A is reduced to ex2 A 49 Consequently it can be shown that do can be massaged into a form where atomic subformulas those without boolean connectives or quantifiers express either a subset a set difference or a successor relation and where each logical operator expresses either a negation a conjunction or an existential quantification The abstract syntax for simplified WS1S formulas can be defined by the following gramma
58. er the alphabet X written t Ty can be defined by the grammar t se e or where e denotes the empty tree a X and t and t are the left and right subtrees of t respectively A guide G D u do is a top down deterministic tree automaton that does not look at the labeling Its states will be used to designate state space names of bottom up automata More formally G consists of D a finite set of state space names p D Dx D the guide function and do D the initial state space name A Guided Tree Automaton GTA Mg with guide G is a set of bottom up tree automata Ma Qa aen Y a aeD da ae p F where Qaae p is a family of disjoint finite sets one set for each state space name Mis the alphabet da aep is a family of transition functions one for each state space name such that if ud di do then dg is of the form dg Qu x Qaz 3 Qa Walaep is the family of initial states one for each state space name such that Ja Qa for each d and F C Qa is the set of final states Given a tree t and a GTA Mg we define whether Mq accepts t by a two step process 1 First a state space is assigned to each node in t Let Tipp denote the set of trees defined by the grammar Pos d edi where a X and d D The bottom up tree automaton distinguishes between different empty subtrees thus the need for the leaf of the form d above The tree t can now be labeled w
59. es For several reasons this is not the way to proceed in practice First of all finding terms T satisfying the side condition can be an expensive task in worst case non elementary Secondly the translation into automata requires the formulas to be flattened by introduction of quantifiers such that there are no nested terms So if the substitution 9 T X generates nested terms then the removed quantifier is recreated by the translation Thirdly when the rewrite rule applies in practice usually has a particular structure as reflected in the following more restrictive rewrite rule chosen in MONA ex2 X 9 O X X provided that 2 amp Xi Xj amp and X is some variable other than X In contrast to equality and boolean reductions this rule is not guaranteed to improve perfor mance since substitutions may cause the DAG reuse degree to decrease The third kind of reductions applies to conjunctions of which there are two special sources One is the formula flattening just mentioned the other is the formula restriction technique mentioned in Section 3 2 Both typically introduce many new conjunctions Studies of a graphical representation of the formula DAGs as explained in Section have shown that many of these new conjunctions are redundant typical rewrite rule addressing such redun dant conjunctions is the following d amp Q9 d provided that nonrestr 2 C nonrestr 1 U restr o1 and restr 9 C re
60. essing and the resulting automata Section 6 contains a description of more advanced constructs which allow you to control variable restrictions import and export automata emulate Presburger arithmetic and more To learn about the WS2S part of MONA turn to Section 7 Our future plans for the MONA project are described in Section 8 If you want to extend MONA you may consult the appendices to find a detailed description of the MONA DFA GTA and BDD packages Also look in the appendices for detailed accounts of MONA syntax and command line usage What s new in version 1 4 This manual describes MONA version 1 4 as released September 2000 It is a revised edition of the version 1 3 manual updating the survey of related work and adding documentation of the newly implemented features recursive types for the tree logic part see Section 7 9 and formula reductions Section 4 2 Furthermore a number of minor modifications and improvements have been made detailed list of changes to the tool can be found on the project Web site Availability The complete UNIX Linux Solaris SGI C C4 4 source code for MONA version 1 4 is avail able under the GNU General Public Licence Please visit the MONA Web site at http www brics dk mona for further information All bug reports ideas for future versions and other comments are appreciated We are always interested in hearing about applications and extensions of the MONA tool Our email a
61. from position p to position q including the p th letter but not the q th belongs to the language defined by E Finally we remember to declare as an allpos variable such that it is removed from the final automaton The details can be found in Figure D It can been seen to be essential that the default restrictions allow values higher than the largest element in the string otherwise the induction would be much more cumbersome to express EEE EE O x ooooon xokoooor KM MM HOOF KM KM KHOR XxX x KM KM KR MOO xxxxxoo XxX orHoooor Pd pe pe DS de pe pe pe xxxxHoor x MK MRO XX e XXX xxx o x Figure 8 Regular expression over ASCII alphabet The resulting automaton is shown in Figure 8 It can be seen that the representation of intervals like a z would be very efficient by the approach just sketched Thanks to the BDD representation any interval on which the transition relation remains constant for a given state introduces at most sixteen nodes but on average only eight nodes Also the regular expressions can easily be extended with complementation and conjunction Thus MONA should be a useful tool for the construction of automata for pattern matching via more concise formalisms than regular expressions 37 MONA 1 4 6 6 Example Regular expressions over the ASCII alphabet var2 where ex1 p where true p notin amp allpos defaultwherel p alli r r lt p gt r in
62. graphviz format if in tree mode See Section 7 6 gc Output counter example tree in graphviz format if in tree mode See Section 7 6 gd Output DAG in graphviz format See Section 4 1 xw Output resulting automaton in external format See Section 6 1 The MONA package includes a man page that also describes these command line options 57 MONA 1 4 C Using automaton files in other applications Appendices D E and Flshow the interfaces to the DFA GTA and BDD packages used inside MONA These packages allow advanced operations on the very efficient but also complex internal representation of automata This appendix describes the format of DFA and GTA files used by import and export see Section 6 1 and some simple libraries for reading and writing such files in other programs If MONA is used as an automaton construction tool these libraries can provide a very simple way of using the automata in other applications The libraries do not require linking any of the MONA code into the applications and they use less memory than the representation MONA uses internally C 1 Using DFA files Format of DFA files The external file format used by import and export in linear mode see Section 6 1 is BDD representation plus some auxiliary information written in ASCII For instance running MONA on var2 P Q export test dfa P sub Q yields the following contents of test dfa MONA DFA number of variables 2 variables P Q
63. h of the given string This restriction is not a WS1S concept because of the closure properties just mentioned From the language point of view M2L Str corresponds exactly to the regular languages all formulas correspond to automata and vice versa This properties make M2L Str preferable for some applications e g SS98 However the fact that not all positions have a successor often makes M2L Str rather unnatural to use Being closer tied to arithmetic the WS1S semantics is easier to understand Also for instance Presburger Arithmetic can easily be encoded in WSIS see Section whereas there is no obvious encoding in M2L Str The standard decision procedure for M2L Str is almost the same as for WSIS see Sec tion 3 only slightly simpler the quotient operation before projection is just omitted However with restrictions Section 3 2 M2L Str can be emulated efficiently in WS1S pro vided that a single extra basic operation allpos is added to the logic for breaking the closure properties mentioned above We turn MONA into M2L Str mode if we write m2l str in the top of a MONA program This declaration is just an abbreviation for wsis var2 where exi p where true p notin amp p 1 in allpos defaultwhere1 p p in defaultwhere2 P P sub The restriction associated to ensures that always has the value 0 n 1 for some n The defaultwhere declarations restrict all variables to The non WS1S c
64. he values of P For example ex2 X where X sub 9 S p restricts X so that the formula is compiled under the restriction p X C Of course the automaton for is equivalent to the one calculated as ex2 X X sub amp 9 However our intention with a restriction is that it should be implicitly conjoined to any subformula mentioning P To do this we assume again that all formulas are subformulas of a main formula do We focus on the simplified syntax but we change the rule for existential quantification to Q ex2 P where p 9 Let p P p be the restriction of variable P We assume that each P is restricted possibly to the formula P P which is a way of writing true in the simplified logic The ternary semantics Under the binary semantics a formula is either true or false for a given interpre tation MONA semantics defines a third possibility that the formula is don t care 1 if the restriction of some free variable in is not fulfilled As an example consider the following MONA program var2 where 0 5 vari p where p in p gt 5 The status of 9 p gt 5 under the interpretation p i is L if i gt 5 and 0 for i lt 5 In particular p gt 5 is not satisfiable under the conjunction of the restrictions for p and It is shown in how this notion yields a robust semantics variables can be con strained where they occur and the meaning of constraints is preserved u
65. here the left state space of d has lsize states and the right state space of d has rsize states The array indices of length num contains the indices of the free variables void gtaAllocExceptions SsId 1 SsId r unsigned n allocates n exceptions for state pair 1 7 in current state space void gtaStoreException unsigned s char path stores next exception go to state s on BDD path path instead of going to the default destination void gtaStoreDefault unsigned s sets the default destination to state s void gtaBuildDelta State initial constructs transitions for current state space with initial state initial GTA gtaBuild char statuses constructs automaton prepared by the previous func tions using the statuses array as state statuses The following pseudo code shows how these functions are used gtaSetup number of states in root state space for each state space s do gtaSetupDelta s size of left s s size of right s s index array number of indices for each state pair lr do gtaAllocExceptions l r number of exceptions gtaStoreException some state some path repeat gtaStoreException for each exception gtaStoreDefault default destination state end gtaBuildDelta initial state end gtaBuild state status array Automaton operations The following GTA operations are available void gtaFree GTA a deallocates the memory used to store a including the BDD man ager void gtaNegati
66. iable h of type bdd handle the value of the last handle The macro BDD ROOT bddm handle looks at the BDD pointer corresponding to handle Sequential mode It is possible to use the BDD manager in a sequential mode where nodes are not hashed This is useful when it is known that any node inserted is a new one Such a situation may occur when a BDD is read from a file or when the apply product of two BDDs is performed with a leaf function that form pairs In these cases BDD nodes can be inserted sequentially When table is doubled nodes do not change position thus for sequential insertions bdd ptr is not volatile Sequential and hashed modes cannot be combined Basic operations The find_node operation locates a BDD node if it already is known to exist hashed mode only or creates a new node In hashed mode there are two variations of the find node operation both add the current value of the BDD pointer to the bdd roots list and they differ only in whether this pointer is returned as a result or the handle is returned There is also a more primitive version that as parameters take a list of bdd ptrs and an update fn as discussed above 74 MONA 1 4 The apply operations The unary apply operation has the following declaration bdd ptr bdd applyi bdd manager bddm bdd ptr p bdd manager bbdm m unsigned applyl leaf function unsigned value Here bddm is the manager that holds the BDD on which the apply operation is car
67. ich are automatically updated when the node table is doubled An offset into this array is called a bdd handle The BDD package guarantees that the pointer described by a handle always denotes the same BDD node The apply operations augment automatically the bdd roots array to contain the result of the operation Some of the basic operations do not use the bdd roots list but can be given a user defined list whose pointers are updated in the case that the table is doubled Such lists are declared and manipulated using the SEQUENTIAL LIST macros which enable lists with pop and push operations to be efficiently implemented as dynamically allocated arrays Basic operations that allow updating of lists also can be given a pointer of type void update fn unsigned new place unsigned node The denoted function takes as argument a function new place The basic operation calls update fn when the table is doubled and it supplies the function new place which specifies the new pointer value of a BDD node given the old value Manipulation of bdd roots The macro BDD ADD ROOT bddm p adds a BDD pointer p to the bdd roots list of the BDD manager bddm The macro BDD LAST HANDLE bddm can be used after a BDD ADD ROOT bddm p application to get the handle of the bdd roots list where the BDD pointer to the node currently designated as p is stored For convenience BDD ADD ROOT SET HANDLE bddm p h combines the two preceding operations and assigns the var
68. imum automaton recognizing the set of satisfying interpretations The command mona simple mona produces the automaton analyzes it and generates the following output A counter example of least length 0 is P X Q X Fed Q A satisfying example of least length 5 is P X 11101 Q X 000X0 P 0 1 2 4 Q 4 This analysis tells us that a counter example to the formula is obtained by interpreting both P and Q as the empty set MONA has also calculated a satisfying interpretation namely P 0 1 2 4 Q An Xin a string means either O or 1 The columns with the two Xs are used for boolean variables of which there are none in this example 12 MONA applications A substantial number of applications of MONA have been published Also MONA has suc cessfully been integrated into or used as foundation of a number of other tools MONA has 4 MONA 1 4 12 MONA applications gained lots of attention recently thus more than 10 of the publications referenced in the following small survey have been published during the last year In an application perspective arithmetic and logic is useful because interesting systems and properties can be encoded common observation is that WS1S and the related logic M2L Str see Section 6 5 can be viewed as generalizations of quantified propositional logic adding a single unbounded dimension orthogonal to the dimension bounded by the number of variables This unboundedness can b
69. ion from A to RA is explicitly available in the MONA syntax in the form of the restriction operator od n restrict d If A is the automaton generated for then RA is the automaton generated for restrict An example Consider the atomic formula p in P in the full MONA syntax If there are no restrictions introduced by where or defaultwhere clauses then the automaton for p in P is formed as the product of e an automaton that calculates a value that is either or 1 according to whether the singleton property holds for the p track and e the basic automaton for p sub P where p is regarded as a second order variable This automaton looks like 0 x i 0 L 3 Q S i 3 where we assume that the variable number of p is 1 and that of P is 2 A complete description of the restriction constructs in MONA is given in Section 6 4 Requirements on restrictions The ternary semantics will not provide meaningful results unless the following requirement holds for all formulas of the form ex2 P where p q E ex2 D p P 25 MONA 1 4 3 2 The MONA approach That is for any interpretation that defines the values of all free variables except for P in the closure p P of P there exists an interpretation of P that makes the closure hold For example ex2 P where P P P P does not satisfy this requirement since the restriction is always false Indeed there is a problem here the form
70. ion of the decision procedures for WS1S and WS2S is possible Efficient here means that the tool is fast enough to have been used in a variety of non trivial settings MONA translates WS1S and WS2S formulas into minimum DFAs Deterministic Finite Automata and GTAs Guided Tree Automata BKR97 re spectively The automata are represented by shared multi terminal BDDs Binary Decision Diagrams HJJ 96 Version 1 4 of the MONA tool is several orders of magitude more efficient than the first experimental versions due to techniques such as BDD representation DAGification and for mula reductions In addition MONA provides many features such as three valued logics and automata automaton visualization importing and exporting of automata and recursive types 11 Introductory example We introduce MONA through a tiny example showing its basic functionality MONA is run on a file that defines a WS1S or WS2 formula The result of the compilation is an automa ton which can be used in any way the MONA programmer might desire Often however the interest in the compilation is the analysis that MONA can carry out on the calculated 1A regular language is a set of finite strings recognized by a finite state automaton We assume that the reader is familiar with automata theory as taught in undergraduate computer science courses A logic is decidable if an algorithm exists that determines for any formula its truth status valid formula is alw
71. ional knowledge Examples are shown in Sections and 7 3 Specifying the guide In addition to the essential tree mode operators MONA also contains syntax for specifying the guide and for restricting variables to specific state spaces The guide is defined in the header with the guide construct s an example guide a gt b c b gt d e c gt c c d gt d d e gt e f f gt f f defines a guide with state space names a f the guide function which maps a to b c etc and with a the first name in the list as name of the initial state space The initial state space is also called the boolean state space since it is reserved for the interpretation of the boolean variables just as the very first position in the strings in linear mode is reserved for boolean variables Universes universe u is a subtree of the infinite binary tree satisfying the property that if the position pis in u then both the left and the right successors of p are also in u universe can thus be identified by a string of Os and 1s representing the sequence of left and right successors leading from the root of the infinite binary tree to the root of the universe universe u has associated to it the set of state spaces D reachable from the root of u a state space d is in D if and only if there is some tree containing a node in u that is assigned state space d We assume that the infinite binary tree is covered with disjoint universes in the fo
72. ise Note that restrictions are only associated to variables not to terms in general However if a subformula evaluates to don t care that value propagates to enclosing formulas as explained in Section 34 MONA 1 4 6 4 Restriction Default restrictions It is possible to specify default user definable restrictions using the constructs defaultwhere1 p q and defaultwhere2 P q For instance defaultwherel x x lt 7 is equivalent to specifying where p lt 7 for each first order variable p that does not already have an explicit where restriction First order variables are always implicitly associated an extra restriction of being non empty as mentioned in Section 8 2 The default restrictions do not apply to variables declared within the default declarations Explicit restriction and global assertions To better take advantage of the ternary semantics programmers may use the formula level construct restrict Q to turn false into don t care More precisely if evaluates to false restrict 9 evaluates to don t care otherwise it evaluates to the same as Internally in MONA all uses of re strictions are reduced to such primitive restrict operations The operation is implemented by converting reject states into don t care states in the automaton corresponding to q and minimizing the result Often the MONA programmer wants to analyze a whole program under certain assumptions For instance if a program co
73. ith state spaces in a top down style by applying the function i Ts x D gt Tis pj to t do where fi is defined by fls d d fi a lt ti t2 gt d a d lt A t1 di t2 do gt where u d di d2 Notice that the state spaces are assigned independently of the labels in t 2 Next each subtree of the resulting tree fi t do is assigned a state in a bottom up style by the function 6 Tipp gt Ugep Qa defined by d qq 0 a d lt ty 127 da 0 t1 0 t2 a The language recognized by Mg is the set of trees t Ty such that o fi t do F A GTA can be seen as an ordinary tree automaton where the state space has been factorized according to the guide GTA with only one state space is thus just an ordinary tree automaton The above definition of Guided Tree Automata follows and does not take the ternary semantics into account T his means that states in the root state space which in the 40 MONA 1 4 7 3 Specifying the guide definition above are partitioned into final and not final are actually partitioned into the three kinds accepting also called final rejecting and don t care All definitions results and operations generalize accordingly Factorizations using a guide may avoid state space explosions If one has certain knowledge or heuristics about locations of independent information in the binary tree then a guide may sometimes be constructed that express these features as posit
74. l state 0 initial state 0 0 0 0 1 1 0 1 1 0 0 0 1 iei a e o It shows the three state spaces there are three because the example uses the first method for specifying guides and universes described in Section 7 3 that is no explicit guide or universes For each state space there is an array of state pairs each with a pointer to a BDD node The numbers in parentheses in the leaves in the root state space named lt hat gt are the state kinds 1 reject 0 don t care 1 accept It can be seen that a tree gets accepted if every position belonging to the univ state space is in state 0 This occurs if and only if whenever the variable with number 0 P has a 1 at one of these positions so has the variable with number 1 Q In other words the automaton does accept the language belonging to the formula P sub Q as stated in the MONA file 61 MONA 1 4 D The MONA DFA package This appendix shows how to use the full finite state automaton package of MONA without going through the front end The package is located in the DFA subdirectory of the source package The interface allows the user to directly construct basic automata perform all automaton operations and to import export analyze and draw automata The whole interface to the package is contained in the file dfa h Note that the package depends on the BDD package see Appendix F Section D 1
75. llocated for the result manager Also it is important to kill and recreate the cache whenever a new apply or project operation is carried out Only if the new operation is identical same leaf function or same index that is projected on may the cache be reused When the node table is doubled the result cache is also doubled The BDD package allows two cache doubling policies either the new cache can be erased or the BDD pointers in the cache may be rehashed Experiments indicate that the former policy is the faster one Examples The program Examples bdd_example c in the MONA source package shows an application of the BDD package including the gathering of very detailed statistics The file Examples bdd volatility shows how to use the hashed version of find node in a setting where the program stores BDD pointers in global and local variables 75 References ABF99 ABP98 BC96 BF97 BF00a BFOOb BK 98 BKR97 BRKM9I Bry86 Bry92 BSBLOO Biic60a Abdelwaheb Ayari David Basin and Stefan Friedrich Structural and behavioral modeling with monadic logics In IEEE International Symposium on Multiple Valued Logic IEEE Computer Society 1999 Abdelwaheb Ayari David Basin and Andreas Podelski LISA A specification language based on WS2S In Computer Science Logic CSL 97 LNCS 1998 Alexandre Boudet and Hubert Comon Diophantine equations presburger arith metic and finite automata
76. llowing sense Along every infinite path defined by the guide starting from the root exactly one universe is eventually reached Furthermore we require that D and D are disjoint whenever u and v are distinct universes And as a final requirement all state spaces must be reachable from the root of the infinite binary tree by the guide This scenario can be depicted by the following example illustrating a division of the in finite binary tree into three universes u1 u2 and u3 identified by the strings 00 01 and 1 respectively and some nodes in the top that are not part of any universe The state spaces associated to the universes are as follows assuming the guide defined above 41 MONA 1 4 7 3 Specifying the guide Du d Da e f Dug c MONA allows the user to define these universes by the declaration universe u1 00 u2 01 u3 1 Since the boolean state space must be separate from the state spaces belonging to universes there must be at least two universes Using state spaces and universes The user can declare variables to range over values in only certain universes For instance vari ui x ex2 u2 u3 Y Z declares that x is interpreted as a node in u1 and that Y and Z are interpreted as subsets of the union of the universes u2 and u3 The semantics of assigning a set of universes to a variable is seen from an automaton point of view that positions outside these universes are ignored at the t
77. lts are written in dot format instead of the usual textual format boolean gtaCalcInheritedAcceptance GTA a performs the inherited acceptance analyses described in Section If the result is stored the variable r then r d pl s where d is a state space number p is a state and s is either 1 0 or 1 is non zero if and only if there is a labelled tree that makes the GTA enter a state at the root node that has status s and enter the state p in a node assigned to state space d void gtaFreeInheritedAcceptance boolean a deallocates the memory allocated by gtaCalcInheritedAcceptance void gtaPrintVitals GTA a prints the number of states and BDD nodes for each state space and the total number of states and BDD nodes 71 MONA 1 4 void gtaPrint GTA a unsigned indices unsigned num char names int inherited acceptance prints a textual description of a as shown in Section 7 6 If inherited acceptance is non zero the results of a inherited acceptance analysis are also printed void gtaPrintVerbose GTA a prints a verbose textual description of a Exporting and importing int gtaExport GTA a char filename char names int orders SSSet ss exports a to the file named filename in the format described in Appendix C 2 The null terminated array names contains the names of the free variable orders contains the orders 0 boolean 1 first order 2 second order and ss is the state space sets
78. maton A is the automaton product A x A of the automata for the subformulas In MONA only the reachable product states pairs of the form s s where s and s are states of A and A are calculated Usually this set is much smaller than the product state space ex2 P amp Intuitively the desired automaton A acts as the automaton A for q except that it is allowed to guess the bits on the P track Let A be the result of such an automaton theoretic projection operation on A that is A is just a non deterministic version of A where there are up to two transitions possible out of each state on each letter In order to acquire a deterministic automaton A we must further subject A to a subset construction to get A Unfortunately already the A automaton does not quite do the job The problem is that the witness w P gt M may be longer than w However if this is the case then it can be seen that there is a state s in A reachable on w from the initial state such that a final state can be reached from s on a string consisting of letters of the form I Thus it suffices to characterize such states s as accepting before the projection and subset construction are carried out This step can be carried out in linear time by a breadth first backwards exploration of the automaton from final states The subset construction is carried out so that only reachable subset states are calculated In practice this constr
79. maton has 10 states and 33 BDD nodes Transitions State 0 XXXO gt state 1 State 0 XXX1 gt state 2 State 1 XXXX gt state 1 State 2 OXXX gt state 1 State 2 100X gt state 3 State 2 101X gt state 1 State 2 11XX gt state 1 State 3 OXXX gt state 1 State 3 100X gt state 4 State 3 101X gt state 1 State 3 11XX gt state 1 State 9 OXXX gt state 9 State 9 10XX gt state 1 State 9 11XX gt state 9 The u option is described in Section 6 4 The output is read as follows First the free variables are printed in order of declaration Next the initial state the types of the various states and the size of the automaton is shown Finally a list of transitions is printed The list of transitions is specified using a bit vector notation this time horizontally This notation is often exponential in the number of BDD nodes see Section 25 In Figure 3 the automaton is visualized as a drawing in the traditional DFA style Note that from the initial state 0 the first three components of the letter do not matter only the last component corresponding to the A track has any importance If A is false the initial transition brings the automaton to the universally rejecting state 1 Otherwise the automaton attempts to proceed from state 2 to 7 while checking that the set difference of P and Q is 0 1 2 4 Then it counts modulo 2 in the cycle of length 2 while checking the set difference until x oc
80. mbatting state space explosions in tree automata Mona amp Fido The Logic Automaton Connection in Practice Kla98 A survey paper on BDDs BDD represented automata WS1S and WS2S practical techniques for decision procedures and applications of automaton based symbolic reasoning A theory of restrictions for logics and automata Kla99 Description of the mathematical framework MONA uses for handling first order variables and emulation of e g M2L Str in WSIS This framework is also described in Section 3 2 MONA Implementation Secrets KMS00 Overview of the techniques used in the MONA tool The respective effects of the techniques are quantified by experiments on a number of benchmarks These papers are available from the MONA Web site 7 MONA 1 4 1 4 How to use this manual 1 4 How to use this manual Read Section Zlto get started It introduces the basic MONA features for using the WSIS logic and it will be sufficient for many applications To understand the semantic details of the logic and the translation procedure turn to Section 3 It summarizes the classical automaton logic connection for WS1S and explains the three valued automaton concept used in the MONA implementation Section 4 describes the DAG representation formula reduction and separate compilation features which all exist to speed up the processing In Section 5 you will learn various ways of making MONA produce detailed information about the proc
81. mula may easily lead to doubly exponential blow ups KTa99 Instead we would like a general semantic mechanism and a simple syntactic means of safely compiling formulas under such constraints 3 2 The MONA approach MONA uses automata that extend the classical translation in three ways e To address the issues in the classical approach MONA uses the notion of formula restric tions and the ternary partitioning of strings suggested in Kla99 Thus the states of MONA automata are partitioned into three kinds accepting rejecting and don t care as described below e To handle boolean variables efficiently MONA automata read an initial letter that encodes only boolean variables before reading the letters that define first and second 22 MONA 1 4 3 2 The MONA approach order variables This was explained in Section 2 First order values are not encoded as singleton sets as suggested but as non empty sets The value denoted by such a set is interpreted as its smallest number This encoding turns out to be slightly more efficient than the singleton method e larger number of basic automata and boolean connectives are used in order to reduce the overhead of simplifying the formulas WSIS with restrictions We introduce WS1S R a version of the simplified WS1S above where restrictions are now made explicit by the syntax The basic notion is that a variable P can be associated with a restriction p which is a formula restraining t
82. n t care the root of the binary tree left successor of t right successor of t predecessor of t Figure 10 Essential tree mode operators In WS2S the 1 successor notation is replaced with 0 and 1 representing the left and right successor respectively string of Os and 1s can be used as abbreviation for multiple applications of the successor operators e g p 011 means p 0 1 1 The predecessor operator 1 in WS1S has an WS2S counterpart named up Finite sets of positions can be expressed with the same set operators as in WSIS For a formal definition of WS2S we refer to Tho90 7 2 Guided Tree Automata Just as WS1S WS2S is decidable using automata This section formally describes the au tomata used in the MONA decision procedure for WS2S The technical definitions are provided here for completeness they are not crucial for the understanding of WS2S and can safely be skipped at first reading Theoretically normal bottom up tree automata are sufficient for deciding validity and generating counter examples for WS2S However tree automata impose an extra level of com plexity compared to string automata since the transition tables have an additional dimension This makes state space explosions a significant practical problem The MONA solution is to use a special kind of tree automata called Guided Tree Automata GTA which are 39 MONA 1 4 7 2 Guided Tree Automata defined in the following A tree t ov
83. n variables in MONA are regarded as zero th order Variables introduced by var declarations are the free variables of the program They are also called global variables The existentially quantified formula ex2 Q is satisfied if and only if x is an even number since the formula reads there is a finite set Q of numbers such that a for all numbers q where 0 lt q x the membership status of q in Q is the opposite of that of q 1 and b O is in Q The variable Q declared by the existential quantifier is a local variable whose scope is the formula that follows the colon character The formula A amp x notin P states that A is true and that x is not in P The whole program is thus satisfied if PQ 0 1 2 4 A is true and x is even and not in P 2 1 The essential syntax The even mona example illustrates the main points about MONA syntax Note how com ments are inserted using the character comment spanning several lines can be made by delimiting it with and One important restriction is not obvious from the example on the right hand side of a or a sign only a term denoting a constant may occur Thus the term x y is not allowed if y is declared as a variable Without this restriction the logic var2 P Q P Q 0 4 union 1 2 the formula from Section 1 vari x varO A ex2 Q x in Q amp alli q 0 lt q amp q lt x gt q in Q gt q 1 notin Q amp q notin Q gt q 1 in Q am
84. nder the connectives and quantifiers Here we briefly explain the semantics along with its automata theoretic implications 23 MONA 1 4 3 2 The MONA approach Let X be an expression that is X is either a formula or a variable We define p X to be the formula that is the conjunction of all p P where P is free in X or free in p P for some P free in X etc that is BOX PE where P is the least set such that FV X C P and UpepFV p P C P In particular p P is the natural closure of p P p P implies the direct restriction p P and all indirect restrictions p P where Pj appears in the transitive closure of free variables in restrictions We assume that this closure is finite The semantics of the boolean connectives in the three valued interpretation is the usual one augmented with the rule that any boolean formula is 1 if and only if a subformula is L In particular we have the following truth tables Now the three valued semantics is defined as lw v w Io amp gw o w amp o w if IM p w P M 2 ifVM 9 w P M and IM Ju P M ex2 P where p w l ifVM e w P M 1 if wF Pj sub P and p P amp p Pj w Pi sub Pj jw 4 ifw P sub P and p Pi amp p Pj w if p 5 amp p Pj wz where we have only shown one kind of atomic formula since the other ones are treated similarly the meaning of an atomic formula
85. nodes with the following properties 1 the subset forms a connected set of nodes 2 each node in the subset is associated a label which is a variant of the type of that node and 3 for each node in the subset a given child node is also in the subset iff it is associated a component of the variant that the node is labeled with In this way a tree variable denotes an instance of one of the declared recursive types Notice that a node can be labeled with a number of variant labels one for each tree variable The reason for this perhaps non obvious interpretation is that it allows a simple and efficient encoding into WS2S with guides However typically there is only one tree variable per universe and often the root of the tree is restricted to be at the root of the universe As an example showing the concrete MONA syntax for WSRT declarations the following program declares two recursive types Tree and List a universe u of type Tree and a tree variable x whose value is a tree located somewhere in the u universe 48 MONA 1 4 7 9 Recursive types and WSRT ws2s type Tree RED left Tree middle List right Tree BLUE next List type List NULL GREEN next List universe u Tree tree u x A formula is built from the usual boolean connectives first order and weak monadic second order quantifiers and the special WSRT basic formulas type t E which is true iff the the first order term t denotes a node whi
86. nsists of two formulas q and 9 one might want to assert that holds so that any counter example that is printed satisfies q but not MONA provides a method for specifying such assertions The declaration assert 0 is equivalent to restrict q and has the desired effect Unrestriction It is often the case that the user does not want to distinguish between don t care states see Section 3 2 and reject states The option u makes MONA unrestrict the automaton printed with w and all automata generated using export see Section 6 1 Unrestricting an automaton means transforming don t care states into reject states and minimizing the resulting automaton In this way the unrestricted automaton is the minimal automaton accepting the same language as the original 35 MONA 1 4 6 5 Emulating Monadic Second order Logic on Strings 6 5 Emulating Monadic Second order Logic on Strings Any automaton produced by the MONA in its pure linear mode recognizes a language that is closed under certain string operations as described in Section A slight variation on WSIS is called Monadic Second order Logic on Strings M2L Str In WSIS formulas are interpreted over infinite string models but quantification is restricted to finite sets only In M2L Str formulas are instead interpreted over finite string models That is the universe is not the whole set of naturals N but a bounded subset 10 n 1 where n is defined by the lengt
87. nt Projecting 20 even mona line 7 column 1 ex2 Q x in Q 6 11 gt 6 7 Minimizing 6 7 5 6 This can be read as follows the conjunction in line 12 results in a product operation of two automata one with 4 states and 4 BDD nodes the other with 7 states and 14 BDD nodes The product automaton with 12 states 26 BDD nodes and its minimized version are also 31 MONA 1 4 5 2 Visualization of automata reported on and so forth The character points to the column in the source line where the operation originates When the compilation is completed a summary of the use of the various automata oper ations is printed Also the largest number of states and the largest number of BDD nodes of any intermediate minimized automata is shown Timing Using the option t causes MONA to print a summary of the total time CPU time not physical time spent in the main automaton operations If t is used together with s statistics the time spent in each operation is also printed Intermediate automata The i option is intended for use together with s see above It extends the informa tion being printed at each automaton operation with a verbose description of the resulting automaton The following example illustrates the output Resulting DFA Initial state 0 Accepting states 1 Rejecting states 2 Don t care states 0 Transitions State 0 gt state 1 State 1 8 0 10 0 11 0 gt state 1 State 1 8
88. o be able to characterize the states in the other state spaces as well An inherited acceptance analysis infers this information It characterizes a state q in a state space d as can lead to accept if there exists a tree which at some position belonging to d is in state q and that tree gets accepted by the automaton Similarly for can lead to don t care and can lead to reject MONA is able to perform this analysis using the h option It writes the results of the analysis combined with the output from the w option see Section 7 6 As an example mona h ab2 mona 46 MONA 1 4 7 8 Emulating Monadic Second order Logic on Trees produces the following results for the states in state space a Inherited acceptance States leading to reject 3 4 States leading to accept or reject 01256 This shows for instance that if the automaton at some point is in state 3 in state space a at some position it can only lead to reject no matter what the automaton reads further up the tree For an application of inherited acceptance information see DKS99 7 8 Emulating Monadic Second order Logic on Trees Just as WS2S is a generalization of WS1S Monadic Second order Logic on Trees M2L Tree is a generalisation of M2L Str which was briefly described in Section 6 5 M2L Tree can be emulated by writing m2l tree which is the same as writing ws2s var2 where alli p where true p in gt p in p p allpos
89. on GTA a changes accept states to reject states and vice versa void gtaRestrict GTA a changes reject states to don t care states void gtaUnrestrict GTA a changes don t care states to reject states 70 MONA 1 4 Boolean function gtaAND gta0R gtaIMPL gtaBIMPL Figure 16 Product operation modes GTA gtaCopy GTA a creates a copy of a void gtaReplaceIndices GTA a unsigned map replaces the indices in a according to map See dfaReplaceIndices p 64 GTA gtaProduct GTA a GTA a2 gtaProductType mode performs product construc tion according to mode see Figure I6 GTA gtaQuotientAndProject GTA a unsigned index int quotient performs pro jection operation of index index on a If quotient is non zero the right quotient operation is performed before the projection GTA gtaMinimize GTA a returns a minimal automaton accepting and rejecting the same languages as a Analysis and printing Tree gtaMakeExample GTA a int kind generates a satisfying example if kind 1 or a counter example if kind 1 to the formula represented by a The re sulting Tree structure is defined in gta h void gtaAnalyze GTA a unsigned num char names unsigned indices int opt int opt analyses the automaton a and prints the results The arrays names and indices of length num contain the names and indices of the free variables If the flags opt and opi are non zero the resu
90. on MONA It has been used to verify properties of SMV Verilog ESTEREL and SPIN systems YakYak YakYak is an extension of the Yacc parser generator Side constraints expressed in a first order parse tree logic are translated into Guided Tree Automata using MONA During the bottom up Yacc parsing the parse tree is run on these automata yielding evaluation of the side constraints Software engineering In KK S96 it is shown that many software design architecture de scriptions are expressible in M2L Tree Using FIDO parse tree constraints are expressed and compiled to automata This project was a precursor of YakYak and did not combine constraint checking with parsing or use Guided Tree Automata FMona FMona BF97 is a high level extension of MONA adding e g enumeration types record types and higher order macros to the MONA syntax It has been used to express parameterized transition systems abstraction relations synthesis of finite abstractions and validation of safety properties STTools MONA has been used for M2L Str based model checking of programs in the Syn chronized Transitions language Ras99 PEN PEN is a tool for verifying distributed programs parameterized by the number of processes T he systems are modeled by transducer automata and properties of configurations are represented by normal automata By performing transitive closure of the transducer see JNO0 and using an acceleration technique reachability properties
91. oncept of a bounded universe is enforced by the allpos declaration It works by conjoining a special basic automaton to the main formula ensuring that is interpreted as the whole set of positions in the universe It also causes the variable to be projected away as a very last op eration and at every export so it will not occur in the program automata or in the analysis Previous versions of MONA used a slightly different emulation technique where instead was a first order variable representing the last position in the universe For backwards compatibility an option m is provided 6 6 Example Regular expressions over the ASCII alphabet Regular expressions can be easily translated into MONA Consider the problem of constructing an automaton over the ASCII alphabet that recognizes the language a ab This can be done in a straightforward manner we introduce a second order variable restricted to 36 MONA 1 4 6 6 Example Regular expressions over the ASCII alphabet 0 n 1 for some n to denote the string We declare second order variables bitO bit7 restricted to be subsets of for the representation of a string of ASCII characters We make the default restriction on first and second order variables that they involve numbers at most 1 higher than the largest element in Then we recursively construct for each subexpression E of a ab a predicate is E p q such that is E p q holds if and only if the substring
92. ons to MONA In particular tools may use existential quantifiers or let constructs to bind terms to fresh variables knowing that MONA will take care of the required optimization 43 Separate compilation MONA supports efficient use of libraries of predicate definitions through the separate com pilation feature The user can divide the input file into a number of smaller files and then use the include construct to combine them If MONA is executed with the option e all automata corresponding to predicate applications are stored in an automaton library and automatically reused in subsequent executions of MONA The user can decide where to store the automaton library by setting the environment variable MONALIB When MONA finds out that a source file has changed using the file time stamp the part of the automaton library containing automata for that specific source file is recomputed The automaton library is a directory containing a sub directory for each source file Each sub directory contains a number of automaton files in the format also used by the import export mechanism see Section 6 1 and a special contents file In Figure 7 a template for separate compilation is shown Executing mona e application mona causes MONA to store the automata generated by applications of the predicates in the direc tory MONALIB library In subsequent compilations of the application file application mona MONA will attempt to reuse the stored au
93. owing functions are in the library mgGta mgLoad char filename loads a GTA from a file int mgStore mgGta gta char filename stores a GTA in a file void mgFree mgGta gta deallocates the memory used by a GTA mgState mgDelta mgGta gta mgId ss mgState left mgState right mA a represents the transition function of a GTA see Section 7 2 The arguments are a GTA a state space identifier a state from the left state space a state from the right state space and an alphabet symbol void mgAssign mgGta gta mgTreeNode t mgId id assigns state space identifiers and states to the nodes of a labeled binary tree int mgCheck mgGta gta mgTreeNode t takes a GTA and a labeled binary tree as arguments and checks whether the tree is accepted by the GTA or not See gtalib h for further descriptions 60 MONA 1 4 C 2 Using GTA files An example application Similar to the dfa2dot application of the DFA library there is an example application of the GTA library called gta2dot It shows the structure of a GTA in BDD representation graphically The following graph generated by gta2dot and the dot tool shows the BDD representation of the GTA test gta from before state space hat root state space univ state space dummy left state space univ left state space univ left state space dummy right state space dummy right state space univ right state space dummy initial state 0 initia
94. p O in Q A amp x notin P Figure 1 even mona MONA 1 4 2 2 The essential semantics Numbers Formulas Formulas 1st order terms Oth order terms Oth order terms HS Oth order arguments 1st order arguments lt Sets 2nd order terms 0 lt gt exO ex1 ex2 allO alli a112 MK HE IVIA VA V gt V 1st 2nd order arguments in g notin Figure 2 Essential MONA syntax would be undecidable Other conventional mathematical syntax is rendered in MONA accord ing to Figure Precedence and associativity rules are the standard ones see Appendix Other simple constructs Integer constants can be introduced by const declarations for example const c 1 2 3 declares a constant c with value 7 Local variables can also be declared without quantification by means of a let expression For example let1 y x c in y notin Q declares a first order variable y with value x c The scope of y is the formula following in Local boolean and second order variables can similarly be declared with letO and let2 constructs There are min and max terms as well for example the value of min 5 3 8 is 3 Certain modulo calculations but not all can be expressed e g 3 5 6 which is 2 2 2 The essential semantics Since WS1S is a logic closely related to arithmetic most constructs have a straightforward mathematical semantics see Section One important property of the semantics is that only finit
95. presenting accept reject and don t care respectively as state statuses These functions are used as the following pseudo code indicates dfaSetup number of states number of variables array of variable indices for each state starting with number 0 the initial state do dfaAllocExceptions number of exceptions for going to the default state for each exception do dfaStoreException some state some path end dfaStoreState default destination state end dfaBuild array of state statuses An example is described in Section Automaton operations The following automaton operations are available All operations returning a DFA leave the input automata unchanged operations returning void change the input automata void dfaFree DFA a deallocates the memory used to store a including the memory handled by the BDD manager void dfaNegation DFA a performs language complementation by changing accept states to reject states and vice versa void dfaRestrict DFA a changes reject states to don t care states void dfaUnrestrict DFA a changes don t care states to reject states DFA dfaCopy DFA a creates a copy of a void dfaReplaceIndices DFA a int map replaces the variable indices in a accord ing to map For each internal BDD node the variable index is replaced by map i The replacing must be order preserving see definition of signature equivalence in Sec tion EIJ void dfaPrefixClose DFA a
96. r where P ranges over a set of variables o 9 o amp g ex2P 0 PsbP P P P B Pju Semantics of the simplified language Given a fixed main formula 9 we define its semantics inductively relative to a string w over the alphabet B where B 0 1 and k is the number of variables in do Assume 18 MONA 1 4 3 1 The classical approach every variable of dp is assigned a unique number in the range 1 2 k called the variable number as in Section 2 5 Let P denote the variable with number 7 As indicated in Section the string w now determines an interpretation w P of P defined as the finite set j the jth bit in the P track is 1 For example the formula do JC A B C has variables A B and C which we can assign the numbers 1 2 and 3 respectively typical string w over IB looks like A 1 0 1 0 B 0 0 1 0 C 1 1 0 0 0 1 2 3 This string interprets all three variables although C is not free in do Thus the language associated with p is independent of the C track in the sense that changing the bits on the track for a string w does not affect the membership status of w Also note that suffixing w with any string of the form 0 defines the same interpretation as w Therefore we will say that w is minimum if there is no such non empty suffix The semantics of a formula can now be defined inductively relative to an interpretation w We use the notation w F
97. r the GNU General Public License Contents 1 Introductio 1 1 Introductory example 3 3 RD E a a 4 7 8 8 1 3 Concepts and algorithms 1 4 How to use this manual 1 5 Acknowledgments Tm 9 EcL 1 MTM 12 2 5 What are MONA automata really 2 ccce 13 ied tang SP E NR a A 14 i 15 18 1 The classical approach 2 llle 18 SEES OE 22 27 27 28 43 Se mE com mm EEE NE ET 29 5 Translation informatio 30 5 1 Verbose processing 4 ss 30 5 2 Visualization of automata els 32 6 Advanced constructs 33 6 1 Exporting and importing automata een 33 dd 34 SENESTE OSTEN 34 icti 34 36 36 39 39 et Ha iN 7 6 Tree SEN output forma 7 7 Inherited acceptance analysis s s a a a e e a a a 46 78 Emulating Monadic Second order Logic on Trees 51 51 51 52 52 52 53 53 56 57 58 58 59 62 66 68 73 76 80 MONA 1 4 1 Introduction It has been known since 1960 that the class of regular languages is linked to decidability questions in formal logics In particular WS1S Weak monadic Second order theory of 1 Successor is decidable through the automaton logic connection which can be simply stated the set of satisfying interpretations of a subformula is represented by a finite state automa ton Elg61 WSIS thus acts as a notation for regular languages just as regular
98. rack corresponding to that variable If uj ur is omitted from such a declaration the set of all explicitly declared universes is assumed by default As an alternative to restricting variables to certain universes individual state spaces names may be used in place of universe names This provides a more fine grained control of the use of guides Guides and universes can be specified by one of four methods 1 Neither a guide nor any universes are specified MONA then generates two universes of which one is a dummy and a trivial guide Two universes are needed because of the encoding of boolean variables mentioned above The automata being constructed are then essentially traditional tree automata 2 A number of universes without positions are specified but no guide MONA then gener ates a guide as a balanced tree and places the universes at the leaves of this tree such that each universe has a single state space If only one universe is explicitly declared a dummy universe is implicitly added 3 A guide and a number of universes with positions are specified completely by the user as described above 4 One or more recursive types are declared as described in Section 7 9 Anywhere a universe name is required a variable name can be used instead The variable name then denotes the set of universes over which the variable ranges according to its decla ration The use of guides and universes has changed considerably since
99. ram holds These strings are like the ones in the introductory example except that they begin with a bit vector that interprets the boolean variables We might regard this initial letter to be in position 1 Therefore the language associated with a formula consists of non empty strings even if there are no global boolean variables in the program Additionally if there is a global first order variable like x above then a string must have length at least 2 including the boolean vector For example when x is 0 the first letter interprets the boolean variables and the second letter in position 0 is a vector with a 1 in the x track MONA analyzes the automaton to find a smallest counter example by calculating a short est path from the initial state to a rejecting state and it prints out a string that puts the 11 MONA 1 4 24 Outputting the program automaton automaton in that rejecting state In the case above a shortest such string has length 2 including the letter at position 1 Finding a satisfying example is done similarly simply by searching for an accepting state instead of a rejecting state 2 4 Outputting the program automaton If MONA is executed with option w then the program automaton is printed For example mona w u even mona generates the following output somewhat abbreviated here DFA for formula with free variables PQ x A Initial state O Accepting states 9 Rejecting states 012345678 Auto
100. ramming CAAP 94 volume 787 of LNCS 1994 Nils Klarlund and Michael I Schwartzbach domain specific language for reg ular sets of strings and trees IEEE Transactions Om Software Engineering 25 3 378 386 1999 David E Long The design of a cache friendly BDD library In nternational Conference on Computer Aided Design ICCAD 98 ACM 1998 Frank Morawietz and Tom Cornell The logic automaton connection in linguistics In Logical Aspects of Computational Linguistics LACL 97 number 1582 in LNAI 1997 Albert R Meyer Weak monadic second order theory of successor is not elemen tary recursive In R Parikh editor Logic Colloquium Proc Symposium on Logic Boston 1972 volume 453 of LNCS pages 132 154 1975 Anders M ller and Michael I Schwartzbach The Pointer Assertion Logic Engine November 2000 Submitted for publication Marcus Nilsson Analyzing parameterized distributed algorithms Master s thesis Department of Computer Systems at Uppsala University Sweden 1999 Sam Owre and Harald Ruess Integrating WS1S with PVS In Computer Aided Verification CAV 00 LNCS 2000 Paritosh K Pandya DCVALID 1 3 The user manual Technical report Tata Institute of Fundamental Research STCS 99 1 1999 Paritosh K Pandya Specifying and deciding quantified discrete time duration calculus formulae using DCVALID Technical report Tata Institute of Funda mental Research TCS00 PKP 1 2000 78 Ras99 Anders Ste
101. ried out We call this manager the source manager The operation is initiated in the node p of the source table The result is written into the shared BDD administered by bbdm r the result manager and a BDD pointer denoting the resulting BDD in bbdm r is returned as a side effect this node is added to bdd roots of the result manager Thus a handle to the result can be obtained by using BDD LAST HANDLE bddm r right after the apply operation unary apply operation does not use a result cache Instead the value of the apply operation on a node is stored in the node itself The mark field holds this information Therefore all such fields must be initialized before the apply operation can be performed This initialization is carried out by a call of void bdd prepare applyl bdd manager bddm In a sequence of unary apply operations with the same leaf function it is not necessary to reinitialize the manager between operations The case that bddm bbdm_r is allowed If on the other hand the managers are different then a doubling of the result table does not invalidate BDD pointers in the source table The binary apply operation apply2 and the project operation bdd project are similar to apply1 with one important difference a result cache is used to store the results of earlier apply or project operations and this cache is administered by the result manager Therefore before any such operation is initiated a cache must have been a
102. s on using a global hashed node space In the world of automata it is computationally expensive to identify isomorphic subgraphs in contrast to the case of BDDs where a node can be hashed relative to its successors in a well founded manner Thus in the MONA BDD package the shared BDD of an automaton is represented in a node space unique to the automaton Such a node space is administered through a BDD manager of type bdd manager The bdd manager A BDD manager keeps the BDD nodes in an array node table Thus nodes are not individ ually allocated in contrast to conventional BDD packages bdd ptr is an offset into this table The first used offset is BDD NUMBER OF BINS 2 The table consists of a hashed part whose size table size is 2table log size where table log size is a natural number In addi tion there is an overflow area following the hashed part The overflow area is enlarged in incre ments of table overflow increment The field table total size is the number of BDD nodes in the allocated table Initially this number is BDD NUMBER OF BINS table size table overflow increment The maximum allowed value of table total size is 274 roughly 16 million The BDD manager also keeps a result cache which is a table of previously computed results used for binary apply and project operations It is pointed to by cache This pointer is null if the cache has not been allocated The cache is hashed with an overflow area incremented in s
103. str d1 28 MONA 1 4 43 Separate compilation example predicate library example application pred foo include library mona pred bar nass application a library mona b application mona Figure 7 Template for separate compilation Here restr is the set of restrict conjuncts in see Sections 8 2 and 6 4 and nonrestr is the set of non restrict conjuncts in q This reduction states that it is sufficient to assert 1 when 4 amp 2 was originally asserted in situations where the non restricted conjuncts of 9 are already conjuncts of whether restricted or not and the restricted conjuncts of are non restricted conjuncts of 41 It is not sufficient that they be restricted conjuncts of 1 since the restrictions may not be the same in q All rewrite rules mentioned here have the property that they cannot do any harm that is have a negative impact on the automaton sizes They can however damage the reuse factor obtained by the DAGification but this is rarely a problem in practice A different kind of rewrite rules could be obtained using heuristic this will be investigated in the future see Section 8 2 The effect of performing the formula reductions mentioned in this section is investigated in KMS00 A general benefit from formula reductions is that tools generating MONA formulas from other formalisms may generate naive and voluminous output while leaving optimizati
104. t 48 type universe 40 41 47 unrestriction variable index 12 3 26 variable number variant visualization BI Web site 7 WSIS WS2S WSRT H6 zero th order variable 81 Recent BRICS Notes Series Publications NS 01 1 NS 00 8 NS 00 7 NS 00 6 NS 00 5 NS 00 4 NS 00 3 NS 00 2 NS 00 1 NS 99 3 NS 99 2 Nils Klarlund and Anders M ller MONA Version 1 4 User Manual January 2001 83 pp Anders M ller and Michael I Schwartzbach The XML Revo lution December 2000 149 pp Nils Klarlund Anders Meller and Michael I Schwartzbach Document Structure Description 1 0 December 2000 40 pp Peter D Mosses and Hermano Perrelli de Moura editors Pro ceedings of the Third International Workshop on Action Seman tics AS 2000 Recife Brazil May 15 16 2000 August 2000 viii 148 pp Claus Brabrand lt bigwig gt Version 1 3 Tutorial Septem ber 2000 ii 92 pp Claus Brabrand lt bigwig gt Version 1 3 Reference Manual September 2000 ii 56 pp Patrick Cousot Eric Goubault Jeremy Gunawardena Mau rice Herlihy Martin Raussen and Vladimiro Sassone edi tors Preliminary Proceedings of the Workshop on Geometry and Topology in Concurrency Theory GETCO 00 State Col lege USA August 21 2000 August 2000 vi 116 pp Luca Aceto and Bj rn Victor editors Preliminary Proceedings of the 7th International Workshop on Expressiveness in
105. t order term t as a second order term T relies on restricting Ts values to be singleton sets where the sole element denotes the value of t therefore the semantics is not closed under complementation For example the formula p 0 where p is first order is handled as q P 0 where P is second order But the complement of is P 0D something that is different from the representation of p 0 namely P 0D amp singleton P where singleton P is a predicate denoting that P is a singleton set So the problem boils down to a simple fact regarding formulas under conjunctive restrictions is not robust under negation The practical problem is that if we try to keep automata in a normal form where the singleton restriction for all first order variables is obeyed then additional product and min imization calculations would be necessary for each automaton A representing a subformula and each free variable P the automaton representing the singleton property for P must be conjoined to A The singleton restriction is not the only one we need For example to emulate the se mantics of the Monadic Second order Logic on Strings in WS1S see Section 6 5 we must restrict all first and second order terms to numbers that correspond to positions in the given finite string naive approach where each occurrence of a first order variable p in an atomic formula is accompanied by conjoining the restriction p in to the atomic for
106. t to newly allocated arrays as those described at dfaExport D 1 Examples Presburger arithmetic and transduction In general there are two methods for creating new automata 1 The first is to write a MONA WSIS formula which expresses the desired property then make MONA export the corresponding automaton using the export construct and finally use dfaImport to import the automaton in your application 2 The other is to use the functions for explicit construction of automata as it has been done for the basic automata in MONA The first method allows you to use the succinct logic of WS1S instead of describing the automaton explicitly The second method allows you to parameterize the construction and has the advantage that you do not have to consider variable ordering The construction of the automaton for Presburger constants see the function dfaPresb Const in DFA basic c illustrates the second method The construction is parameterized in the sense that it depends on the choice of the constant The example program Examples presburger analysis c illustrates the use of the func tions dfalmport and dfaMakeExample and shows how to use the DFA package without in cluding the MONA front end It takes two command line arguments the name of a dfa file and the name of a variable It reads the file searches for the variable of the given name and then analyses the automaton to find a satisfying example It then extracts the part of the example b
107. teps of cache overflow increment Various statistics about the number of lookups insertions and collisions in the node table and the result cache are maintained by the BDD manager BDD nodes A BDD node is described in a structure data type name bdd record The left and right successors are each described as a bdd ptr packed into three bytes The node index name of variable is a two byte unsigned integer Thus the maximum allowed index is 216 2 65534 since the value 2 6 1 encodes a leaf The successors and the index are packed into two words each word is four bytes named 1ri 2 The bdd record also contains a next field which holds a bdd ptr to an overflow list and a mark field used by the unary apply routine and by other routines BDD node occupies four words or 16 bytes This small size should enable two consecutive nodes to be loaded into a CPU cache line at a time Consequently 3 A more recent version of Long s package is described in Lon98 73 MONA 1 4 the hashing scheme uses two bins per bucket that is BDD NUMBER OF BINS 2 Note that a BDD table consists of at most 2 bytes or 256Mb Since BDD nodes sit in the hashed node table BDD pointers are volatile data when the node table is doubled all BDD pointers in existence become invalid For this reason a BDD manager provides an alternative way of describing the results of BDD operations The manager maintains a dynamic array of BDD pointers bdd roots wh
108. the first MONA applica tions of WS2S We plan to simplify the use of tree mode in the future perhaps by removing the concept of universes in favor of a more direct access to the state spaces 42 MONA 1 4 7 4 Other tree mode specific constructs ws2s var2 A B ex1 pl p2 p3 p4 p5 pi lt p2 amp p2 lt p3 amp p3 lt p4 amp p4 lt p5 amp A p1 p2 p3 p4 p5 ex1 pi p2 p3 p4 p5 p6 p7 pi lt p2 amp p2 lt p3 amp p3 lt p4 amp p4 lt pd amp pb p6 amp p6 p7 amp B p1 p2 p3 p4 p5 p6 p7 Figure 11 ab1 mona 7 4 Other tree mode specific constructs The root of a universe u can be expressed using the first order construct root u If the guide and universes are specified according to method 1 then the expression root can be used to denote the root of the implicitly constructed non dummy universe The root u term can be used to express first order constants i e position constants e g root u2 01101 Another way of accessing the roots of universes is using the formula root t u1 u2 Un where is a first order term and each u is a universe name It is true if and only if t is the root of one of the universes u1 U2 Un The formula in_state_space t s1 S where t is a first order term and s1 sk are state space names declared in the guide is true if and only if the position designated by t in the binary tree belongs to one of the state spaces 51 sk according to the g
109. tomata unless the library source file library mona has been altered 29 MONA 1 4 5 Translation information This section describes features that provide detailed information about the translation process from formula to automaton 5 1 Verbose processing To monitor the translation process MONA provides a number of facilities which can be used for debugging MONA code For instance the s and t options can reveal the source of state space explosions something that likely happens if complicated properties are expressed The user can then attempt to rewrite that particular part of the source code or modify the tool generating the MONA code if not manually written and rerun MONA Progress information By default MONA prints some progress information It prints the name of the current trans lation phase the time spent in each phase and the completion percentage in the automaton construction phase Also information about the DAG representing the code see Section 4 1 and the results of the formula reductions see Section is shown s an example mona lossy queue mona yields the following output where the counter example and the satisfying example are omitted for clarity MONA vi 4 for WS1S WS2S Copyright C 1997 2000 BRICS PARSING Time 00 00 00 01 CODE GENERATION DAG hits 297 nodes 116 Time 00 00 00 01 REDUCTION Projections removed 1 of 15 Products removed 10 of 63 Other nodes remove
110. trees In European Symposium on Programming Languages and Systems ESOP 00 volume 1782 of LNCS 2000 Patrice Godefroid and David E Long Symbolic protocol verification with Queue BDDs In IEEE Symposium on Logic in Computer Science LICS 96 1996 Jesper G Henriksen Jakob L Jensen Michael E J rgensen Nils Klarlund Robert Paige Theis Rauhe and Anders Sandholm Mona Monadic second order logic in practice In Tools and Algorithms for the Construction and Analysis of Systems TACAS 95 volume 1019 of LNCS 1996 Thomas Hune and Anders Sandholm case study on using automata in control synthesis In Fundamental Approaches to Software Engineering FASE 00 volume 1783 of LNCS 2000 Jakob L Jensen Michael E J rgensen Nils Klarlund and Michael I Schwartzbach Automatic verification of pointer programs using monadic second order logic In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 97 1997 Bengt Jonsson and Marcus Nilsson Transitive closures of regular relations for verifying infinite state systems In Tools and Algorithms for the Construction and Analysis of Systems TACAS 00 volume 1785 of LNCS 2000 Nils Klarlund Jari Koistinen and Michael I Schwartzbach Formal design con straints In ACM SIGPLAN Conference on Object Oriented Programming Sys tems Languages amp Applications OOPSLA 96 1996 Nils Klarlund Mona amp Fido The logic automaton connection in practic
111. ually using quantifications As an example importing an automaton mapping automaton variables A1 A2 where the numbers define the ordering into a MONA variables B2 B1 respectively can be done as follows var2 B1 B2 ex2 C1 C2 import file dfa A1 gt C1 A2 gt C2 amp B1 C2 amp B2 C1 We here use the property that MONA chooses the variable order as the order of declaration of the variables As an alternative to the w option the option xw is provided It causes the main formula to be output in external format rather than the format shown in Section 33 MONA 1 4 6 2 Prefix closing 6 2 Prefix closing The predicate notation prefix amp stands for an operation that calculates the prefix closure of the automaton associated to q In other words a string w satisfies a formula prefix if and only if there is some string v so that w v satisfies q The prefix operation has no logical meaning but it is useful for instance in the synthesis of controllers for reactive systems SS98 HS00 6 3 Presburger arithmetic Presburger arithmetic consists of formulas built from natural number constants and variables equality first order logical connectives and addition In contrast to WS1S there are no second order constructs but addition of arbitrary terms is allowed not just addition with constants Presburger arithmetic can be expressed in WS1S by encoding naturals as bit strings using base 2 encoding SKR9 8 In this way
112. uction is often linear not exponential as it may be feared BK98 In language theoretic terms the operations above can be characterized as follows Let the right quotient of a language L with a language L be defined as L I 2 w 3u I wue L Also let the projection operation E be defined by E L w dw w is identical to w except for the P track Choose the language L to be L w B the Pj track w is of the form 0 for j 4 i It can then be proven that L ex2 Pi amp ELG L9 which is a language theoretic explanation of the automata calculations outlined above 21 MONA 1 4 3 2 The MONA approach Notice that a conjunction or some other binary boolean operator in worst case causes a quadratic increase in automaton size while a quantification may cause an exponential increase due to the determinization As a consequence the number of states in the minimal automaton corresponding to a formula with n nested quantifiers or more precicely alternation depth n since theoretically a sequence of quantifiers of the same type could be implemented as a single combined projection is in the worst case gon 22 jen for some constant c In other words the complexity of this decision procedure is non elementary Issues in the classical approach The elimination of first order variables poses conceptual and practical problems The concep tual problem is that viewing a firs
113. uide 7 5 Example Exponential savings with guides Assume we want a GTA to accept the set of trees which have a branch with exactly 5 a labels and a branch with exactly 7 b labels With ordinary tree automata e g using method 1 for describing universes the automaton could be encoded as shown in Figure Since the resulting automaton has to keep track of both how many as 0 to 5 and how many bs 0 to 7 it encounters it has approximately 6 8 states Now assume that we happen to know that as occur only in the left part of the binary tree that is any node labeled a is below root 0 Similarly any node labeled b is below root 1 Utilizing this location independence we can construct a guide with three state spaces and two universes and restrict the various variables to the appropriate universes as shown in Figure 43 MONA 1 4 7 6 Tree mode output format ws2s guide d0 a b a gt a a b gt b b universe ua 0 ub 1 var2 ua A var2 ub B ex1 ua p1 p2 p3 p4 p5 pi lt p2 amp p2 lt p3 amp p3 lt p4 amp p4 lt p5 amp A p1 p2 p3 p4 p5 exi ub p1 p2 p3 p4 p5 p6 p7 pi lt p2 amp p2 lt p3 amp p3 lt p4 amp p4 lt p5 amp pb lt p6 amp p6 p7 amp B pi p2 p3 p4 p5 p6 p7 gt Figure 12 ab2 mona In effect we now get one automaton counting as and one counting b s so the total number of states is now around 6 8 In general exploiting positional knowledge using the guide universe technique
114. ul features 8 1 BDD variable orderings The indices assigned to the variables in a formula see Section are used in the internal BDD representation to define the ordering of BDD nodes It is a well known fact see Bry86 that the ordering has a significant influence on the number of BDD nodes required When the number of nodes increases the time spent on automaton operations increases correspondingly In the current version of MONA indices are assigned to variables in order of occurrence Consider the following MONA program var2 P1 Q1 P2 Q2 P3 Q3 P4 Q4 P5 Q5 Pi Q1 amp P2 Q2 amp P3 Q3 amp P4 Q4 amp P5 Q5 The corresponding automaton generated by MONA has 3 states and 17 BDD nodes are used to represent the transition function If we simply change the order of the declarations of the variables as shown below 95 BDD nodes are required to represent essentially the same automaton var2 P1 P2 P3 P4 P5 Q1 Q2 Q3 Q4 Q5 Pi Q1 amp P2 Q2 amp P3 Q3 amp P4 Q4 amp P5 Q5 By adding more Pi Qi pairs the number of BDD nodes grows linearly in the first program and exponentially in the second This is thus an example of an exponential difference caused by the ordering of the indices Another well known fact about BDDs is that deciding the optimal ordering is NP complete so searching for optimal orderings is not feasible One solution is to shift the burden to the MONA programmer such that the variable ordering can be specifi
115. ula evaluates to L under the semantics just given not to as one would expect of a false formula that contains no restricted free variables Equivalence of the binary and ternary semantics It can be proven Kla99 that the classical semantics is equivalent to the ternary semantics for WSIS R in the following sense wkp e f ju 1 wF amp p w 1 wF amp kp amp w 0 Section describes how to make MONA generate ordinary two valued automata 26 MONA 1 4 4 Translation optimizations Although the decision procedure does have a very high worst case complexity in practice it does pay off to simplify and reuse computations whenever possible as shown in KMS00 This section describes the internal representation of formulas and related techniques for improving performance as employed by MONA 41 DAG representation of formulas Internally MONA is divided into a front end and a back end The front end parses the input and reduces it to an internal code describing the automata theoretic operations that will calculate the resulting program automata The back end then carries out the automaton operations in a way similar to the simplified decision procedure explained in Section 3l For efficiency reasons the internal code is stored in a DAG Directed Acyclic Graph rather than a more conventional tree structure The atomic formulas are located in the leaves and the composite constructs are in the internal nodes The D
116. ver something is encoded directly in MONA logic The FIDO language is based on recursive data types over finite domains but it also adds other programming language concepts such as subtyping unification and coercion Not exploiting the Guided Tree Automata concept of MONA FIDO has to some extent been obsoleted by the WSRT logic described in Section 7 9 LISA The LISA language ABP98 was developed in parallel with FIDO It contains many of the same features as FIDO but instead of recursive data types it is based on the more general feature logics Trace abstractions In KNS96a FIDO is used to perform behavioral reasoning about distributed reactive systems based on trace abstractions M2L Str is used as a temporal logic to address the Broy Lamport challenge of modeling and verification a memory server specification This work provided the motivation for the development of FIDO Computational linguistics An application of MONA for linguistic processing and theory verification using WS2S is described in MONA 1 4 12 MONA applications Protocol verification MONA has been used for various kinds of protocol verification In HJJ 96 a variant of the Dining Philosophers protocol is verified and in SK99 the Sliding Window communication protocol is modeled using I O automata and then translated to WSIS and verified DCVALID DCVALID Pan99 is a tool for checking validity of Quantified Discrete time Duration Calculus formulas based
117. w by induction on the formula how to construct a deterministic automaton A such that L A 9 where A is the language recognized by A The atomic formulas are hand translated into what we call basic automata Composite formulas correspond to well known automaton operations Translating atomic formulas For simplicity we only show basic automata for the case where i 1 7 2 k 3 We also only show the first two or three components of a letter P sub P The automaton must recognize the language P sub P5 w B for all letters in w if the first com ponent is 1 then so is the second Such an automaton is The other atomic formulas are treated similarly P PAPs fo Pj P 1 MONA 1 4 3 1 The classical approach Translating composite formulas d Negation of a formula corresponds to automaton complementation so if we have already calculated A such that L L A then LCG CLCH LL A LCA where denotes both the language theoretic operation of complementation and automata theoretic operation of complementation Thus A CA is the desired automaton for q Naturally the automaton operation C in MONA is implemented as the linear time com plementation algorithm that simply consists of flipping accepting and rejecting states p amp 4 Conjunction corresponds to language intersection L g amp 6 L N L G So the desired auto
118. y decision diagrams ACM Computing surveys 24 3 293 318 September 1992 Kai Baukus Karsten Stahl Saddek Bensalem and Yassine Lakhnech Abstracting WSIS systems to verify parameterized networks In Tools and Algorithms for the Construction and Analysis of Systems TACAS 00 volume 1785 of LNCS 2000 Julius Richard B chi On a decision method in restricted second order arith metic In Proc Internat Cong on Logic Methodol and Philos of Sci Stanford University Press 1960 76 B c60b DKS99 Don70 Elg61 Elg99 EMSO00 GL96 HJJ 96 HS00 JJKS97 JN00 KKS96 Kla98 Kla99 KMS00 Julius Richard B chi Weak second order arithmetic and finite automata Z Math Logik Grundl Math 6 66 92 1960 Niels Damgaard Nils Klarlund and Michael I Schwartzbach YakYak Parsing with logical side constraints In Developments in Language Theory DLT 99 1999 John Doner Tree acceptors and some of their applications J Comput System Sci 4 406 451 1970 Calvin C Elgot Decision problems of finite automata design and related arith metics Transactions of the American Mathematical Society 98 21 52 1961 Jacob Elgaard Verifying C pointer programs using monadic second order logic Master s thesis Department of Computer Science University of Aarhus 1999 Jacob Elgaard Anders M ller and Michael I Schwartzbach Compile time debug ging of C programs working on

MONA Version 1.4 User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents