Counterexample-Guided Synthesis of Observation Predicates

  • Rayna Dimitrova
  • Bernd Finkbeiner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)


We present a novel approach to the safety controller synthesis problem with partial observability for real-time systems. This in general undecidable problem can be reduced to a decidable one by fixing the granularity of the controller: finite sets of clocks and constants in the guards. Current state-of-the-art methods are limited to brute-force enumeration of possible granularities or manual choice of a finite set of observations that a controller can track. We address this limitation by proposing a counterexample-guided method to successively refine a set of observations until a sufficiently precise abstraction is obtained. The size of the abstract games and strategies generated by our approach depends on the number of observation predicates and not on the size of the constants in the plant. Our experiments demonstrate that this results in better performance than the approach based on fixed granularity when fine granularity is necessary.


Action Point Winning Strategy Symbolic Constant Controller Synthesis Predicate Abstraction 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    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
  3. 3.
    Cassez, F.: Efficient On-the-Fly Algorithms for Partially Observable Timed Games. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 5–24. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed Control with Observation Based and Stuttering Invariant Strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Algorithms for Omega-Regular Games with Imperfect Information,. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 287–302. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    de Alfaro, L., Roy, P.: Solving Games Via Three-Valued Abstraction Refinement. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 74–89. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    De Wulf, M., Doyen, L., Raskin, J.-F.: A Lattice Theory for Solving Games of Imperfect Information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153–168. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Dimitrova, R., Finkbeiner, B.: Abstraction refinement for games with incomplete information. In: Proc. FSTTCS 2008. Dagstuhl Seminar Proceedings, vol. 08004 (2008)Google Scholar
  9. 9.
    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
  10. 10.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-Guided Control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886–902. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Reif, J.H.: The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29(2), 274–301 (1984)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Rayna Dimitrova
    • 1
  • Bernd Finkbeiner
    • 1
  1. 1.Saarland UniversityGermany

Personalised recommendations