Abstract
Supervisory Control Theory (SCT) is a model-based framework for automatically synthesizing a supervisor that minimally restricts the behavior of a plant such that given specifications is fulfilled. The main obstacle which prevents SCT from having a major industrial breakthrough is that the supervisory synthesis, consisting of a series of reachability tasks, suffers from the state-space explosion problem. To alleviate this problem, a well-known strategy is to represent and explore the state-space symbolically by using Binary Decision Diagrams. Based on this principle, an alternative symbolic state-space traversal approach, depending on the disjunctive partitioning technique, is presented in this paper. In addition, the approach is adapted to the prior work, the guard generation procedure, to extract compact propositional formulae from a symbolically represented supervisor. These propositional formulae, referred to as guards, are then attached to the original model, resulting in a modular and comprehensible representation of the supervisor.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ramadge, P.J.G., Wonham, W.M.: The Control of Discrete Event Systems. Proceedings of the IEEE 77, 81–98 (1989)
Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2008)
Balemi, S., Hoffmann, G.J., Gyugyi, P., Wong-Toi, H., Franklin, G.F.: Supervisory Control of a Rapid Thermal Multiprocessor. IEEE Transactions on Automatic Control 38, 1040–1059 (1993)
Feng, L., Wonham, W.M., Thiagarajan, P.S.: Designing Communicating Transaction Processes by Supervisory Control Theory. Formal Methods in System Design 30, 117–141 (2007)
Shoaei, M.R., Lennartson, B., Miremadi, S.: Automatic Generation of Controllers for Collision-Free Flexible Manufacturing Systems. In: 6th IEEE Conference on Automation Science and Engineering, pp. 368–373 (2010)
Akers, S.B.: Binary Decision Diagrams. IEEE Transactions on Computers 27, 509–516 (1978)
Bryant, R.E.: Symbolic Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys 24, 293–318 (1992)
Miremadi, S., Akesson, K., Lennartson, B.: Extraction and Representation of a Supervisor Using Guards in Extended Finite Automata. In: 9th International Workshop on Discrete Event Systems, pp. 193–199 (2008)
Hoare, C.A.R.: Communicating Sequential Processes. Communications of the ACM 21, 666–677 (1985)
Shannon, C.E., Weaver, W.: The Mathematical Theory of Communication. University of Illinois Press (1949)
Bollig, B., Wegener, I.: Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Transactions on Computers 45, 993–1002 (1996)
Aloul, F.A., Markov, I.L., Sakallah, K.A.: Force: A Fast and Easy-To-Implement Variable-Ordering Heuristic. In: 13th ACM Great Lakes symposium on VLSI, pp. 116–119 (2003)
Vahidi, A., Fabian, M., Lennartson, B.: Efficient Supervisory Synthesis of Large Systems. Control Engineering Practice 14, 1157–1167 (2006)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic Model Checking with Partitioned Transition Relations. In: International Conference on Very Large Scale Integration, vol. A-1, pp. 49–58 (1991)
Burch, J.R., Clarke, E.M., Long, D.E., Mcmillan, K.L., Dill, D.L.: Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13, 401–424 (1994)
Byröd, M., Lennartson, B., Vahidi, A., Åkesson, K.: Efficient Reachability analysis on Modular Discrete-Event Systems using Binary Decision Diagrams. In: 8th International Workshop on Discrete Event Systems, pp. 288–293 (2006)
Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement Learning: A Survey. Journal of Artificial Intelligence Research 4, 237–285 (1996)
Glover, F., Laguna, M.: Tabu Search. Journal of the Operational Research Society 5 (1997)
Åkesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica – An Integrated Environment for Verification, Synthesis and Simulation of Discrete Event Systems. In: 8th International Workshop on Discrete Event Systems, pp. 384–385 (2006)
JavaBDD, http://javabdd.sourceforge.net
Holloway, L.E., Krogh, B.H.: Synthesis of Feedback Control Logic for a Class of Controlled Petri Nets. IEEE Transactions on Automatic Control 35, 514–523 (1990)
Leduc, R.J.: Hierarchical Interface-Based Supervisory Control. In: 40th IEEE Conference on Decision and Control, pp. 4116–4121 (2002)
Murray Wonham, W.: Notes on Control of Discrete Event Systems. University of Toronto (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fei, Z., Miremadi, S., Åkesson, K., Lennartson, B. (2013). Symbolic State-Space Exploration and Guard Generation in Supervisory Control Theory. In: Filipe, J., Fred, A. (eds) Agents and Artificial Intelligence. ICAART 2011. Communications in Computer and Information Science, vol 271. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29966-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-29966-7_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29965-0
Online ISBN: 978-3-642-29966-7
eBook Packages: Computer ScienceComputer Science (R0)