Advertisement

The Complexity of Bounded Synthesis for Timed Control with Partial Observability

  • Hans-Jörg Peter
  • Bernd Finkbeiner
Conference paper
  • 402 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)

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.

Keywords

Model Check Boolean Function Synthesis Problem Synthesis Algorithm Controller Synthesis 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 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. 3.
    Bouyer, P., Chevalier, F.: On the control of timed and hybrid systems. EATCS Bulletin 89, 79–96 (2006)MathSciNetzbMATHGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. 5.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  6. 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)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 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–206Google Scholar
  8. 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)CrossRefGoogle Scholar
  9. 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. 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. 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)CrossRefGoogle Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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)CrossRefGoogle Scholar
  14. 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)CrossRefGoogle Scholar
  15. 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. 16.
    Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theoretical Computer Science 221(1-2), 369–392 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22(3), 384–406 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975)zbMATHCrossRefGoogle Scholar
  19. 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. 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)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 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)CrossRefGoogle Scholar
  23. 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)CrossRefGoogle Scholar
  24. 24.
    Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc. (1967)Google Scholar
  25. 25.
    Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.): ATVA 2007. LNCS, vol. 4762. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  26. 26.
    Papadimitriou, C.H.: Computational complexity. Addison-Wesley (1994)Google Scholar
  27. 27.
    Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  28. 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. 29.
    Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)MathSciNetzbMATHCrossRefGoogle Scholar
  30. 30.
    Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, et al. [25], pp. 474–488Google Scholar
  31. 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)CrossRefGoogle Scholar
  32. 32.
    Veith, H.: Languages represented by boolean formulas. Inf. Process. Lett. 63(5), 251–256 (1997)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Hans-Jörg Peter
    • 1
    • 2
  • Bernd Finkbeiner
    • 2
  1. 1.Advanced Research Center, Atrenta Inc.GrenobleFrance
  2. 2.Department of Computer ScienceSaarland UniversitySaarbrückenGermany

Personalised recommendations