Roberto Ziller
Skip Abstract Section
Abstract
Model checking and supervisor synthesis have been successful in solving different design problems related to discrete systems in the last decades. In this paper, we analyze some advantages and drawbacks of these approaches and combine them for mutual improvement. We achieve this through a generalization of the supervisory control problem proposed by Ramadge and Wonham. The objective of that problem is to synthesize a supervisor which constrains a system's behavior according to a given specification, ensuring controllability and coaccessibility. By introducing a new representation of the solution using systems of μ-calculus equations, we are able to handle these two conditions separately and thus to exchange the coaccessibility requirement by any condition that could be used in model checking. Well-known results on μ-calculus model checking allow us to easily assess the computational complexity of any generalization. Moreover, the model checking approach also delivers algorithms to solve the generalized synthesis problem. We include an example in which the coaccessibility requirement is replaced by fairness constraints. The paper also contains an analysis of related work by several authors.
- Antoniotti, M. and Mishra, B. 1996. NP-completeness of the supervisor synthesis problem for unrestricted CTL specifications. In Workshop on Discrete Event Systems. Edinburgh, Scotland, UK.Google Scholar
- Arnold, A. and Crubille, P. 1988. A linear algorithm to solve fixed-point equations on transition systems. Information Processing Letters 29, 2, 57--66. Google ScholarDigital Library
- Arnold, A., Vincent, A., and Walukiewicz, I. 2003. Games for synthesis of controllers with partial observation. Theor. Comput. Sci. 1, 303 (Jun.), 7--34. Google Scholar
- Asarin, E., Maler, O., and Pnueli, A. 1995. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, vol. 999. LNCS, Springer, Berlin. Google Scholar
- Browne, A., Clarke, E., Jha, S., Long, D., and Marrero, W. 1997. An improved algorithm for the evaluation of fixpoint expressions. Theore. Comput. Sci. 178, 1--2, 237--255. Google ScholarDigital Library
- Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 1992. Symbolic model checking: 1020 states and beyond. Information and Computation 98, 2 (June), 142--170. Google ScholarDigital Library
- Burstall, R. 1974. Program proving considered as hand simulation plus induction. In Congress on Information Processing, 308--312.Google Scholar
- Cassandras, C. G. and Lafortune, S. 1999. Introduction to Discrete Event Systems. Kluwer Academic Publishers, Boston, MA. Google Scholar
- Clarke, E. M., Emerson, E., and Sistla, A. 1986. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Trans. Progr. Lang. Syst. 8, 2, 244--263. Google ScholarDigital Library
- Clarke, E., Grumberg, O., and Long, D. 1993. Verification tools for finite state concurrent systems. In A Decade of Concurrency---Reflections and Perspectives, J. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds. Vol. 803. Springer-Verlag, Noordwijkerhout, Netherlands, 124--175. Google Scholar
- Clarke, Jr, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. The MIT Press, London. Google Scholar
- Cleaveland, R., Klein, M., and Steffen, B. 1992. Faster model checking for the modal μ-calculus. In Computer Aided Verification (CAV'92), G. Bochmann and D. Probst, Eds. LNCS, Vol. 663. Springer-Verlag, Heidelberg, Germany, 410--422. Google Scholar
- Dam, M. 1994. CTL* and ECTL* as fragments of the modal μ-calculus. Theore. Comput. Sci. 126, 1, 77--96. Google ScholarDigital Library
- de Alfaro, L., Henzinger, T., and Majumdar, R. 2001. From verification to control: dynamic programs for omega-regular objectives. In Proceedings of the 16th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., 279--290.Google Scholar
- Emerson, E. and Clarke, E. 1980. Characterizing correctness properties of parallel programs as fixpoints. In Colloquium on Automata, Languages and Programming (ICALP), LNCS, Vol. 85. Springer, Berlin, 169--181. Google Scholar
- Emerson, E. and Jutla, C. 1988. The complexity of tree automata and logics of programs. In Symposium on Foundations of Computer Science (FOCS). White Plains, New York, 328--337.Google Scholar
- Emerson, E. and Jutla, C. 1999. The complexity of tree automata and logics of programs. SIAM Journal on Computing 29, 1, 132--158. Google ScholarDigital Library
- Emerson, E. and Lei, C.-L. 1986a. Efficient model checking in fragments of the propositional mu-calculus. In IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Washington, D.C., 267--278.Google Scholar
- Emerson, E. and Lei, C.-L. 1986b. Temporal reasoning under generalized fairness constraints. In Symposium on Theoretical Aspects of Computer Science (STACS), B. Monien and G. Vidal-Naquet, Eds. LNCS, Vol. 210. Springer, Orsay, France, 21--36. Google Scholar
- Emerson, E. A., Jutla, C. S., and Sistla, P. 1993. On model-checking for fragments of μ-calculus. In Computer Aided Verification, C. Courcoubetis, Ed. LNCS, Vol. 697. Springer, Elounda, Greece, 385--396. Google Scholar
- Floyd, R. 1967. Mathematical aspects of computer science. In Proceedings of Symposia in Applied Mathematics, 19--32.Google Scholar
- Hoare, C. 1969. An axiomatic basis for computer programming. Communications of the ACM 12, 10 (Oct.), 576--583. Google ScholarDigital Library
- Hoffmann, G. and Wong-Toi, H. 1992. Symbolic synthesis of supervisory controllers. In Proceedings of the American Control Conference, Chicago, IL.Google Scholar
- Jiang, S. and Kumar, R. 2001. Supervisory control of discrete event systems with CTL* temporal logic specifications. In Proceedings of the of the 40th IEEE Conference on Decision and Control, Orlando, FL.Google Scholar
- Jurdziński, M. 1998. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters 68, 3, 119--124. Google ScholarCross Ref
- Kirsten, D. 2002. Alternating tree automata and parity games. In Automata, Logics, and Infinite Games---A Guide to Current Research, E. Grädel, W. Thomas, and T. Wilke, Eds. LNCS 2500. Springer, Heidelberg, 153--167. Google Scholar
- Kröger, F. 1977. Lar: a logic of algorithmic reasoning. Acta Informatica 8, 243--266.Google ScholarDigital Library
- Kumar, R. and Garg, V. 1995. Modeling and Control of Logical Discrete Event Systems. Kluwer Academic Publishers, Dordrecht.Google Scholar
- Lassez, J.-L., Nguyen, V., and Sonenberg, E. 1982. Fixed point theorems and semantics: A folk tale. Information Processing Letters 14, 3 (May), 112--116.Google ScholarCross Ref
- Long, D., Browne, A., Clarke, E., Jha, S., and Marrero, W. 1994. An improved algorithm for the evaluation of fixpoint expressions. In Conference on Computer Aided Verification (CAV), D. Dill, Ed. LNCS, Vol. 818. Springer, Stanford, CA, USA, 338--350. Google Scholar
- Niwiński, D. 1986. On fixed point clones. In International Colloquium on Automata, Languages and Programming (ICALP), L. Kott, Ed. LNCS of Vol 226, Springer-Verlag, Berlin, 464--473. Google Scholar
- Pnueli, A. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science. IEEE, Providence, RI, 46--57.Google Scholar
- Ramadge, P. J. and Wonham, W. M. 1987. Supervisory control of a class of discrete event processes. SIAM Journal of Control and Optimization 25, 1, 206--230. Google ScholarDigital Library
- Ramadge, P. J. and Wonham, W. M. 1989. The control of discrete event systems. Proceedings of the IEEE 77, 1, 81--98.Google ScholarCross Ref
- Safra, S. 1988. On the complexity of ω-automata. In Symposium on Foundations of Computer Science (FOCS), 319--327.Google Scholar
- Schneider, K. 2003. Verification of Reactive Systems---Formal Methods and Algorithms, Texts in Theoretical Computer Science (EATCS Series). Springer, Berlin. Google Scholar
- Seidl, H. 1996. Fast and simple nested fixpoints. Information Processing Letters 59, 6, 303--308. Google ScholarDigital Library
- Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 2, 285--309.Google ScholarCross Ref
- Thistle, J. G. and Wonham, W. M. 1994a. Control of infinite behavior of finite automata. SIAM Journal of Control and Optimization 32, 4, 1075--1097. Google ScholarDigital Library
- Thistle, J. G. and Wonham, W. M. 1994b. Supervision of infinite behavior of discrete--event systems. SIAM Journal of Control and Optimization 32, 4, 1098--1113. Google ScholarDigital Library
- Wilke, T. 2001. Alternating Tree Automata, Parity Games, and Modal μ-Calculus. Bull. Soc. Math. Belg. 8, 2 (May).Google Scholar
- Wonham, W. M. 2004. Supervisory control of discrete-event systems. Tech. rep., Dept. of Electrical and Computer Engineering, University of Toronto. ECE 1636F/1637S 2004-05, http://www.control.utoronto.ca/DES.Google Scholar
- Wonham, W. M. and Ramadge, P. 1987. On the supremal controllable sulanguange of a given language. SIAM J. Control and Optimization 25, 3 (May), 637--659. Google ScholarDigital Library
- Ziller, R. and Schneider, K. 2003. A μ-calculus approach to supervisor synthesis. In GI/ITG/ GMM---Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. 132--143.Google Scholar
Index Terms
- Combining supervisor synthesis and model checking
Recommendations
Model-Checking and Game theory for Synthesis of Safety Rules
HASE '15: Proceedings of the 2015 IEEE 16th International Symposium on High Assurance Systems EngineeringEnsuring that safety requirements are respected is a critical issue for the deployment of hazardous and complex reactive systems. We consider a separate safety channel, called a monitor, that is able to partially observe the system and to trigger safety-...
Modeling for supervisor synthesis – a lock-bridge combination case study
AbstractDesigning supervisory controllers for high-tech systems is becoming increasingly complex due to demands for verified safety, higher quality and availability, and extending functionality. Supervisor synthesis is a method to automatically derive a ...
Transformational supervisor synthesis for evolving systems
AbstractSupervisory controller synthesis is a means to compute correct-by-construction controllers for discrete event systems. As these systems and their requirements evolve over time, an updated supervisor needs to be computed each time an adaptation ...
Comments