Skip to main content
SpringerLink
Log in

Synthesizing Controllers for Automation Tasks with Performance Guarantees

  • Conference paper
Model Checking Software (SPIN 2013)

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

Included in the following conference series:

Abstract

We present an extension of the MGSyn toolbox that allows synthesizing parallelized controller programs for industrial automation with performance guarantees. We explain the underlying design, outline its algorithmic optimizations, and exemplify its usage with examples for controlling production systems.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 380–395. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Cheng, C.-H., Geisinger, M., Ruess, H., Buckl, C., Knoll, A.: MGSyn: Automatic synthesis for industrial automation. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 658–664. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoretical Computer Science 318(3), 323–354 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  5. Droste, M., Kuich, W., Vogler, H.: Handbook of weighted automata. Springer (2009)

    Google Scholar 

  6. Ghallab, M., Howe, A., Krobnock, C., McDermott, D., Ram, A., Veloso, M., Weld, D., Wilkins, D.: PDDL-the planning domain definition language. Technical Report CVC TR-98003/DCS TR-1165, Yale Center for Computer Vision and Control (October 1998)

    Google Scholar 

  7. Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. fortiss GmbH, Guerickestr. 25, 80805, München, Germany

    Chih-Hong Cheng, Michael Geisinger & Christian Buckl

Authors
  1. Chih-Hong Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Geisinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian Buckl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Vienna, University of Technology, Austria

    Ezio Bartocci

  2. Department of Computer Science, Stony Brook University, 11794-4400, Stony Brook, NY, USA

    C. R. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cheng, CH., Geisinger, M., Buckl, C. (2013). Synthesizing Controllers for Automation Tasks with Performance Guarantees. In: Bartocci, E., Ramakrishnan, C.R. (eds) Model Checking Software. SPIN 2013. Lecture Notes in Computer Science, vol 7976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39176-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39176-7_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39175-0

  • Online ISBN: 978-3-642-39176-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation