|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Synthesis from Temporal Specifications
If you have a question about this talk, please contact Thomas Tuerk.
Speaker: Nir Piterman
One of the most ambitious goals in the field of verification is to automatically produce designs from their specifications, a process called synthesis. We are interested in reactive systems, systems that continuously interact with other programs, users, or their environment (like CPUs). The complexity of reactive system does not necessarily arise from computing complicated functions but rather from the fact that they have to be able to react to all possible inputs and maintain their behavior forever. Classical solutions to synthesis use either two player games or tree automata and require the construction of deterministic automata. However, determinization for automata on infinite words is extremely complicated and does not work well in practice. Here we suggest a syntactic approach that restricts the kind of properties users are allowed to write. We claim that this approach is general enough and can be extended to cover most properties written in practice. The main advantage of our approach is that it is tailored to the use of BDDs and uses the structure of given properties to handle them more efficiently. We discuss how to extend our approach to handle more general properties and a few open issues.
This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listscu palestine society Kavli Institute for Cosmology Seminar Magdalene Society of Medievalists
Other talksCPP Seminar: Aspirations and the Capability Approach: Implications for Public Policy in Education and Health Microdroplets in Action Symposium Revealing the AGN (negative) feedback through broad wings of CO emission lines “Variability in Psychological Reactivity: Vulnerability, Differential Susceptibility, or Vantage Sensitivity?” Quantum black holes from gauge/string duality Surface Plasmon Resonance (Biacore)