A qualitative assessment of \(\alpha \)Rby in the perspective of the supervisory control theory

  • Maxime Routhier
  • Richard St-DenisEmail author
Regular Paper


It becomes more and more evident today that SAT-solving approaches have the potential to verify properties and synthesize supervisors of controlled systems described with a high level of abstraction. Such approaches can be particularly appropriate when engineers give more importance to decentralized, hierarchical, and parameterized control paradigms than to centralized ones in the design of systems composed of multiple small agents. One advantage of declarative programming languages, such as relational logic, in specifying control problems, including their underlying properties and reasoning methods, is their proximity to the mathematical objects used in the formulation of the theory itself, which allows for implementing new fragments of it faster. The disadvantage is, however, that SAT-solving approaches do not lend themselves to efficient calculations of auxiliary objects involved in some control problems, even if they can be described with the logic at hand. In some cases, the latter is not sufficiently powerful to express the entire solution logically. Such difficulties can be circumvented with \(\alpha {\textsc {Rby}}\), a fusion of Alloy and Ruby. Based on earlier experiments conducted with Alloy, this paper provides a qualitative assessment of \(\alpha {\textsc {Rby}}\) and reports on the results of new experiments with two fragments of the supervisory control theory: state-based control and decentralized control.


Multi-paradigm programming language SAT solver Supervisor control theory Alloy \(\alpha \textsc {Rby}\) 


  1. 1.
    Åkesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: 2006 8th International Workshop on Discrete Event Systems (WODES), pp. 384–385 (2006)Google Scholar
  2. 2.
    Åkesson, K., Fabian, M., Flordal, H., Vahidi, A.: Supremica—a tool for verification and synthesis of discrete event supervisors. In: 11th Mediterranean Conference on Control and Automation (MED) (2003)Google Scholar
  3. 3.
    Bagheri, H., Tang, C., Sullivan, K.: TradeMaker: automated dynamic analysis of synthesized tradespaces. In: 36th International Conference on Software Engineering (ICSE), pp. 106–116 (2014)Google Scholar
  4. 4.
    Bagheri, H., Sullivan, K.: Model-driven synthesis of formally precise, stylized software architectures. Form. Asp. Comput. 28(3), 441–467 (2016)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Barati, M., St-Denis, R.: Behavior composition meets supervisory control. In: 2015 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 115–120 (2015)Google Scholar
  6. 6.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, New York (2008)CrossRefzbMATHGoogle Scholar
  7. 7.
    Claessen, K., Een, N., Sheeran, M., Sörensson, N., Voronov, A., Åkesson, K.: SAT-solving in practice, with a tutorial example from supervisory control. Discrete Event Dyn. Syst. Theory Appl. 19(4), 495–524 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Côté, D., Fraikin, B., Frappier, M., St-Denis, R.: A SAT-based approach for the construction of reusable control system components. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS 6959, pp. 52–67. Springer, Berlin (2011)Google Scholar
  9. 9.
    Côté, D., Embe Jiague, M., St-Denis, R.: Systems-theoretic view of component-based software development. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS 6921, pp. 163–181. Springer, Berlin (2012)Google Scholar
  10. 10.
    Côté, D., St-Denis, R.: Component-based method for the modeling and control of modular production systems. IEEE Trans. Control Syst. Technol. 21(5), 1570–1585 (2013)CrossRefGoogle Scholar
  11. 11.
    Demirezen, Z., Mernick, M., Gray, J., Bryant, B.: Verification of DSMLs using graph transformation: a case study with Alloy. In: 6th International Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa), Article No. 3 (2009)Google Scholar
  12. 12.
    Flanagan, D., Matsumoto, Y.: The Ruby Programming Language. O’Reilly, Cambridge (2008)Google Scholar
  13. 13.
    Fraikin, B., Frappier, M., St-Denis, R.: Modeling the supervisory control theory with Alloy. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS 7316, pp. 94–107. Springer, Berlin (2012)Google Scholar
  14. 14.
    Fraikin, B., Frappier, M., St-Denis, R.: Supervisory control theory with Alloy. Sci. Comput. Program. 94, 217–237 (2014)CrossRefGoogle Scholar
  15. 15.
    Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, Chapter 2, pp. 89–134. Elsevier, Amsterdam (2008)CrossRefGoogle Scholar
  16. 16.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis, Revised Edition. MIT Press, Cambridge (2012)Google Scholar
  17. 17.
    Khoury, J., Abdallah, C.T., Heileman, G.L.: Towards formalizing network architectural descriptions. In: Frappier, M., et al. (eds.) ABZ 2010. LNCS 5977, pp. 132–145. Springer, Berlin (2010)Google Scholar
  18. 18.
    Kim, J.S., Garlan, D.: Analyzing architectural styles. J. Syst. Softw. 83(7), 1216–1235 (2010)CrossRefGoogle Scholar
  19. 19.
    Kumar, R., Takai, S.: Inference-based ambiguity management in decentralized decision-making: decentralized control of discrete event systems. IEEE Trans. Autom. Control 52(10), 1783–1794 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Leduc, R.J.: Hierarchical Interface-Based Supervisory Control. Doctoral thesis, Graduate Department of Electrical and Computer Engineering, University of Toronto (2003)Google Scholar
  21. 21.
    Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRefGoogle Scholar
  22. 22.
    Liao, H., Wang, Y., Stanley, J., Lafortune, S., Reveliotis, S., Kelly, T., Mahlke, S.: Eliminating concurrency bugs in multithreaded software: a new approach based on discrete-event control. IEEE Trans. Control Syst. Technol. 21(6), 2067–2082 (2013)CrossRefGoogle Scholar
  23. 23.
    Maoz, S., Ringert, J.O., Rumpe, B.: Synthesis of component and connector models from crosscutting structural views. In: 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium of the Foundations of Software Engineering (ESEC/FSE), pp. 444–454 (2013)Google Scholar
  24. 24.
    Ma, C., Wonham, W.M.: Nonblocking Supervisory Control of State Tree Structure. LNCIS, vol. 317. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  25. 25.
    Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE), vol. 1, pp. 609–619 (2015)Google Scholar
  26. 26.
    Milicevic, A., Efrati, I., Jackson, D.: \(\alpha \)Rby–an embedding of alloy in Ruby. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS 8477, pp. 56–71. Springer, Berlin (2014)Google Scholar
  27. 27.
    Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)CrossRefGoogle Scholar
  28. 28.
    Ricker, L., Lafortune, S., Genc, S.: DESUMA: a tool integrating GIDDES and UMDES. In: 2006 8th International Workshop on Discrete Event Systems (WODES), pp. 392–393 (2006)Google Scholar
  29. 29.
    Sanchez, A., Reza, J., Douriet, J., Gonzalez, R.: A comparison of synthesis tools for supervisory controllers. In: 2003 European Control Conference (ECC), pp. 600–605 (2003)Google Scholar
  30. 30.
    Shayman, M.A., Kumar, R.: Supervisory control of nondeterministic systems with driven events via prioritized synchronization and trajectory models. SIAM J. Control Optim. 33(2), 469–497 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, pp. 135–152 (2013)Google Scholar
  32. 32.
    Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS 4424, pp. 632–647. Springer, Berlin (2007)Google Scholar
  33. 33.
    Tronci, E.: Automatic synthesis of controllers from formal specifications. In: Second International Conference on Formal Engineering Methods (ICFEM), pp. 134–143 (1998)Google Scholar
  34. 34.
    Tronci, E.: Formally modeling a metal processing plant and its closed loop specifications. In: 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE), pp. 151–158 (1999)Google Scholar
  35. 35.
    Tronci, E.: On computing optimal controllers for finite state systems. In: 36th IEEE Conference on Decision and Control (CDC), vol. 4, pp. 3592–3593 (1997)Google Scholar
  36. 36.
    Wang, Xi., Ray, A., Phoba, S., Liu, J.: J-DES: a graphical interactive package for analysis and synthesis of discrete event systems. In: 2003 American Control Conference (ACC), vol. 4, pp. 3405–3410 (2003)Google Scholar
  37. 37.
    Wonham, W.M.: Supervisory Control of Discrete-Event System. Electrical & Computer Engineering, University of Toronto, Technical Report ECE 1636F/1637S (2013)Google Scholar
  38. 38.
    Yadav, N., Felli, P., De Giacomo, G., Sardina, S.: Supremal realizability of behaviors with uncontrollable exogenous events. In: 23rd International Joint Conference on Artificial Intelligence (IJCAI), pp. 1176–1182 (2013)Google Scholar
  39. 39.
    Yoo, T.-S., Lafortune, S.: A general architecture for decentralized supervisory control of discrete-event systems. Discrete Event Dyn. Syst. Theory Appl. 12(3), 335–377 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Yoo, T.-S., Lafortune, S.: Decentralized supervisory control with conditional decisions: supervisor existence. IEEE Trans. Autom. Control 49(11), 1886–1904 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  41. 41.
    Zhang, Z., Wonham, W.M.: STCT: an efficient algorithm for supervisory control design. In: Caillaud, B., et al. (eds.) Synthesis and Control of Discrete Event Systems, pp. 77–100. Kluwer Academic Publisher, Boston (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2017

Authors and Affiliations

  1. 1.Département d’informatiqueUniversité de SherbrookeSherbrookeCanada

Personalised recommendations