Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Mathematical Foundations of Computer Science

MFCS 2013: Mathematical Foundations of Computer Science 2013 pp 45–49Cite as

Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development

  • Conference paper

  • 1421 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8087))

Abstract

Synthesis from temporal specifications is the automatic production of adaptable plans (or input enabled programs) from high level descriptions. The assumption underlying this form of synthesis is that we have two interacting reactive agents. The first agent is the system for which the plan / program is being designed. The second agent is the environment with which the system interacts. The exact mode of interaction and the knowledge available to each of the agents depends on the application domain.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of Büchi automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 262–272. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: Design Automation and Test in Europe, pp. 1188–1193 (2007)

    Google Scholar 

  3. Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification. Electronic Notes in Computer Science, vol. 190, pp. 3–16 (2007)

    Google Scholar 

  4. Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and Systems Science 78(3), 911–938 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Braberman, V., D’Ippolito, N., Piterman, N., Sykes, D., Uchitel, S.: Controller synthesis: From modelling to enactment. In: 35th International Conference on Software Engineering, San Francisco, USA (2013)

    Google Scholar 

  7. Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)

    MATH  Google Scholar 

  8. Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. I, pp. 3–50. Cornell University, Ithaca (1957)

    Google Scholar 

  9. Conner, D., Kress-Gazit, H., Choset, H., Rizzi, A., Pappas, G.: Valet parking without a valet. In: Proceedings IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 572–577. IEEE (2007)

    Google Scholar 

  10. D’Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behavior models for fallible domains. In: 33rd International Conference on Software Engineering. ACM, ACM Press (2011)

    Google Scholar 

  11. D’Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesising non-anomalous event-based controllers for liveness goals. Transactions on Software Engineering and Methodology 22(1) (2012)

    Google Scholar 

  12. Ehlers, R.: Symbolic bounded synthesis. Formal Methods in System Design 40(2), 232–262 (2012)

    Article  MATH  Google Scholar 

  13. Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 328–337 (1988)

    Google Scholar 

  14. Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Jobstmann, B., Bloem, R.: Game-based and simulation-based improvements for ltl synthesis. In: 3nd Workshop on Games in Design and Verification (2006)

    Google Scholar 

  17. Jurdziński, M.: Deciding the winner in parity games is in up ∩ co-up. Information Processing Letters 68(3), 119–124 (1998)

    Article  MathSciNet  Google Scholar 

  18. Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 199–212. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Barner, S., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 161–181. Springer, Heidelberg (2010)

    Google Scholar 

  20. Kress-Gazit, H., Fainekos, G., Pappas, G.: From structured english to robot motion. In: Proceedings IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 2717–2722. IEEE (2007)

    Google Scholar 

  21. Kress-Gazit, H., Fainekos, G., Pappas, G.: Where’s waldo? sensor-based temporal logic motion planning. In: Proc. IEEE International Conference on Robotics and Automation, pp. 3116–3121. IEEE (2007)

    Google Scholar 

  22. Kugler, H., Plock, C., Pnueli, A.: Controller synthesis from LSC requirements. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 79–93. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Kugler, H., Segall, I.: Compositional synthesis of reactive systems from live sequence chart specifications. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 77–91. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3), e5 (2007)

    Google Scholar 

  26. Piterman, N., Pnueli, A.: Faster solution of Rabin and Streett games. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 275–284. IEEE, IEEE Computer Society Press (2006)

    Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179–190 (1989)

    Google Scholar 

  29. Rabin, M.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  30. Raman, V., Piterman, N., Kress-Gazit, H.: Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In: IEEE International Conference on Robotics and Automation. IEEE, IEEE Computer Society Press (2013)

    Google Scholar 

  31. Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319–327 (1988)

    Google Scholar 

  32. Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  33. Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of büchi complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 261–271. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  35. Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning for dynamical systems. In: IEEE Conference on Decision and Control, pp. 5997–6004. IEEE Computer Society Press (2009)

    Google Scholar 

  36. Wongpiromsarn, T., Topcu, U., Murray, R.M.: Automatic synthesis of robust embedded control software. In: AAAI Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems (2010)

    Google Scholar 

  37. Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon control for temporal logic specifications. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, pp. 101–110. ACM (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Leicester, UK

    Nir Piterman

Authors
  1. Nir Piterman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Science and Technology, 3400, Klosterneuburg, Austria

    Krishnendu Chatterjee

  2. Charles University, 11800, Prague, Czech Republic

    Jirí Sgall

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Piterman, N. (2013). Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development. In: Chatterjee, K., Sgall, J. (eds) Mathematical Foundations of Computer Science 2013. MFCS 2013. Lecture Notes in Computer Science, vol 8087. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40313-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40313-2_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40312-5

  • Online ISBN: 978-3-642-40313-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation