Skip to main content
SpringerLink
Log in

Controllers with Minimal Observation Power (Application to Timed Systems)

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7561))

  • 917 Accesses

Abstract

We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.

Partly supported by ANR project ECSPER (JC09- 472677), ERC Starting Grant inVEST-279499, Danish-Chinese Center for Cyber Physical Systems (IDEA4CPS) and VKR Center of Excellence MT-LAB.

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. AlAttili, I., Houben, F., Igna, G., Michels, S., Zhu, F., Vaandrager, F.W.: Adaptive scheduling of data paths using uppaal tiga. In: QFM, pp. 1–11 (2009)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for Playing Games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Bouyer, P., Brihaye, T., Bruyre, V., Raskin, J.-F.: On the optimal reachability problem of weighted timed automata. Formal Methods in System Design 31(2), 135–175 (2007)

    Article  MATH  Google Scholar 

  5. Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal Strategies in Priced Timed Game Automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 148–160. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. 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 

  7. Brihaye, T., Bruyère, V., Raskin, J.-F.: On Optimal Timed Strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49–64. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  9. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient On-the-Fly Algorithms for the Analysis of Timed Games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 90–104. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Flexible Timeline-Based Plan Verification. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol. 5803, pp. 49–56. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: Quantitative Synthesis Tool. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 267–271. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Chatterjee, K., Majumdar, R., Henzinger, T.A.: Controller Synthesis with Budget Constraints. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 72–86. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. Dimitrova, R., Finkbeiner, B.: Abstraction refinement for games with incomplete information. In: FSTTCS. LIPIcs, vol. 2, pp. 175–186. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)

    Google Scholar 

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

    Chapter  Google Scholar 

  16. Majumdar, R., Tabuada, P. (eds.): HSCC 2009. LNCS, vol. 5469. Springer, Heidelberg (2009)

    Google Scholar 

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

    Chapter  Google Scholar 

  18. 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 

  19. Malinowski, J., Niebert, P., Reynier, P.-A.: A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 198–212. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Orlandini, A., Finzi, A., Cesta, A., Fratini, S.: TGA-Based Controllers for Flexible Plan Execution. In: Bach, J., Edelkamp, S. (eds.) KI 2011. LNCS, vol. 7006, pp. 233–245. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  21. Raskin, J.-F., Chatterjee, K., Doyen, L., Henzinger, T.A.: Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(3) (2007)

    Google Scholar 

  22. Reif, J.H.: The complexity of two-player games of incomplete information. Journal of Computer and System Sciences 29(2), 274–301 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  23. Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CISS, CS, Aalborg University, Denmark

    Peter Bulychev, Alexandre David & Kim Guldstrand Larsen

  2. National ICT Australia, Sydney, Australia

    Franck Cassez

  3. Computer Science Department, Université Libre de Bruxelles (U.L.B.), Belgium

    Jean-François Raskin

  4. LIF, Aix-Marseille University & CNRS, France

    Pierre-Alain Reynier

Authors
  1. Peter Bulychev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Franck Cassez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandre David
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Pierre-Alain Reynier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, IIT Bombay, Powai, 400076, Mumbai, Maharashtra, India

    Supratik Chakraborty

  2. Chennai Mathematical Institute, H1, SIPCOT IT Park, Kelambakkam, 603103, Siruseri, Tamil Nadu, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bulychev, P., Cassez, F., David, A., Larsen, K.G., Raskin, JF., Reynier, PA. (2012). Controllers with Minimal Observation Power (Application to Timed Systems). In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33386-6_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33385-9

  • Online ISBN: 978-3-642-33386-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation