Skip to main content
SpringerLink
Log in

Certainly Unsupervisable States

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2013)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 419))

Abstract

This paper proposes an abstraction method for compositional synthesis. Synthesis is a method to automatically compute a control program or supervisor that restricts the behaviour of a given system to ensure safety and liveness. Compositional synthesis uses repeated abstraction and simplification to combat the state-space explosion problem for large systems. The abstraction method proposed in this paper finds and removes the so-called certainly unsupervisable states. By removing these states at an early stage, the final state space can be reduced substantially. The paper describes an algorithm with cubic time complexity to compute the largest possible set of removable states. A practical example demonstrates the feasibility of the method to solve real-world problems.

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 EPUB and 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

References

  1. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, pp. 109–120, Vienna, Austria (2001)

    Google Scholar 

  2. Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 1–20. Springer, Heidelberg (1995)

    Google Scholar 

  3. Aziz, A., Singhal, V., Swamy, G.M., Brayton, R.K.: Minimizing interacting finite state machines: a compositional approach to language containment. In: Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD ’94, pp. 255–261 (1994)

    Google Scholar 

  4. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  5. Baier, C., Klein, J., Klüppelholz, S.: A compositional framework for controller synthesis. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 512–527. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Fabian, M.: On object oriented nondeterministic supervisory control. Ph.D. thesis, Chalmers University of Technology, Göteborg, Sweden. https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=1126 (1995)

  7. Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 112–127. Springer, Heidelberg (2010)

    Google Scholar 

  8. Flordal, H., Malik, R.: Compositional verification in supervisory control. SIAM J. Control Opt. 48(3), 1914–1938 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  9. Flordal, H., Malik, R., Fabian, M., Åkesson, K.: Compositional synthesis of maximally permissive supervisors using supervision equivalence. Discrete Event Dyn. Syst. 17(4), 475–504 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  10. Gohari, P., Wonham, W.M.: On the complexity of supervisory control design in the RW framework. IEEE Trans. Syst. Man Cybern. 30(5), 643–652 (2000)

    Article  Google Scholar 

  11. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  12. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Boston (2001)

    MATH  Google Scholar 

  13. Lin, F., Wonham, W.M.: Decentralized control and coordination of discrete-event systems with partial observation. IEEE Trans. Autom. Control 35(12), 1330–1337 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  14. Malik, R.: The language of certain conflicts of a nondeterministic process. Working Paper 05/2010, Dept. of Computer Science, University of Waikato, Hamilton, New Zealand. http://hdl.handle.net/10289/4108 (2010)

  15. Malik, R., Streader, D., Reeves, S.: Conflicts and fair testing. Int. J. Found. Comput. Sci. 17(4), 797–813 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  16. Mohajerani, S., Malik, R., Fabian, M.: A framework for compositional synthesis of modular nonblocking supervisors. IEEE Trans. Autom. Control. 59(1), 150–162 (2014)

    Google Scholar 

  17. Mooij, A.J., Stahl, C., Voorhoeve, M.: Relating fair testing and accordance for service replaceability. J. Logic Algebr. Program. 79(3–5), 233–244 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  18. Nuutila, E.: Efficient transitive closure computation in large digraphs. Acta Polytechnica Scandinavica, Mathematics and Computing in Engineering Series, vol. 74. Finnish Academy of Technology, Helsinki (1995)

    MATH  Google Scholar 

  19. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 179–190 (1989)

    Google Scholar 

  20. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2), 285–309 (1955)

    Article  MATH  MathSciNet  Google Scholar 

  21. Wonham, W.M.: On the control of discrete-event systems. In: Nijmeijer, H., Schumacher, J.M. (eds.) Three Decades of Mathematical System Theory. LNCIS, vol. 135, pp. 542–562. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Waikato, Hamilton, New Zealand

    Simon Ware & Robi Malik

  2. Department of Signals and Systems, Chalmers University of Technology, Gothenburg, Sweden

    Sahar Mohajerani & Martin Fabian

Authors
  1. Simon Ware
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robi Malik
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sahar Mohajerani
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Fabian
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robi Malik .

Editor information

Editors and Affiliations

  1. AIST, Research Institute for Secure Systems, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo Department of Informatics, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Ware, S., Malik, R., Mohajerani, S., Fabian, M. (2014). Certainly Unsupervisable States. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05416-2_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05415-5

  • Online ISBN: 978-3-319-05416-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation