PROSYD: - Verimag
Contents
1. i 5 24 Specification Ele iode edente arie 5 2 2 Partition File rere A ke deg te deat eee du 6 2 39 Command Line Options 7 2 4 Qutput Files retener eger Dee dene d ener eese Dd 10 3 Installation e rentre tet eek te te De e d eue ne eene nenas 13 3 1 System Requirements iii 13 3 2 bicense IssUes iu 13 3 9 JInstalling Lily ioo alal too EE E 13 4 Technical Details illa lira 15 4L Implementation iaia 15 Ad TEST ic 16 5 Underlying Dheoty 2 noto ce cene denda te taceo ntadantdaawnaameauinaniers 19 Del Denno ilaele 19 5 22 Simplifying tree automata see 20 Simplification Using Games oaa 21 Simplification Using Simulation Relations esses 21 5 3 Optimizations for SynthesiS esse 22 Synthesis Algorithm 22 cost fr t boe eR UR DX da Rd ar Te Re RE Iu 23 NBE Wc xe secs aia A Wm UU IEEE 23 UC ERRE RE TORO de aute quad oebesdubus da DAN doe 24 AW T ila 25 NB Terea aek aE EE E NEE 28 Moore Machini iaia 29 EB ido E T E 31 Property Based Synthesis Tool Contents e v A Syntax Rule Summary aaa 33 vi e Contents Al Syntax of the Specification File ii 33 A 2 Syntax of the Partition File esse 34 A 3 Syntax of the generated DOT Files 34 A 4 Syntax of the Automata Files ssseee aaa 34 Property Based Synthesis Tool Table2. X let sat S c C 2P 2 C is minimal set such thatVq SAC 6 q 0 C4 CC For S O 22 x 22 let sat S O 0 S O 22 x 22 S sat S 6 0 sat 0 0 0 C S Furthermore let Sy s d s S let Og s d s O Let Cy S O d Sa Oa d D and let Co S d Sa Sa a d D Definition 15 KV05 MH84 Let Aygrx X D 22 x 22 q0 0 3 22 x 0 with Cy S O S O sat S O o ifO Z0 a S 0 0 ee is sat S o otherwise We have L ANBTK L AAwTk We improve this construction in three ways First we make use of the simulation relation on the AWT to reduce the size of the NBT Second we remove inconsistent states and third we compute the NBT on the fly Simulation Based Optimization We can use the simulation relation that we have computed on Aawr to approximate the simulation relation on Angry This is a simple extension of Fritz result for word automata Fri03 28 e Underlying Theory Property Based Synthesis Tool Given a direct simulation relation lt awr for A awr we define the simulation rela tion lt C Q x Q on Aypty as 81 01 2 82 03 iffvq S2 3q1 S1 q1 XAwr q2 q2 O2 gt q1 01 Note that lt is a subset of the full direct simulation relation on Angry and thus the following lemma holds Lemma 16 51 01 lt S2 02 implies L A C
3. assign hl state 0 state 2 assign fl state 1 initial begin state 0 n15 1n18 1 end always posedge clk begin case state 0 begin n15 1n18 1 car 0 state 0 if car 1 amp amp timer 1 state 1 if car 1 amp amp timer 0 state 2 end 1 begin n12 1n18 1 if timer 1 state 0 if timer 0 state 1 end 2 begin n10_1n15_1n18_1 if timer 0 state 2 if timer 1 state 1 end endcase end endmodule synthesis Figure 1 Generated design for a simple traffic light Property Based Synthesis Tool Usage e 11 hl 1 f1 0 D car 1 timer 0 D car 1 timer 1 D timer 0 D timer 1 D timer 1 fl 1 hl 0 Figure 2 State diagram of the generated traffic light 12 e Usage Property Based Synthesis Tool 3 Installation In this section we provide information about installation related issues including system requirements license issues and a guide to install Lily 3 1 System Requirements Lily was developed on a Gentoo GNU Linux based x86 machine with a 2 6 14 kernel using Perl 5 It should run on any similar machine that runs e Perl 5 8 8 or higher PRL If used with mc option Lily also requires e Vis release 2 1 or higher VIS 3 2 License Issues Copyright c 2006 Graz University of Technology TU Graz Copyright c 2006 University of Colorado at Boulder CU Boulder Permission is hereby granted without writt
4. 0 for all o Thus L ANgq L Angrx If L AXpr Z 0 the witness of nonemptiness of L Axpr is a witness of nonemptiness of L Angrx Otherwise we select a state q Q with d 9 6 0 and expand it setting 9 0 9 q 6 introducing the necessary states to Q Our current heuristic expands states in a breadth first manner which is quite ef fective It may be beneficial to expand certain state first say states with a low cardinality or with high ranks Moore Machine We use the game defined in Section 5 2 to compute language emptiness on the Anptg Since Angry is nondeterministic all states in the winning region have a Property Based Synthesis Tool Underlying Theory e 29 nonempty language If the initial state is in the winning region the language of Anptx is not empty and we extract a witness Since Awpry is a subset of AnpTk 1 We can reuse all results obtained when com puting language emptiness on Angr to compute language emptiness on A NBTk 1 Moreover it follows from Miyano and Hayashi s construction that if L A 40 and SC S then L A S 0 0 We may use this fact to further speed up the computation of language emptiness and especially to reuse information obtained computing language emptiness on Angr for larger k A witness for nonemptiness corresponds to a winning attractor strategy Tho95 The winning strategy follows the u iterations of the final v computation of Wg o From a state q
5. 4 e Introduction Property Based Synthesis Tool 2 Usage This sections explains how to use Lily Lily takes a specification and a partition file as input and provides a VERILOG and a DOT version of the generated design In the first two subsections we explain the purpose and the syntax of the specification and the partition file Then we show how to call Lily and explain the available command line options Finally we talk about the generated output files 2 1 Specification File The specification file holds a formal specification written in the linear part of PSL or in LTL The tool distinguishes between the language due to the file extension Files ending with psl are recognized as PSL files Files ending with Itl are recognized as LTL files Table 2 shows the Boolean and temporal operators recog nized by Lily for the PSL and the LTL flavor The two flavors also differ in the way they handle variables In LTL flavor we have to assign a Boolean value 0 or 1 to each variable In PSL flavor the assignment can be omitted Those variable are assigned to 1 by default In both flavors the keywords assert and assume can be use to distinguish between assumptions on the environment and assertions the system has to fulfill If the keywords are omitted we synthesize the conjunction of all formulas Table 2 Operators recognized by Lily Boolean operator LTL flavor PSL flavor And amp amp amp Or FEE Imply gt g
6. amp we go to a state q from which the protagonist can force a shorter path to an accepting state In an accepting state we move back to an arbitrary state in the winning region If a strategy exists it corresponds to a complete X labeled D tree and thus to a Moore machine M The states of M are the states of Angry that are reachable when the strategy is followed and the edges are given by the strategy To minimize the strategy we compute the simulation relation and apply Theo rem 4 which is equivalent to using the classical FSM minimization algorithm HU79 Thus the optimized strategy is guaranteed to be minimal with respect to its given I O language The output of our tool is a state machine described in VERILOG that implements this strategy 30 e Underlying Theory Property Based Synthesis Tool 6 References AHKV98 ATWO05 B 96 BDBF 05 CGP99 Chu62 DOT Fri03 FW02 GBS02 GKSV03 GVZ Har05 HU79 R Alur T A Henzinger O Kupferman and M Y Vardi Alternating refine ment relations In Proc 9th Conferance on Concurrency Theory pages 163 178 Nice September 1998 Springer Verlag LNCS 1466 C Schulte Althoffa W Thomas and N Wallmeier Observations on deter minization of buchi automata In nternational Conference on the Implementa tion and Application of Automata 2005 R K Brayton et al VIS A system for verification and synthesis In T Hen zi
7. is an academic toolkit for linear logics and automata on infinite words It contains a translator from LTL to nonderministic B chi word automata and various transfor mation and optimization algorithms for such automata which were of use for the synthesis tool The synthesis approach we implemented consists of a sequence of automata trans lations and corresponding optimizations see Section 5 for more details Each type of automata and the translations and optimizations applicable to it form a separated part of our tool e Wring Block to construct and manipulate nondeterministic B chi word automata e BuildUCT Block to construct and manipulate universal co B chi tree au tomata e BuildAWT Block to construct and manipulate alternating weak tree au tomata e BuildNBT Block to construct and manipulate nondeterministic B chi tree automata e BuildFSM Block to construct and manipulate finite state machines Property Based Synthesis Tool Technical Details e 15 Partition of signals Synthesize x Xe 7 7 2t BuildAWT Je optimize e s SE Sw Sa sg E NO Da N b Sy SRI N e BuildNBT d optimize 5 n d s Synthesize ser N 2s xu Check Language FI Emptiness Not Output If the formula is not realizable the VERILOG output files contain the message module Formula is not realizable Figure 3 Block
8. The transition corresponding to a box C consists of all pairs d q such that there is an edge from C to q such that d satisfies the label on the edge In particular if d satisfies none of the labels the branch in direction d is finite e g in state m with light 0 and timer 1 Note that finite branches are accepting Even though the NBW is optimized the UCT is not minimal The tree languages L Aucr and L Aycr are empty Our algorithm finds both states and replaces them by transitions to false removing the part of Avcr to the right of the dashed line Note that the optimizations cause the automaton to become weak 24 e Underlying Theory Property Based Synthesis Tool Figure 4 NBW for 9 always eventually timer eventually light light R timer Figure 5 UCT for always eventually timer always light light until timer AWT From the automaton Aycr we construct an AWT AaAwry such that L A awr C L Aucr Definition 9 KV05 Let Aycr X D Q q0 9 Q let n Q and let k N Let k denote 0 k We construct Aawrk Z D Q qo 9 00 with Q qi e amp Qx k q amp aoriis even do 90k 5 q 1 6 di mi s des gx ix I da di 4 8 4 0 i1 ie V a5 ij 0 o Qx 13 2k 1 We call i the rank of an AWT state q i If k 2n2 we have L Aawrtk 0 implies L Aucr 0 KV05 Pit06 We improve this
9. We define a sufficient but not necessary condition for language emptiness of A4 Our heuristic views the alternating automaton as a game which is played in rounds In each round starting at a state q the protagonist decides the label o X and a set C C 8 q 0 and the antagonist chooses a pair d q C The next round starts in g If 6 q 6 or C are empty the play is finite and the player who has to choose from an empty set loses the game If a play is infinite the winner is determined by the acceptance condition For an ABT the protagonist wins the play if the play visits the set of accepting states a infinitely often For a ACT the protagonist wins if from some point on the play avoids a A strategy s maps a finite sequence of states qo qy to a set C C 0 qi 0 for some a label o X A play q1 q2 adheres to a strategy s if for every k s qo qx C implies that there is a pair d qy41 C The game A is won if there is a strategy such that all plays starting at q that adhere to the strategy are won We call q a winning state and the set of all winning states is called the winning region If the game is lost then L A is empty In the case of an NBT NCT the converse holds as well However in general it does not A counterexample would be a word automaton such that 1 6 go 6 q1 qo for all o 2 L A A L A 0 and 3 the games A and A are won In this case the game A is also won Note that computi
10. Aucr Z D Q q0 8 0 with for every q Qando X 8 q c d q d e D q 8 g dUo We have L Aucr Tz p T Anpw We can reduce the size of L Aucr using game based simulation and Theorem 2 Optimizing the UCT reduces the time spent optimizing the AWT and most im portantly it may make the UCT weak which means that we avoid the expensive construction of the AWT discussed in the next section Because the UCT is small in comparison to the AWT and the NBT optimization comes at little cost Specifications are often of the form w where is an assumption on the envi ronment and y describes the allowed behavior of the system States necessary to ensure that the environment assumptions are fulfilled once the system assertion y is violated are not necessary Such states among others are removed by the game based optimization Example 8 We give a small example to show which states will be removed by our algorithm Let 9 always eventually timer always light light until timer Fig 4 shows a minimal NBW Aygw accepting all words in q Edges are labeled with cubes over the atomic propositions We partition the atomic propositions into I light and O timer The UCT Aycr that accepts all 2 labeled 2 trees not in T Awgw is shown in Fig 5 Circles denote states and boxes denote transi tions We label edges starting at circles with cubes over O and edges from boxes with cubes over I
11. Synthesizes the formula given with or lt1 to VERILOG code using the signal partition stored in file Only valid with syn option dir is the name of the directory in which all re sults of the synthesis process are stored If syndir is not set the result files are stored in the current directory Read in the automaton described in file Use the following file extensions to defined the type of automaton to read see Appendix A 4 for a syntax description aut fora state labeled NBW default 12a foratransition labeled NBW uct for an UCT The automaton specifies the allowed be havior of the system to construct This options overwrites the specification given with f or 1tl Only valid with syn and 1tl option Modelcheck the result of the synthesis process using the program Vis B 96 To use this option Vis has to be installed and in the search path Optimize the universal co B chi tree au tomaton using game and simulation based optimizations see Section 5 3 On by default Optimize the alternating weak tree au tomaton using game and simulation based optimizations see Section 5 3 On by default Optimize the witness strategy using sim ulation relation see Section 5 3 On by default Use Fritz optimizations see Section 5 3 during Miyano and Hayashi s construc tion Combine Miyano and Hayashi s construc tion with language emptiness check see Section 5 3 Merge direction by applying Theorem 11 of
12. construction in three ways by using games by merging direc tions and by using simulation relations Game Simulation We can use Theorem 2 to remove states from A awry Example 10 Consider the UCT in Fig 6 and the corresponding AWT in Fig 7 using k 5 The UCT has been optimized using the techniques discussed in Sec tion 5 3 and the AWT has been optimized in three ways We have removed states that are not reachable from the initial state we have merged directions and we have removed edges The last two optimizations are explained in the next sec tions Still there is ample room for improvement of the AWT Property Based Synthesis Tool Underlying Theory e 25 Figure 6 UCT that requires rank 5 Edges that are not shown for instance from r4 with label a correspond to labels that are not allowed M Ss a DI N true N x true N C M 4 true SR e o 3 o Oo i Ce E o nim Figure 7 AWT for UCT in Figure 6 Application of Theorem 2 removes the 12 states below the dashed line on the bot tom left and the incident edges This is a typical situation each UCT state has an associated minimum rank It should be noted that Aawr has a layered structure there are no states with rank j with a transition back to a state with a rank i gt j Furthermore A AWTk 1 consists of A awr plus one layer of states with rank k 1 This implies that game information computed for A awr can be r
13. of Figures Figure 1 Figure 2 Figure 3 Figure 4 Figure 5 Figure 6 Figure 7 Generated design for a simple traffic light 11 State diagram of the generated traffic light 12 Blockdiapram of Lily eee 16 dido 25 UCT fot qo 25 UCT that requires Tank 5 aite tdi ot 26 AWT for UCT in Figure 6 esse 26 Property Based Synthesis Tool Table of Figures e vii Glossary Acceptance Condition A condition defining how an infinite automaton accepts an input object We use B chi and co B chi acceptance conditions both defined by a set of states F An input word is B chi accepted by an automaton if the set of states visited infinitely often while reading the input word intersects the set F Dually a word is co B chi accepted if the set of states visited infinitely often does not intersect F Alternating Tree Automaton An automaton with an arbitrary branching mode running on trees Atomic Proposition An atomic proposition of a formula in a propositional logic corresponds to signals in a design or implementation AWT Alternating Weak Tree Automaton An alternating tree automaton with a particu larly structured state space The states are partitioned into partially ordered sets Each set is classified as accepting or rejecting The transition function is restricted so that in each transition the automaton either
14. stays at the same set or moves to a set smaller in the partial order Branching Mode The branching mode is a way to classify automata We distinguish between four branching modes Deterministic nondeterministic universal and alternating In a deterministic automaton the transition function maps from state and letter to a single state The transition functions of nondeterministic and universal automata map to sets of states The automata differ in the way they accept an input word or tree In a nondeterministic automaton the suffix of the word or tree should be accepted by one of the states in the set In the universal automaton all states in the set have to accept the suffix An alternating automaton can have nondeterministic and universal edges Infinite Game A finite state machine on which two players the protagonist and the antagonist determine the run by each determining part of the input The game comes with a winning condition and the task of the protagonist is to make sure that the run satisfies this condition Language Emptiness The language of an automaton is empty iff the automaton accepts no input object word or tree that means there is no accepting run for this automaton LTL Linear Temporal Logic or Linear time temporal logic LTL is a temporal logic for property specification in formal verification Pnu77 LTL Game An infinite game where the winning condition is given as LTL formula All plays in which the sequen
15. the notions and terms related to PSL and VERILOG In order to understand the underlying theory readers need to have a good understanding of model checking of game theory and of automata theory including tree automata and alternating automata on infinite words Background Synthesis of linear time formulas is closely related to Church s problem of synthe sis for S1S Chu62 It was formalized by Pnueli and Rosner PR89 There exist a few implementations covering subsets of LTL but to our knowledge no implemen tation for the complete language Recent work of Amir Pnueli handles the most general subset His approach is applicable to specifications expressible with a gen eralized Streett 1 acceptance condition Those specifications have to be rewritten to a particular syntax in order to be synthesized The work presented here is the first implementation of a synthesis algorithm for the linear time fragment of PSL Property Based Synthesis Tool Contents Table Of REVISIONS ssaa iii Lune ili Executive Summary aa ili PUTpose rire iii Intended Audience ili BacKsround crioa i aa iv Contents T E V Table of Figures ci rrr erret a Cae eda o eode koe d Yes vii CI siria viii ll Introduction inline 1 1 Whatis Lily coi iii aiar 1 1 23 Why tse Lily marensin i i e re pedes 1 1 3 Features Listini iii iaia 2 1 4 History of Synthesis alari 2 MESI
16. through careful use of optimization techniques Safra s determinization construc tion turned out to be very resistant to efficient implementations ATW05 In order to deal with these complexity issues previous implementations on LTL synthesis focuses on restricted subsets of LTL WHT03 Har05 PPS06 The approach of Piterman Pnueli and Sa ar PPS06 handles the most general sub set Their approach is applicable to specifications expressible with a generalized Streett 1 acceptance condition Recently Kupferman and Vardi KV05 proposed an alternative to the standard approach Starting from a specification over UO they generate through the nondeterministic B chi word automaton for a universal co B chi tree automa ton that accepts all trees satisfying From that they construct an alternating weak tree automaton accepting at least one regular tree satisfying or none if is not realizable Finally the alternating automaton is converted to nondeterministic B chi tree automaton with the same language A witness for the nonemptiness of this automaton is an implementation of The approach is applicable to any linear logic that is closed under negation and that can be compiled to nondeterministic B chi word automata Our implementation is based on this approach It is the first to handle the complete language and does not impose any syntactic requirements on the specification Property Based Synthesis Tool Introduction e 3
17. ERILOG monitor to file Read in the automaton described in ile and optimizes it This automaton can be used as specification for the synthesis process of Lily as well See Table 4 for a detailed description of using auto option with Lily Example comp f l G F q 1 h ltl specl ltl m LTL2AUT o l p examplel ver 1 mon monitor v auto nbwl aut Lily has new command line options to invoke the synthesis process to define the name of the partition file to specify an output directory to verify the generated design and to switch various optimizations on and off By default all optimizations are turned on The user need not care about those options In Table 4 we list and describe all available options Let us continue the traffic light example If the specification is stored in the file tl psl and the partition is stored in the file t1 part the simplest way to call Lily is to use one of the following commands ltl2aut pl syn tl part ltl tl psl or ltl2aut pl syn tl part ltl tl psl syndir trafficlight The output file are stored in the current directory or in the new directory trafficlight depending on the chosen command 8 e Usage Property Based Synthesis Tool Command syn file syndir dir auto file mc ouct 0 1 oawt 0 1 owit 0 1 omh 0 1 omhc 0 1 oedges 0 1 orelease 0 1 oreuse 0 1 Table 4 Command line options for Lily Result
18. FP6 IST 507219 PROSYD Property Based System Design Instrument Specific Targeted Research Project Thematic Priority Information Society Technologies Manual for Property Based Synthesis Tool Deliverable 2 2 3 Due date of deliverable 1 August 2006 Actual submission date 13 August 2006 Start date of project January 1 2004 Duration Three years Organisation name of lead contractor for this deliverable TU Graz Revision 1 0 Project co funded by the European Commission within the Sixth Framework Programme 2002 2006 Dissemination Level Public Restricted to a group specified by the consortium including the Commission Services PP Restricted to other programme participants including the Commission Services Oo Confidential only for members of the consortium including the Commission Services Notices For information contact Roderick Bloem rbloem ist tugraz at This document is intended to fulfil the contractual obligations of the PROSYD project con cerning deliverable 2 2 3 described in contract number 507219 The information in this document is provided as is and no guarantee or warranty is given that the information is fit for any particular purpose The user thereof uses the information at its sole risk and liability Copyright PROSYD 2006 All rights reserved ji e Property Based Synthesis Tool Table of Revisions Version Date Description an
19. LIST OUTPUTS outputs SIGNALLIST SIGNALLIST SIGNAL SIGNAL SIGNALLIST SIGNAL w A 3 Syntax of the generated Dor Files GRAPH digraph NAME HEADER BODY NAME wt HEADER OPTIONLIST OPTIONLIST OPTION OPTION OPTIONLIST OPTION KEY VALUE KEY wt VALUE wt dt BODY NODEEDGELIST NODEEDGELIST NODE EDGE NODE NODEEDGELIST EDGE NODEEDGELIST NODE NAME NODEOPTIONLIST EDGE NAME gt NAME NODEOPTIONLIST NODEOPTIONLIST NODEOPTION NODEOPTION NODEOPTIONLIST NODEOPTION KEY VALUE See DOT for the completed definition of the DOT language A 4 Syntax of the Automata Files AUTOMATON STATES STATES ARCS FAIR States NEWLINE STATEDEFS 34 e Syntax Rule Summary Property Based Synthesis Tool STATEDEFS NAME DESCRIPTION LABEL LTLFORMULAE ARCS ARCSDEFS Di ARCS a FAIR vas LISTOFSTATES E STATE NEWLINE I STATE NEWLINE STATEDEFS w TLFORMULAE TLFORMULAE FORMULA FORMULA LTLFORMULAE Arcs NEWLINE ARCSDEFS ARC NEWLINE ARC NEWLINE ARCSDEFS gt NAME gt ARCLIST LISTOFSTATES NAME NAME LISTOFSTATES I Note that the syntax for a valid LTL formula is shown in Section A 1 The syntax of STATE and ARCLIST depend o
20. Section 5 3 Restrict release function to stay in odd layer if possible Theorem 13 Reuse the result from previous computa tions with lower ranks see Section 5 3 Property Based Synthesis Tool Example syn exl part syndir results auto count 12a mc ouct 1 oawt 1 owit 0 omh 1 omhc 1 oedges 1 orelease 0 oreuse 1 Usage e 9 2 4 Output Files Lily provides a VERILOG module and a graphical state diagram of the the generated design We use DOT format to store the state diagram Files in DOT format can be translated using dot GVZ See Appendix A 3 for a syntax description of the generated DOT files By default Lily generated the following two files ltl2vl verilog v ltl2vl synthesis dot If the specification is realizable 1t12vl verilog v holds the VERILOG module of the generated design The state diagram of the generated design is stored in ltl2vl synthesis dot Ifthe specification is not realizable both files state that the given specification is unrealizable Note that the prefix 1t12v1 can be replaced by a user defined prefix with the option p The specification we used in our traffic light example is realizable and the design generated by Lily is shown in Figure 1 The corresponding state diagram is shown in Figure 2 10 e Usage Property Based Synthesis Tool module synthesis fl hl clk car timer input clk car timer output fl hl wire clk fl hl car timer reg 1 0 state
21. ce of states visited fulfill the given formula are winning for the protagonist Otherwise the antagonist wins viii e Table of Figures Property Based Synthesis Tool Mu Calculus A calculus of predicates and binary relations which enables writing and solving relational equations among states NBT Nondeterministic B chi Tree Automaton An alternating tree automaton with B chi acceptance condition and nondeterministic branching mode NBW Nondeterministic B chi Word Automaton An alternating automaton with B chi acceptance condition and nondeterministic branching mode The automaton runs on words PSL Property Specification Language the language for specification of designs upon which PROSYD is based PSL Game Similar to an LTL game but with a PSL formula as winning condition Realizable A given formula y over a sets of input and output O signal is realizable if there exists a strategy f 2 2 such that all the computations of the system gener ated by f satisfy w Intuitively a specification is realizable if there exists a system that can respond in such a way that independent of the input values the environment chooses the combination of inputs and outputs always fulfills the given formula Synthesis The process of automatically generating a design from a given specification For mally check if the given specification is realizable and find a witness UCT Universal co B chi Word Automaton An alternating tree au
22. d reason By Affected sec tions 0 5 June 9 2006 Included Theory Bloem Jobst Section 5 mann 0 6 June 12 2006 Extended User Manual 0 7 June 13 2006 Completed syntax summary and Sec Jobstmann Section A 4 2 tion 2 0 9 June 19 2006 Wrote installation guide and technical details 0 92 June 30 2006 Revised all sections All 1 0 July 17 2006 Revision based on feedback from project Bloem All manager Authors Roderick Bloem Barbara Jobstmann Executive Summary We present our property based synthesis tool Lily Given a set of properties written in the linear time fragment of PSL and a partition of the signals used in those prop erties into input and output signals Lily synthesizes a functionally correct design for the given properties The synthesized design a finite state machine is provided as a VERILOG module or as a labeled directed graph in DOT format This document states how to use and install Lily and gives technical and theoretical details about the tool Purpose The purpose of this document is to describe the effort done to develop a property based synthesis tool for the linear time fragment of PSL Furthermore it explains how to install and use this tool Property Based Synthesis Tool e iii Intended Audience This guide is intended for researchers working with PSL or a similar specification language who want to use automatic synthesis It is assumed that readers are familiar with
23. diagram of Lily The block Negate takes an LTL formula and builds its negation Finally the block Check Language Emptiness takes a nondeterministic B chi tree automata and check if the language of the automaton is empty and provides a witness if the language is not empty 16 e Technical Details Property Based Synthesis Tool 4 2 Test Suite We have performed tests with formulas generated by the Wring random formula generator Even though we used different partitions of the atomic propositions into input and output signals only a few of these formulas could be synthesized Most formulas were either unrealizable or Lily could not tell because the UCT was not weak and the bound on k was too high see Section 5 3 for the meaning of k Furthermore we are interested in meaningful specifications to see the relation between our design intent and the generated design Thus we concentrated on hand written formulas We show the effectiveness of the various optimizations by synthesizing 20 hand written formulas Our examples are small but we show a significant improvement over the straightforward implementation For realizable formulas we verified the output of our tool with a model checker In the case of unrealizability we negated the formula switched the input and output signals and tried to synthesize an environment that forces any system to violate the formula Since we synthesize Moore machines this is not always possible For instanc
24. e always r a with input r and output a can not be realized as a Moore machine and neither can always r a with input a and output r In such cases we have verified the result by hand which is a tedious job even for small formulas Property Based Synthesis Tool Technical Details e 17 18 e Technical Details Property Based Synthesis Tool 5 Underlying Theory In this section we explain the algorithms using in Lily JB06a JBO6b We start with introducing the necessary definitions in Section 5 1 In Section 5 2 we de scribe a game based and a simulation based optimization that can be used on any tree automaton In Section 5 3 we recall the construction of Kupferman and Vardi KV05 and discuss how we implemented it efficiently 5 1 Definitions We assume that the reader is familiar with the u calculus and PSL For an introduc tion see MP91 CGP99 We will use the linear time fragment of PSL to specify the behavior of a system Properties will use the set U O of atomic propositions where denotes the input signals and O the output signals A amp labeled D tree is a tuple T t such that T C D is prefix closed and 1 T X The tree is complete if T D The set of all X labeled D trees is denoted by Ty p An alternating tree automaton for X labeled D trees is a tuple A D 0 90 6 1 such that Q is a finite set of states qo Q is the initial state 6 Q x X 227 js the transition relation an elemen
25. e in AAwrx state q i has all transitions that q i has r is a run of Aawrtr and because it satisfies the extra condition on 8 it is also a run of A eri If r is accepting then every infinite path x in r gets stuck in an odd rank w from some level onwards So starting from all children of nodes on x have rank at most w That implies that the nodes on x in r have rank w starting at rank 1 at the latest Thus x is still accepting and since is arbitrary r is accepting as well L1 This theorem is key to an efficient implementation as it allows us to represent a set of pairs di q di q as di dy q whenever di dy can efficiently be represented by a cube over the input signals Simulation minimization We compute the simulation relation on AAwr and use Theorems 4 5 and 6 to optimize the automaton We would like to point out one optimization in particular Lemma 12 For q i q j Q with i gt j such that i is odd or j is even we have q i q j Thus for any 0 if i is even we can remove all transitions C 6 q i o that include a pair q j for j lt i 2 If iis odd we can additionally remove all transi tions that contain a pair q j with q amp and j i 1 That is odd states become deterministic and for even states there are at most two alternatives to choose from Theorem 13 Let A4 5 X D Q qu 07 as in Definition 9 but wi
26. elation can be computed in polynomial time as can the optimizations It should be noted that application of the theorems does not alter the simulation relation 22 e Underlying Theory Property Based Synthesis Tool 5 3 Optimizations for Synthesis Synthesis Algorithm The goal of synthesis is to find a Moore machine M implementing a PSL specifi cation or to prove that no such M exists Our approach follows that of KV05 introducing optimizations that make synthesis much more efficient The flow is as follows 1 Construct an NBW Anpw with L Anpw w ZUD w o Let n be the number of states of Angw Note n is exponential in if is expressible with an LTL formula of the same length and at most doubly exponential otherwise BDBF 05 2 Construct a UCT Aycr with L Aucr Ty p N T ANBw T Q Let n be the number of states of Aycr we have n lt n 3 Perform the following steps for increasing k starting with k 0 a Construct an AWT A awry such that L A awr L Aucr and L Aucr 4 0 implies L AAwrx 4 0 A awr has at most n k states b Construct an NBT Angry such that L Anprx L AawTk Apr has at most k 1 states c Check for the nonemptiness of L Angtx If the language is nonempty proceed to Step 4 d If k 2n2 stop Specification is not realizable Otherwise pro ceed with the next iteration of the loop The bound on k follows from Pit06 4 Compute a wit
27. en and W Thomas Symbolic synthesis of finite state con trollers for request response specifications In Proceedings of the International Conference on the Implementation and Application of Automata Springer Verlag 2003 32 e References Property Based Synthesis Tool A Syntax Rule Summary A 1 Syntax of the Specification File SPECFILE FORMULALIST FORMULALIST FORMULA POSTFIX FORMULA POSTFIX FORMULALIST PREFIX FORMULA POSTFIX PREFIX FORMULA POSTFIX FORMULALIST PREFIX assert assume POSTFIX NEWLINE NEWLINE Mn LTL Flavor FORMULA TERM BINARYOP TERM TERM ATOM FORMULA UNARYOP FORMULA TEMPORALOP FORMULA BINARYOP r gt lt gt UtTRIV UNARYOP MI TEMPORALOP G F X ATOM VARIABLE VALUE VARIABLE wt VALUE 0 1 PsL Flavor FORMULA TERM BINARYOP TERM TERM ATOM FORMULA UNARYOP FORMULA TEMPORALOP FORMULA BINARYOP amp amp amp gt lt gt until release UNARYOP TEMPORALOP always eventually NEXT NEXT next next_e COUNT next_a COUNT COUNT NUM NUM NUM ATOM VARIABLE VALUE VARIABLE Property Based Synthesis Tool Syntax Rule Summary e 33 VARIABLE wt VALUE 0 1 NUM d A 2 Syntax of the Partition File PARTFILE PARTITION PARTITION INPUTS NEWLINE OUTPUTS NEWLINE INPUTS inputs SIGNAL
28. en agreement and without license or royalty fees to use copy modify and distribute this software and its documenta tion for any purpose provided that the above copyright notice and the following two paragraphs appear in all copies of this software In no event shall TU Graz or CU Boulder be liable to any party for direct indirect special incidental or consequential damages arising out of the use of this software and its documentation even if TU Graz or CU Boulder have been advised of the possibility of such damage TU Graz and CU Boulder specifically disclaims any warranties including but not limited to the implied warranties of merchantability and fitness for a particular purpose The software provided hereunder is on an as is basis and TU Graz and the CU Boulder have no obligation to provide maintenance support updates enhancements or modifications Property Based Synthesis Tool Installation e 13 3 3 Installing Lily Follow the four steps below to install Lily Li 14 e Installation Download Lily source files 1ily tar gz from http www ist tugraz at staff jobstmann lily lily tar gz Unpack sources using tar xvfz lily tar gz to target directory e g opt lily Add source directory to the perl library path e g export PERLSLIB opt lily PERL5LIB or setenv PERL5LIB opt lily PERL5LIB Lily includes its own Wring version If you have installed another version of Wring add the source direct
29. eused for A awrk 1 A play is won lost in A awrk 1 if it reaches a states that is won lost in Aawrg Furthermore if q j is won then so is q i for i gt j when i is odd or j is even which allows us to reuse some of the information computed for states with rank k when adding states with rank k 1 This follows from the fact that q i simulates q j as will be discussed in Section 5 3 Merging Directions Note that 5 may be drastically larger than a single tran sition C 8 q 6 yields i transitions out of state q i Q Often however the transitions in the UCT are the same for many directions and this fact can be used for to optimize the transition relation 26 e Underlying Theory Property Based Synthesis Tool Theorem 11 Let A wy E D Q qu 9 0 be as in Definition 9 but with 8 q i 0 8 g i 6 V 4 9 7 4 4 7 C a74 gt j J We have L A wrx L Aawrk O Proof Because q 0 C q 0 any tree accepted by Ay is also accepted by Aawrr Let r be a run of A awrg we will build a run r of Awr Run r is isomorphic to r using a bijection that maps a node v of r to a node v of r Run r has the same labels as r with the following exception If node v in r is labeled t q i and has children t q i and t g i with i gt i then the corresponding children of node v of r are labeled q i and t q i Becaus
30. mulated by v If additionally u v we say that u and v are simulation equivalent denoted u v Lemma 3 fu lt v then L A C L A The following theorems are tree automaton variants of those presented in GKSV03 for optimizing alternating word automata The first theorem allows us to restrict the state space of an ABT to a set of representatives of every equivalence class under Theorem 4 Let A 2 D Q qo0 5 0 be an ABT let u v Q and suppose u v Let A D Q u qo 8 0 where q v if qo u and q qo otherwise and amp is obtained from by replacing u by v everywhere Then L A L A The following two theorems allow us to simplify the relations of an NBT Theorem 5 Let A 2 D Q qo 5 Q be an ABT let u v Q and suppose u v andu lt v For C C D xQ let eis C d v if3d d u C C otherwise Let A 2 D Q qo 8 a where for all q and 6 we have 8 q 0 C C 5 q 0 We have L A L A Theorem 6 Let A 2 D Q q0 5 0 be an ABT Suppose C C 6 q 0 C Z C and for all d and d q C there is a d q C such that q lt q Let A X D Q qo 9 be an ABT for which 8 equals except that d q 6 9 q 6 C We have L A L A We can simplify an ABT by repeated application of the last two theorems and removal of states that are no longer reachable from the initial state The simulation r
31. n the automaton State labeled Nondeterministic B chi Word Automaton STATE 11 ARCSLIST Di NAME DESCRIPTION label LABEL LISTOFSTATES Transition labeled Nondeterministic B chi Word Automaton STATE ARCLIST ARC NAME DESCRIPTION ARC ARC ARCLIST LABEL NAME Universal co B chi Tree Automaton STATE HS ARCLIST Di ARC rac DIRSTATELIST DIRSTATI bi Il Property Based Synthesis Tool NAME DESCRIPTION ARC ARC ARCLIST ABEL DIRSTATELIST DIRSTATE DIRSTATE DIRSTATELIST I ABEL NAME Syntax Rule Summary e 35
32. ness for the nonemptiness of Angr and convert it to a Moore machine If the UCT constructed in Step 2 is weak synthesis is much simpler we comple ment the acceptance condition of Aycr turning it into a UWT a special case of an AWT Then we convert the UWT into an NBT Angr as in Step 3b If L Anpr is nonempty the witness is a Moore machine satisfying if it is empty in un realizable In this case we avoid increasing k and the size of the NBT is at most 22n It turns out that in practice for realizable specifications the algorithm terminates with very small k often around three It should be noted that if the the UCT is not weak it is virtually impossible to prove the specification unrealizable using this approach because of the high bound on k In the following we will describe the individual steps discuss the optimizations that we use at every step and show how to reuse information gained in one itera tions of the loop for the following iterations Property Based Synthesis Tool Underlying Theory e 23 NBW We use Wring SB00 to construct a nondeterministic generalized B chi automaton for the negation of the specification We then use the classic counting construc tion and the optimizations available in Wring to obtain a small NBW Awgw with L Anpw DUE A L 9 UCT We construct a UCT Aucr over X labeled D trees with L Aucr T ZUD 9N L Anpw Definition 7 KV05 Given an NBW Anew Z D Q q0 5 a let UCT
33. ng a necessary and sufficient condition in polynomial time is not possible as this would give us an EXPTIME algorithm for deciding realizability The game is computed as follows Let P X S qeQl 3oeX Ce q o V d q eC q ES Wg S vY P X uZ Y S v P X Z and Wc S gY PYX vZ Y V S P X Z x I 2 In an ABT ACT with acceptance condition we can discard the states outside of Wg a Wc a resp Theorem 2 Given an ABT ACT A X D Q q0 9 Q let W Wg a W Wc a resp Let the ABT ACT A Z D Q qo 8 a with Q QW a anW and 9 4 0 C C 6 q 0 V d q C q EW If qo EW then q qo otherwise do is some state in Q with an empty language We have L A L A for all q Q and in particular L A L A O Property Based Synthesis Tool Underlying Theory e 21 Simplification Using Simulation Relations The second optimization uses direct simulation minimization on alternating tree automata Simulation minimization on nondeterministic word automata is well es tablished Our construction generalizes that for alternating word automata AHKV98 FW02 GKSV03 Let A D 0 40 be an ABT The direct simulation relation lt C Q x Q is the largest relation such that u lt v implies that 1 u a implies v a and 2 Vo X C 6 u o AC 6 v o Vd D d v C 3X d w Cu W 3 V If u lt v we say that u is si
34. nger and R Alur editors Eighth Conference on Computer Aided Verification CAV 96 pages 428 432 Springer Verlag Rutgers University 1996 LNCS 1102 Shoham Ben David Roderick Bloem Dana Fisman Andreas Griesmayer Ingo Pill and Sitvanit Ruah Automata construction algorithms optimized for PSL 2005 Prosyd D 3 2 4 E M Clarke O Grumberg and D A Peled Model Checking MIT Press Cambridge MA 1999 A Church Logic arithmetic and automata In Proceedings International Math ematical Congress 1962 The DOT Language http graphviz org doc info lang html C Fritz Constructing B chi automata from linear temporal logic using sim ulation relations for alternating B chi automata In O H Ibarra and Z Dang editors Conference on Implementation and Application of Automata CIAA 03 pages 35 48 2003 LNCS 2759 C Fritz and T Wilke State space reductions for alternating B chi automata In Foundations of Software Technology and Theoretical Computer Science pages 157 168 Kanpur India December 2002 Springer Verlag LNCS 2556 S Gurumurthy R Bloem and F Somenzi Fair simulation minimization In E Brinksma and K G Larsen editors Fourteenth Conference on Com puter Aided Verification CAV 02 pages 610 623 Springer Verlag Berlin July 2002 LNCS 2404 S Gurumurthy O Kupferman F Somenzi and M Y Vardi On complementing nondeterministic B chi automata In Correct Hardware Design and Verifica
35. ogics and automata on infinite words 1 2 Why use Lily Writing both a specification and an implementation and subsequently checking whether the latter satisfies the former seems wasteful A much more attractive approach is to automatically construct the implementation from the specification leaving the designer with only the task of ensuring that the specification describes the intended behavior The benefit is even more pronounced when one takes into effect the costs for debugging the manual implementation and of redesigning it when the specification changes Due to the complexity of the problem the size of the specification is limited Nev ertheless the ability to synthesize small specifications is also very useful For instance it can be used to synthesize functional models on the block level or it can help engineer to get familiar with properties more easily Our tool provides several optimizations to make synthesis more competitive We have applied our optimizations to synthesize several examples and achieved a sig nificant improvement over the straightforward implementation Lily constitutes the Property Based Synthesis Tool Introduction e 1 first implementation of a synthesis algorithm for the linear part of PSL We believe that the optimizations implemented in our tool and discussed in Section 5 form an important step towards making linear time synthesis practical 1 3 Features List Table 1 reports the status of the featu
36. omputer Science LICS 06 2006 To appear A Pnueli The temporal logic of programs In JEEE Symposium on Foundations of Computer Science pages 46 57 Providence RI 1977 N Piterman A Pnueli and Y Sa ar Synthesis of reactive 1 designs In Proc Verification Model Checking and Abstract Interpretation VM CAI 06 pages 364 380 2006 A Pnueli and R Rosner On the synthesis of a reactive module In Proc Symposium on Principles of Programming Languages POPL 89 pages 179 190 1989 Perl http www perl com or http www perl org R Rosner Modular Synthesis of Reactive Systems PhD thesis Weizmann Institute of Science 1992 S Safra On the complexity of automata In Symposium on Foundations of Computer Science pages 319 327 October 1988 F Somenzi and R Bloem Efficient B chi automata from LTL formulae In E A Emerson and A P Sistla editors Twelfth Conference on Computer Aided Ver ification CAV 00 pages 248 263 Springer Verlag Berlin July 2000 LNCS 1855 W Thomas On the synthesis of strategies in infinite games In Proc 12th Annual Symposium on Theoretical Aspects of Computer Science pages 1 13 Springer Verlag 1995 LNCS 900 M Vardi A game theoretic approach to automated program generation Presentation at IFIP Working Group 2 11 Second Meeting Available from http www cs rice edu taha wg2 11 m 2 2005 URL http vlsi colorado edu vis N Wallmeier P Hiitt
37. on Property Based Synthesis Tool 1 4 History of Synthesis LTL synthesis was proposed in PR89 The key to the solution is the observation that a program with input signals and output signals O can be seen as a com plete E labeled D tree with X 2 and D 2 the label of node t D gives the output after input sequence t The solution proposed in PR89 is to build a nondeterministic B chi word automaton for the specification and then to convert this automaton to a deterministic Rabin automaton that recognizes all Z labeled D trees satisfying the specification A witness to the nonemptiness of the automaton is an implementation of the specification There are two reasons that this approach has not been followed by an implemen tation The first reason is that synthesis of LTL properties is 2EXPTIME complete Ros92 The second is that the solution uses an intricate determinization construc tion Saf88 that is hard to implement and very hard to optimize The first reason should not prevent one from implementing the approach After all the bound is a lower bound and a manual implementation is also subject to it Cf Var05 Thus the complexity of verifying the specification on a manual implementation is not lower than that of automatically synthesizing the design In combination with the second reason however the argument gains strength For many speci fications a doubly exponential blow up is not necessary but can only be avoided
38. ory to the beginning of the library path to ensure that the right version is used The same holds for setting the search path explained below Add source directory to the search path e g export PATH opt lily PATH or setenv PATH opt lily S PATH Property Based Synthesis Tool 4 Technical Details In this section we give some details about how we implemented and tested Lily In the first part we talk about the programming language and provide a diagram of the program structure In the second part we discuss the examples we used to test our implementation 4 1 Implementation Lily is written in Perl 5 Perl is a dynamic procedural programming language which summarizes features from C shell scripting AWK sed Lisp and many other programming languages in an easy to use way In Perl 5 features were added that support complex data structures first class functions and an object oriented programming model We make extensive use of these features Lily is implemented according to the object oriented paradigm Figure 3 shows a block diagram of the structure illustrating the major parts of Lily and the connection between Lily and Wring The rounded rectangles represent the major functional parts and the wavelike rectangles represent the data structures Rounded rectangles in grey belong to Lily The single rounded rectangle in white represents Wring Wring from the University of Colorado SB00 GBS02
39. p A8 02 In particular for a state 0 Q if q d S q Xawr qd andg O q 0 then S O SN q O q Thus by Theorem 4 we can remove 4 from such sets Likewise if Angry contains two simulation equivalent states S O and S O we keep only one preferring the one with smaller cardinality Finally we can use Theorem 6 to remove states that have a simulating sibling Removing Inconsistent States In KVO5 it is shown that it is not necessary to include states S O such that q i and q j S with i Z j This implies that we can use the following optimization Theorem 17 Let Ayn E D Q q0 0 8 22 x 0 be as in Definition 15 with Q Q S O 3 g i g j S i zz j The transition relation 9 is obtained from amp by replacing for all C 8 q 6 and all S O C state S O by S O0 where S is obtained from S by removing all states q j with j not minimal and O is obtained from O by replacing q j O by q j if q j ES and q j S We have L Anpre L Angr LI This is an important theorem as it reduces the number of states in the NBT to k 1 instead of 2 where n is the number of states in Auc On the Fly Computation Suppose Anpt X D 0 490 0 Instead of build ing Angr in full we construct an NBT Axgr k X D Q q9 6 1 Q such that qo Q C Q and for q Q either 6 q 6 9 q 0 for all o or 9 6
40. qo If it is in state q in state of the input tree and is labeled o then 6 q 6 tells A what to do next The automaton can nondeterministically choose a C 8 q 6 Then for all d q C A moves to node t d in state q The transition relation 8 q 6 can be considered as a DNF formula over D x Q Note that there are no runs with a node t q for which g t 1 0 On the other hand a run that visits a node t needs not visit all of its children there are no restrictions on the subtrees rooted in a node that is not visited In particular a node t q such that 5 q t t 0 does not have any children and there are no restrictions on the subtree rooted in f An automaton is universal if q 1 1 A universal automaton has at most one run for a given input An automaton is nondeterministic if for all q c Q o c C 5 q 6 and di qi dj q C we have d d implies q qj That is the au tomaton can only send one copy in each direction and a run is isomorphic to the input tree An automaton is deterministic if it is both universal and nondetermin istic An automaton is a word automaton if D 1 In that case we can leave out D altogether We will abbreviate alternating nondeterministic universal deterministic B chi co B chi weak tree word automaton as a three letter acronym A N U D B C W T W We will use X labeled D trees to model programs with input alphabet D and output alphabet X In orde
41. r to establish a link with the PSL specification we will assume that D 2 and X 2 Thus a path of a X labeled D tree can be seen as a word over ZU D we merge the label of the node with the direction edge following it in the path Given a word language L ZU D let T L C Ty be the set of trees T such that all paths of T are in L For a word automaton A we will write T A for T L A Similarly we will write T for the set of trees T such that every path of T satisfies the PSL formula q A Moore machine with output alphabet X and input alphabet D is a tuple M X D S s9 T G such that S is a finite set of states so S is the initial state T S x D Sis the transition function and G S X is the output function We extend T to the domain S x X in the usual way The input output language L M of M is ix e LUD m 954 01 4 04 G T goidi a1 Every Moore machine corresponds to a complete X labeled D tree for which every node 1 D is labeled with G T qo t Thus every tree language T C Tg p defines a set M T of Moore machines those machines M for which T L M T Note that not every tree can be defined by a Moore machine and thus there are T for which U T L M M M T AT 20 e Underlying Theory Property Based Synthesis Tool 5 2 Simplifying tree automata In this section we discuss two optimizations that can be used for any tree automa ton Simplification Using Games
42. res stated in the Description of Work docu ment for this tool The list contains mandatory desirable and nice to have features with the inten tion that the minimal requirement for this deliverable is the implementation of all mandatory features Other features are not explicitly requested to fulfill the due of the deliverable We implemented all mandatory and desirable features Present Reference Mandatory Features Pointers to algorithms used YES 5 List of target operating systems YES 3 1 Explanation of coding standards YES 4 1 Discussion of license issues YES 3 2 User documentation including documentation of YES 2 Appendix user interface command line switches and im ported exported file formats Test suite YES 4 2 Standard Input Language PSL YES 2 1 Support for Verilog Flavor YES 2 1 Appendix Synthesis of the linear part of PSL LTL like YES 5 Outputs Verilog YES 2 4 Desirable features Efficient for weak properties weakness expresses an YES 5 3 First Section automata theoretic notion of expressibility Nice to have features Support for other flavors NO Efficient synthesis for all of the linear subset of PSL NO Table 1 Table of features We have implemented optimizations to speed up the synthesis process for strong properties as well Even though the optimizations work very well for many cases there are still specifications where they do not help cf First Section of 5 3 2 e Introducti
43. t Equivalent lt gt lt gt Not Temporal operator LTL flavor PSL flavor Next X next Existential Next next e n m Universal Next next a n m Strong Until U until Strong Release R V Always G always Strong Eventually F eventually Property Based Synthesis Tool Usage e 5 We present an example to show what the formulas and the corresponding specifi cation files look like A detailed syntax description for the specification file can be found in Appendix A 1 Example 1 We specify a small traffic light system for a crossing of a highway and a farm road The systems has only two lights which are either green or red Signals hl and fl which are output signals encode these two lights The highway light is green iff hl 1 and similarly for the crossing farm road and fl The input signal car indicates that a car is waiting at the farm road and timer represents the expiration of a timer The specification assumes that the timer expires regularly It requires that a green lamp stays green until the timer expires Furthermore one of the lamps must always be red every car at the farm road is eventually allowed to drive on and the highway lamp is regularly set to green Below we show the specification file for Lily in PSL and LTL flavor Specification file for Example 1 in PsL flavor assume always eventually timer assert always hl amp f1 assert always eventually hl assert always car gt event
44. t 0 1 omh 0 1 omhc 0 1 oedges 0 1 orelease 0 1 oreuse 0 1 With the command line options inherited from Wring the user can determine the name of the specification file the prefix for the output files verbosity and pa rameters for the construction of Biichi automata provided by Wring A detailed description of those options is shown in Table 3 Property Based Synthesis Tool Usage e 7 Command c num comp f formula h ltl file m method o 0 1 p prefix s num v level ver num mon file auto file Table 3 Command line options inherited from Wring Result Iff num Z 0 make the transition relation of the automaton complete Off by default Build B chi automaton and its complement for the given LTL formula The LTL formula to be translated Use either Itlor t Gives help on the usage File containing the LTL formulae to be trans lated Use either 1t1 or f Sets the method used in translation Method ranges over GPVW GPVW LTL2AUT Boolean Default is Boolean Optimize the automaton after translation us ing simulation relations On by default Sets the prefix of the files that are written De fault values is 1t12aut Iff num Z 0 simplify the formula before trans lating it using rewriting On by default Sets the verbosity level 0 lt level lt 4 De fault is 1 Iff num 0 make an attempt at verifying the automaton Off by default Write a V
45. t C 2P is called a transition and a C Q is the acceptance condition We denote by A for q Q the automaton A with the initial state q A run R p of A on a X labeled D tree T t isa T x Q labeled N tree satisfying the following constraints 1 p e 40 2 Ifr Ris labeled t q then there is a set d1 91 dk qx 8 q T t such that r has k children labeled t d q1 t dk qx We have two acceptance conditions B chi and co B chi A run R p of a B chi co B chi automaton is accepting if all infinite paths of R p have infinitely many states in a only finitely many states in 0 The language L A of A is the set of trees for which there exists an accepting run An ABT induces a graph The states of the automaton are the nodes of the graph and there is an edge from q to q if d q occurs in p q 0 for some o X and d D The automaton is weak if each strongly connected component SCC contains either only states in amp or only states not in a Intuitively A is a top down tree automaton for infinite trees A run of A is also a tree The nodes are labeled with pairs t q meaning that A is in state q in node t Property Based Synthesis Tool Underlying Theory e 19 of T Because A is alternating it can be in multiple states simultaneously for any given node For a given f there can be multiple q and nodes labeled f q in R The automaton starts at the root note in state
46. th 8 g 0 C 6 q 0 V d qi eC e i 1 i i is even Vq cavi i V d ahi C q q NN i is then L A wr L Aawrk Example 14 States n4 4 n5 4 and ns 3 top right are simulation equiva lent with n4 2 ns 2 and ns 1 respectively Using Theorem 4 we can remove states n4 4 ns 4 and ns 3 and redirect incoming edges to equivalent states Property Based Synthesis Tool Underlying Theory e 27 Furthermore the previous removal of the states on the bottom left implies that n3 4 lt n3 3 Since n2 4 has identical transitions to n3 4 and n3 3 The orem 6 allows us to remove the transition to n3 4 Thus n3 4 becomes un reachable and can be removed The same holds for ns 2 for a similar reason This optimization also allows us to remove states n4 4 n5 4 and ns 3 but Theorem 6 is not in general stronger than Theorem 4 The optimization of the edges due to Theorem 13 is already shown in Fig 7 Con sider for instance the transition from n2 4 to n3 4 Altogether we have reduced the number of states in the AWT from 22 to 5 The removal of edges is equally important as it reduces nondeterminism and makes the translation to an NBT more efficient NBT The next step is to translate Aawr to an NBT Angry with the same language KV05 MH84 Assume that A awr D Q q0 6 0 We first need some additional notation For C Q and o
47. tion Methods CHARME 03 pages 96 110 Berlin October 2003 Springer Verlag LNCS 2860 Graphviz Graph Visualization Software http graphviz org A Harding Symbolic Strategy Synthesis For Games With LTL Winning Condi tions PhD thesis University of Birmingham 2005 J E Hopcroft and J D Ullman Introduction to Automata Theory Languages and Computation Addison Wesley Reading MA 1979 Property Based Synthesis Tool References e 31 JB06a JB06b KV05 MH84 MP91 Pit06 Pnu77 PPS06 PR89 PRL Ros92 Saf88 SB00 Tho95 Var05 VIS WHTO03 B Jobstmann and R Bloem Game based and simulation based improvements for LTL synthesis In Third Workshop on Games in Design and Verification 2006 To Appear B Jobstmann and Roderick Bloem Optimizations for LTL synthesis In 6th Conferences on Formal Methods in Computer Aided Design FMCAD 06 2006 To Appear O Kupferman and M Vardi Safraless decision procedures In Symposium on Foundations of Computer Science FOCS 05 pages 531 542 2005 S Miyano and T Hayashi Alternating finite automata on w words Theoretical Computer Science 32 321 330 1984 Z Manna and A Pnueli The Temporal Logic of Reactive and Concurrent Sys tems Specification Springer Verlag 1991 N Piterman From nondeterministic B chi and Streett automata to deterministic parity automata In 2 st Symposium on Logic in C
48. tomaton with co B chi acceptance condition and universal branching mode Winning Strategy A recipe with which a player is guaranteed to win an infinite game no matter what the other player does A finite state strategy may depend on a finite memory of the past i e the move the strategy suggests can depend on previous moves of the two players A memoryless strategy depends only on the current state of the game Property Based Synthesis Tool Table of Figures e ix x e Table of Figures Property Based Synthesis Tool 1 Introduction In this document we introduce our tool Lily a LInear Logic sYnthesizer We de scribe what Lily is and what it can do We explain how to use Lily and provide a run ning example Furthermore we explain some details on the implementation and on the test suite Finally we present the theoretical background JB06a JB06b 1 1 What is Lily Lily is a linear logic synthesizer which synthesizes a functionally correct design from a formal specification Lily is a command line tool written in Perl Lily takes a set of PSL or LTL properties and a partition of the used signals into input and output signals If the given specification is realizable Lily provides a design with the stated input and output signals that fulfills the specification The design is a state machine represented as a VERILOG module or as a directed graph in DOT format Lily is implemented on top of Wring SB00 GBS02 a toolkit for linear l
49. ually f1 assert always hl j hl until timer assert always fl gt fl until timer Specification file for Example 1 in LTL flavor G F timer 1 gt G fl 1 gt fl 1 U timer 1 G hl 1 gt hl 1 U timer 1 G car l gt F fl 1 G F hl 1 G hl 1 fl 1 2 2 Partition File The partition file divides the signals used in the specification file into input and output signals In Example 1 we have the four signals car timer fl and hl The first two are input signals the later are output signals The corresponding partition file is shown below and a detailed syntax description is provided in Appendix A 2 6 e Usage Property Based Synthesis Tool Partition file for Example 1 inputs timer car outputs hl fl 2 3 Command Line Options Lily is invoke with the command 1t12aut pl All command line options valid in Wring are valid in Lily as well since Lily uses Wring to construct a B chi automaton in its first step Below we show the original Wring command and the new Lily command Wring Command ltl2aut pl c 0 1 f formula h ltl file m method o 0 1 p prefix s 0 1 v n ver 0 1 auto file mon file Lily Command ltl2aut pl c 0 1 f formula h ltl file m method o 0 1 p prefix s 0 1 v n ver 0 1 auto file mon file syn file syndir synthesisDir mc ouct 0 1 oawt 0 1 owi
Download Pdf Manuals
Related Search