Skip to main content
Springer Nature Link
Log in

The Complexity of Bounded Synthesis for Timed Control with Partial Observability

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2012)

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

  • 517 Accesses

Abstract

We revisit the synthesis of timed controllers with partial observability. Bouyer et al. showed that timed control with partial observability is undecidable in general, but can be made decidable by fixing the granularity of the controller, resulting in a 2ExpTime-complete problem. We refine this result by providing a detailed complexity analysis of the impact of imposing a bound on the size of the controller, measured in the number of locations. Our results identify which types of bounds are useful (and which are useless) from an algorithmic perspective. While bounding the number of locations without fixing a granularity leaves the problem undecidable, bounding the number of locations and the granularity reduces the complexity to NExpTime-complete. If the controller is restricted to be a discrete automaton, the synthesis problem becomes PSpace-complete, and, for a fixed granularity of the plant, even NPTime-complete. In addition to the complexity analysis, we also present an effective synthesis algorithm for location-bounded discrete controllers, based on a symbolic fixed point computation. Synthesis of bounded controllers is useful even if the bound is not known in advance. By iteratively increasing the bound, the synthesis algorithm finds the smallest, and therefore often most useful, solutions first.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (China (P.R.))
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 37.44
Price includes VAT (China (P.R.))
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 46.00
Price excludes VAT (China (P.R.))
  • 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.

Similar content being viewed by others

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Lafay, J.-F. (ed.) Proc. 5th IFAC Conference on System Structure and Control, pp. 469–474. Elsevier (1998)

    Google Scholar 

  3. Bouyer, P., Chevalier, F.: On the control of timed and hybrid systems. EATCS Bulletin 89, 79–96 (2006)

    MathSciNet  MATH  Google Scholar 

  4. Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed Control with Partial Observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  6. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, et al. [25], pp. 192–206

    Google Scholar 

  8. Cassez, F., Henzinger, T.A., Raskin, J.-F.: A Comparison of Control Problems for Timed and Hybrid Systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Chatain, T., David, A., Larsen, K.G.: Playing games with timed games. In: Giua, A., Silva, M., Zaytoon, J. (eds.) Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009), Zaragoza, Spain (September 2009)

    Google Scholar 

  10. Chen, T., Lu, J.: Towards the complexity of controls for timed automata with a small number of clocks. In: Ma, J., Yin, Y., Yu, J., Zhou, S. (eds.) FSKD (5), pp. 134–138. IEEE Computer Society (2008)

    Google Scholar 

  11. D’Souza, D., Madhusudan, P.: Timed Control Synthesis for External Specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 571–582. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Ehlers, R.: Symbolic Bounded Synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365–379. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Filiot, E., Jin, N., Raskin, J.-F.: An Antichain Algorithm for LTL Realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Finkbeiner, B., Peter, H.-J.: Template-Based Controller Synthesis for Timed Systems. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 392–406. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Finkbeiner, B., Schewe, S.: SMT-based synthesis of distributed systems. In: Proceedings of the 2nd Workshop on Automated Formal Methods (AFM 2007), Atlanta, Georgia, USA, November 6, pp. 69–76. ACM Press (2007)

    Google Scholar 

  16. Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theoretical Computer Science 221(1-2), 369–392 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  17. Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22(3), 384–406 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  18. Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975)

    Article  MATH  Google Scholar 

  19. Kupferman, O., Lustig, Y., Vardi, M.Y., Yannakakis, M.: Temporal synthesis for bounded systems and environments. In: Schwentick, T., Dürr, C. (eds.) STACS. LIPIcs, vol. 9, pp. 615–626. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

    Google Scholar 

  20. Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking Timed Automata with One or Two Clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Lozano, A., Balcázar, J.L.: The Complexity of Graph Problems for Succinctly Represented Graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol. 411, pp. 277–286. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  22. Lustig, Y., Vardi, M.Y.: Synthesis from Component Libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 395–409. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Maler, O., Pnueli, A., Sifakis, J.: On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract). In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  24. Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc. (1967)

    Google Scholar 

  25. Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.): ATVA 2007. LNCS, vol. 4762. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  26. Papadimitriou, C.H.: Computational complexity. Addison-Wesley (1994)

    Google Scholar 

  27. Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  28. Rintanen, J.: Complexity of planning with partial observability. In: Zilberstein, S., Koehler, J., Koenig, S. (eds.) ICAPS, pp. 345–354. AAAI (2004)

    Google Scholar 

  29. Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  30. Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, et al. [25], pp. 474–488

    Google Scholar 

  31. Thomas, W.: On the Synthesis of Strategies in Infinite Games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  32. Veith, H.: Languages represented by boolean formulas. Inf. Process. Lett. 63(5), 251–256 (1997)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Advanced Research Center, Atrenta Inc., 38000, Grenoble, France

    Hans-Jörg Peter

  2. Department of Computer Science, Saarland University, 66123, Saarbrücken, Germany

    Hans-Jörg Peter & Bernd Finkbeiner

Authors
  1. Hans-Jörg Peter
    View author publications

    Search author on:PubMed Google Scholar

  2. Bernd Finkbeiner
    View author publications

    Search author on:PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Warwick, CV4 7AL, Coventry, UK

    Marcin Jurdziński

  2. Business Unit Safe and Autonomous Systems, Department of Safety and Security, AIT Austrian Institute of Technology, Donau-City-Str. 1, 1220, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Peter, HJ., Finkbeiner, B. (2012). The Complexity of Bounded Synthesis for Timed Control with Partial Observability. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. http://doi.org/10.1007/978-3-642-33365-1_15

Download citation

  • DOI: http://doi.org/10.1007/978-3-642-33365-1_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33364-4

  • Online ISBN: 978-3-642-33365-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics