Abstract
Parameterized synthesis was recently proposed as a way to circumvent the poor scalability of current synthesis tools. The method uses cut-off results in token rings to reduce the problem to bounded distributed synthesis, and thus ultimately to a sequence of SMT problems. This solves the problem of scalability in the size of the architecture, but experiments show that the size of the specification is still a major issue. In this paper we propose several optimizations of the approach. First, we tailor the SMT encoding to systems with isomorphic processes and token-ring architecture. Second, we extend the cut-off results for token rings and refine the reduction, using modularity and abstraction techniques. Some of our optimizations also apply to isomorphic or distributed synthesis in arbitrary architectures. To evaluate these optimizations, we developed the first completely automatic implementation of parameterized synthesis. Experiments show a speed-up of several orders of magnitude, compared to the original method.
This work was supported in part by the European Commission through project DIAMOND (FP7-2009-IST-4-248613), and by the Austrian Science Fund (FWF) through the national research network RiSE (S11406).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Global State
- Label Transition System
- Parameterized Synthesis
- Strongly Connect Component
- Parameterized Architecture
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi Automata Translation: Fast and More Deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95–109. Springer, Heidelberg (2012)
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY – A New Requirements Analysis Tool with Synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425–429. Springer, Heidelberg (2010)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78, 911–938 (2012)
Chapiro, D.M.: Globally-asynchronous locally-synchronous systems. Ph.D. thesis, Stanford Univ., CA (1984)
Clarke, E.M., Talupur, M., Touili, T., Veith, H.: Verification by Network Decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 276–291. Springer, Heidelberg (2004)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Ehlers, R.: Symbolic bounded synthesis. Formal Methods in System Design 40, 232–262 (2012)
Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. International Journal of Foundations of Computer Science 14, 527–549 (2003)
Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011)
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Logic in Computer Science (LICS), pp. 321–330. IEEE Computer Society Press (2005)
Finkbeiner, B., Schewe, S.: SMT-based synthesis of distributed systems. In: Proc. Workshop on Automated Formal Methods, pp. 69–76. ACM (2007)
Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. on Software Tools for Technology Transfer, 1–21 (2012)
Jacobs, S., Bloem, R.: Parameterized Synthesis. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 362–376. Springer, Heidelberg (2012)
Katz, G., Peled, D.: Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 117–132. Springer, Heidelberg (2011)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)
Pnueli, A., Rosner, R.: Distributed systems are hard to synthesize. In: Foundations of Computer Science (FOCS), pp. 746–757. IEEE Computer Society Press (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khalimov, A., Jacobs, S., Bloem, R. (2013). Towards Efficient Parameterized Synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, vol 7737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35873-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-35873-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35872-2
Online ISBN: 978-3-642-35873-9
eBook Packages: Computer ScienceComputer Science (R0)