Bounded Synthesis for Streett, Rabin, and CTL* Overview
Delve into the world of bounded synthesis for Streett, Rabin, and CTL*, exploring LTL synthesis problems, a bounded approach, SMT-based synthesizers, encodings, and the significance of Streett/Rabin and CTL*. Understand CoBuchi and Streett automata, model checking synthesis, and more. Discover the essence of searching for bad cycles in graphs with CoBuchi ranking.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Bounded Synthesis for Streett, Rabin, and CTL* Ayrat Khalimov, Roderick Bloem Rigorous Systems Engineering
LTL synthesis problem Given: LTL formula ?, system inputs and outputs Return: system that satisfies ?, else unrealizable
Bounded Approach to LTL Synthesis [SF] LTL formula ? k = 1 search a system of size k increase k not found found is limit on k reached? NO system YES unrealizable
SMT-based bounded synthesizer [SF] LTL formula ? system size k ???? ? ???: (?,???) ?(????) ? system of size k unrealizable for k
Our results Known encodings: ??????? ?/?(????? ?/??? ?) New encodings: ??????? ?/? ???????/????? ??????? ??? First bounded synthesizer for (conjunctions of) Streett and Rabin automata, and branching logics.
Why Streett/Rabin and CTL*? Streett/Rabin automata - can be smaller than CoBuchi/Buchi CTL* - can express resettability property ????( ) - can be used for vacuity checking
We can focus on model checking synthesis ?? ????: (??,????) ?(????) ? (declare-datatypes () ((S s0 s1))) (declare-fun tau (S Bool) S) (declare-fun out (S) Bool) ; assertions to check ; (?,?0,?1) ?(????)
CoBuchi and Streett automata ( ,?,?0,?,???) CoBuchi acceptance ??? ? - Path is accepted if it does not visit ??? infinitely often Streett acceptance ??? = ?1,?1, ,(??,??) - Path is accepted if for all pairs (??,??): ?? is visited inf often -> ?? is visited inf often
Searching for bad cycles in graph ?????? ????????? with CoBuchi ranking [SF] 5 Rank maps a product state to a number: ? ? ??? CoBuchi ranking requires: exit normal state: exit bad state: < 5 5 < 4 UNSAT if require all paths to be good
Searching for one good path in graph ?????? ????????? with CoBuchi ranking [SF] 5 Rank maps a product state to a number: ? ? ??? CoBuchi ranking requires: exit normal state: exit bad state: < 5 < 5 5 SAT if search for one good path
New ranking for Streett acceptance ??? ? ??? ? 5 Rank maps a product state to a number: ? ? ??? Streett ranking requires: exit normal state: exit A state: < exit G state: reset 5 5 10
Conjoining E- and A- properties ?????? ? ?( ) We can solve SMT query for ?????? ?( ) ?????? ?( )
Encoding ?????? ??? into SMT ? ?? ??? ? ? ? ? ? ? ?? Introduce propositions for sub-formulas Encode ?????? ???? Encode ??????? ??????,????? ??? ? ? ???: ??: ?????? ???? ??? ??????,? ??? ?
Conclusion First bounded synthesizer for (conjunctions of) Streett and Rabin automata, and CTL*. https://github.com/5nizza/party-elli (branch cav17) Future directions: How to check unrealizability efficiently? [SYNT] Extend to multi-agent logics Efficiency: reduce to safety games and use BDDs
