Synthesis of Reactive Systems and Parameterized Party Solution
Delve into the innovative approach of synthesizing reactive systems through parameterized solutions offered by PARTY. Explore how PARTY addresses the synthesis challenges for token rings and asynchronous composition of processes. Gain insights into the ideas and methodologies behind this cutting-edge tool.
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
PARTY PARTY parameterized synthesis of token rings Ayrat Khalimov, Swen Jacobs, Roderick Bloem
synthesis of reactive systems ?1 ?1 arbiter (FSM) ?2 ?2 Specification: ? ?1 ??1 ? ?2 ??2 "?? ???????? ??????"//too big for 5min talk ? (?1 ?2) 2
P P P P P P P P P P P P ?: ? ?? ??? ?: "?? ???????? ??????" ? ?: ? (?? ??) Synthesize s.t.: ?: ????(?) P 3
why? Synthesis time for an arbiter for different number of clients: because synthesis tools do not scale 4
parameterized synthesis problem that PARTY solves given parameterized specification Spec P synthesize FSM such that: ?: ????????? ????(?) asynchronous composition of n processes (FSM) P one-directional token ring ?: ? ? ?:?(?) e.g. n=4: 5
ideas behind PARTY 1. Cutoffs in token rings [EN95]: a large token ring satisfies a spec if and only if a small token ring of cutoff size satisfies the spec 2. SMT-based bounded synthesis [FS07]: bound the number of states in the implementation, synthesize, if solution not found increase the bound 6
an example: synthesis of an arbiter Specification: - ?: ? ?? ??? - ?: "?? ???????? ??????" - ? ?: ? (?? ??) According to [EN95]cutoff=4: P P , , , P P P 7
an arbiter example: PARTY show case Synthesis time for full arbiter for different number of clients: 8
conclusion PARTY supports: 1. parameterized synthesis of token rings [KJB13] 2. SMT-based bounded synthesis [FS07] Available at https://github.com/5nizza/Party 10
