Control of Non-Deterministic Systems With <i>μ</i>-Calculus Specifications Using Quotienting

Samik Basu; Ratnesh Kumar

doi:10.1109/JAS.2021.1003964

Volume 8 Issue 5

May 2021

IEEE/CAA Journal of Automatica Sinica

JCR Impact Factor: 15.3, Top 1 (SCI Q1)

CiteScore: 23.5, Top 2% (Q1)
Google Scholar h5-index: 77， TOP 5

Turn off MathJax

Article Contents

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2021 > 8(5): 953-970

S. Basu, R. Kumar, "Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting," IEEE/CAA J. Autom. Sinica, vol. 8, no. 5, pp. 953-970, May. 2021. doi: 10.1109/JAS.2021.1003964

Citation:

S. Basu, R. Kumar, "Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting," IEEE/CAA J. Autom. Sinica, vol. 8, no. 5, pp. 953-970, May. 2021. doi: 10.1109/JAS.2021.1003964

Citation:

PDF( 2123 KB)

Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting

doi: 10.1109/JAS.2021.1003964

Samik Basu^1
,,
Ratnesh Kumar^{2
,
,}

1.
Department of Computer Science, Iowa State University, Iowa 50011-3060 USA
2.
Department of Electrical and Computer Engineering, Iowa State University, Iowa 50011-3060 USA

Funds: The work was supported in part by the National Science Foundation (NSF-ECCS-1509420, NSF-CSSI-2004766)

More Information

Author Bio:
Samik Basu is Professor in the Department of Computer Science at Iowa State University, USA. His research interests include formal methods, software verification, social network analysis, preference reasoning and security. He received the B.E. in computer science and engineering from Jadavpur University, India, in 1998, and the M.S. and Ph.D. degrees in computer science from Stony Brook University in 2001 and 2003, respectively

Ratnesh Kumar (F’07) is a Harpole Professor at the Department of Electrical and Computer Engineering at Iowa State University, where he directs the ESSeNCE (Embedded Software, Sensors, Networks, Cyberphysical, and Energy) Lab. Previously, he held faulty position at the University of Kentucky, and various visiting positions with the University of Maryland (College Park), the Applied Research Laboratory at the Pennsylvania State University (State College), the NASA Ames, the Idaho National Laboratory, the United Technologies Research Center, and the Air Force Research Laboratory. He received the B.Tech. degree in electrical engineering from IIT, India, in 1987, and the M.S. and Ph.D. degrees in electrical and computer engineering from The University of Texas at Austin in 1989 and 1991, respectively. He was a recipient of the Gold Medals for the Best EE Undergrad, the Best EE Project, and the Best All Rounder from IIT Kanpur, the Best Dissertation Award from UT Austin, the Best Paper Award from the IEEE Transactions on Automation Science and Engineering, and Keynote Speaker and paper awards recipient from multiple conferences. He is or has been an Editor of several journals (including of IEEE, SIAM, ACM, Springer, IET, MDPI), was a Distinguished Lecturer of the IEEE Control Systems Society, is a recipient of D. R. Boylan Eminent Faculty Award for Research from Iowa State University, a Fellow of IEEE, and also a Fellow of AAAS
Corresponding author: Ratnesh Kumar, e-mail: rkumar@iastate.edu
Received Date: 2020-09-23
Revised Date: 2020-12-10
Accepted Date: 2021-01-10

Available Online: 2021-02-02

Abstract

Abstract

The supervisory control problem for discrete event system (DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES, results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional μ-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new μ-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of μ-calculus satisfiability. In contrast to the existing μ-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate μ-calculus formula to describe the controllability constraint (that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.
- Discrete event systems (DES),
- non-deterministic plant,
- μ-calculus,
- supervisory control

FullText(HTML)

References(55)

References

[1]	P. J. Ramadge and W. M. Wonham, “Supervisory control of a class of discrete event processes,” SIAM J. Control Optim., vol. 25, no. 1, pp. 206–230, Jan. 1987. doi: 10.1137/0325013
[2]	R. Kumar and V. K. Garg, Modeling and Control of Logical Discrete Event Systems. Boston, MA: Kluwer Academic Publishers, 1995.
[3]	A. Arnold, A. Vincent, and I. Walukiewicz, “Games for synthesis of controllers with partial observation,” Theor. Comput. Sci., vol. 303, no. 1, pp. 7–34, Jun. 2003. doi: 10.1016/S0304-3975(02)00442-5
[4]	A. Arnold, X. Briand, G. Point, and A. Vincent, “A generic approach to the control of discrete event systems,” in Proc. 44th IEEE Conf. Decision and Control, Seville, Spain, 2005, pp. 1–5.
[5]	X. Briand, “Dynamic control with indistinguishable events,” Discrete Event Dyn. Syst., vol. 16, no. 3, pp. 353–384, Sept. 2006. doi: 10.1007/s10626-006-9327-x
[6]	S. Basu and R. Kumar, “Quotient-based control synthesis for non-deterministic plants with μ-calculus specifications,” in Proc. 45th IEEE Conf. Decision and Control, San Diego, CA, USA, 2006, pp. 6041–6046.
[7]	A. Arnold and I. Walukiewicz, “Nondeterministic controllers of nondeterministic processes,” Logic and Automata, vol. 2, pp. 29–52, 2008.
[8]	S. Basu and R. Kumar, “Quotient-based control synthesis for partially observed non-deterministic plants with μ-calculus specifications,” in Proc. 46th IEEE Conf. Decision and Control, New Orleans, LA, USA, 2007, 5294–5299.
[9]	S. Riedweg and S. Pinchinat, “Quantified μ-calculus for control synthesis,” in Mathematical Foundations of Computer Science. Berlin, Heidelberg: Springer, 2003, pp. 642–651.
[10]	S. Pinchinat and S. Riedweg, “A decidable class of problems for control under partial observation,” Inform. Process. Lett., vol. 95, no. 4, pp. 454–460, Aug. 2005. doi: 10.1016/j.ipl.2005.04.011
[11]	H. R. Andersen, “Partial model checking,” in Logic in Computer Science, 1995.
[12]	S. Basu and C. R. Ramakrishnan, “Compositional analysis for verification of parameterized systems,” Theor. Comput. Sci., vol. 354, no. 2, pp. 211–229, Mar. 2006. doi: 10.1016/j.tcs.2005.11.016
[13]	E. A. Emerson and C. S. Jutla, “The complexity of tree automata and logics of programs,” SIAM J. Comput., vol. 29, no. 1, pp. 132–158, Sept. 1999. doi: 10.1137/S0097539793304741
[14]	C. Stirling, “Games and modal mu-calculus,” in Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 1996, pp. 298–312.
[15]	J. Zappe, “Modal μ-calculus and alternating tree automata,” in Automata Logics, and Infinite Games. Berlin, Heidelberg: Springer, 2002, pp. 171–184.
[16]	M. A. Shayman and R. Kumar, “Supervisory control of nondeterministic systems with driven events via prioritized synchronization and trajectory models,” SIAM J. Control Optim., vol. 33, no. 2, pp. 469–497, Mar. 1995. doi: 10.1137/S0363012992239600
[17]	R. Kumar and M. A. Shayman, “Nonblocking supervisory control of nondeterministic systems via prioritized synchronization,” IEEE Trans. Automat. Control, vol. 41, no. 8, pp. 1160–1175, Aug. 1996. doi: 10.1109/9.533677
[18]	R. Kumar and M. A. Shayman, “Centralized and decentralized supervisory control of nondeterministic systems under partial observation,” SIAM J. Control Optim., vol. 35, no. 2, pp. 363–383, Mar. 1997. doi: 10.1137/S0363012994272903
[19]	A. Overkamp, “Supervisory control for nondeterministic systems,” in 11th Int. Conf. Analysis and Optimization of Systems Discrete Event Systems. Lecture Notes in Control and Information Sciences. Berlin, Heidelberg: Springer-Verlag, 1994, pp. 59–65.
[20]	M. Heymann and F. Lin, “Discrete-event control of nondeterministic systems,” IEEE Trans. Automat. Control, vol. 43, no. 1, pp. 3–17, Jan. 1998. doi: 10.1109/9.654883
[21]	R. Kumar and M. Heymann, “Masked prioritized synchronization for interaction and control of discrete event systems,” IEEE Trans. Automat. Control, vol. 45, no. 11, pp. 1970–1982, Nov. 2000. doi: 10.1109/9.887621
[22]	S. B. Jiang and R. Kumar, “Supervisory control of nondeterministic discrete-event systems with driven events via masked prioritized synchronization,” IEEE Trans. Automat. Control, vol. 47, no. 9, pp. 1438–1449, Sept. 2002. doi: 10.1109/TAC.2002.802768
[23]	K. Inan, “Nondeterministic supervision under partial observations,” in 11th Int. Conf. Analysis and Optimization of Systems Discrete Event Systems. Lecture Notes in Control and Information Sciences. Berlin, Heidelberg: Springer-Verlag, 1994, pp. 39–48.
[24]	M. A. Shayman and R. Kumar, “Process objects/masked composition: An object-oriented approach for modeling and control of discrete-event systems,” IEEE Trans. Automat. Control, vol. 44, no. 10, pp. 1864–1869, Oct. 1999. doi: 10.1109/9.793725
[25]	R. Kumar, S. B. Jiang, C. Y. Zhou, and W. B. Qiu, “Polynomial synthesis of supervisor for partially observed discrete-event systems by allowing nondeterminism in control,” IEEE Trans. Automat. Control, vol. 50, no. 4, pp. 463–475, Apr. 2005. doi: 10.1109/TAC.2005.844725
[26]	S. B. Jiang and R. Kumar, “Supervisory control of discrete event systems with CTL* temporal logic specifications,” SIAM J. Control Optim., vol. 44, no. 6, pp. 2079–2103, Jan. 2006. doi: 10.1137/S0363012902409982
[27]	M. Antoniotti, “Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the control-D system,” Ph.D. dissertation, Department of Computer Science, New York University, New York, NY, 1995.
[28]	O. Kupferman, M. Y. Vardi, and P. Wolper, “Module checking,” Inform. Comput., vol. 164, no. 2, pp. 322–344, Jan. 2001. doi: 10.1006/inco.2000.2893
[29]	O. Kupferman, P. Madhusudan, P. S. Thiagarajan, and M. Y. Vardi, “Open systems and reactive environments: Control and synthesis,” in CONCUR 2000 — Concurrency Theory. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer-Verlag, 2000, pp. 92–107.
[30]	O. Kupferman and M. Y. Vardi, “Robust satisfaction,” in CONCUR’99 Concurrency Theory. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer-Verlag, 1999, pp. 382–398.
[31]	S. Riedweg and S. Pinchinat, “Quantified mu-calculus for control synthesis,” in Mathematical Foundations of Computer Science. Berlin, Heidelberg: Springer, 2003, pp. 642–651.
[32]	J. J. M. M. Rutten, “Coalgebra, concurrency, and control,” in Discrete Event Systems. Boston, MA: Springer, 2000, pp. 31–38.
[33]	J. Komenda, “Computation of supremal sublanguages of supervisory control using coalgebra,” in Proc. 6th Int. Workshop on Discrete Event Systems, Zaragoza, Spain, 2002, pp. 26–33.
[34]	G. Barrett and S. Lafortune, “Using bisimulation to solve discrete event control problems,” in Proc. American Control Conf., Albuquerque, New Mexico, USA, 1997, pp. 2337–2341.
[35]	H. Marchand and S. Pinchinat, “Supervisory control problem using symbolic bisimulation techniques,” in Proc. American Control Conf., Chicago, Illinois, USA, 2000, pp. 4067–4071.
[36]	J. Komenda, “Coalgebra and supervisory control of discrete-event systems with partial observations,” in Int. Symposium, Notre Dame, 2002, pp. 12–16.
[37]	H. J. Qin and P. Lewis, “Factorization of finite state machines under observational equivalence,” in Proc. Int. Conf. Concurrency Theory. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer-Verlag, 1990, pp. 427–441.
[38]	P. Madhusudan and P. S. Thiagarajan, “Branching time controllers for discrete event systems,” Theor. Comput. Sci., vol. 274, no. 1–2, pp. 117–149, Mar. 2002. doi: 10.1016/S0304-3975(00)00307-8
[39]	P. Tabuada, “Open maps, alternating simulations and control synthesis,” in Proc. Int. Conf. Concurrency Theory. Berlin, Heidelberg: Springer, 2004, pp. 466–480.
[40]	C. Y. Zhou, R. Kumar, and S. B. Jiang, “Control of nondeterministic discrete-event systems for bisimulation equivalence,” IEEE Trans. Automat. Control, vol. 51, no. 5, pp. 754–765, May 2006. doi: 10.1109/TAC.2006.875036
[41]	C. Y. Zhou and R. Kumar, “Bisimilarity enforcement for discrete event systems using deterministic control,” IEEE Trans. Automat. Control, vol. 56, no. 12, pp. 2986–2991, Dec. 2011. doi: 10.1109/TAC.2011.2161790
[42]	R. Kumar, S. B. Jiang, and C. Y. Zhou, “Comment on “bisimilarity control of partially observed nondeterministic discrete event systems and a test algorithm” [automatica 47 (2011) 782–788],” Automatica, vol. 50, no. 1, pp. 296–297, Jan. 2014. doi: 10.1016/j.automatica.2013.09.040
[43]	S. Takai, “Synthesis of bisimilarity enforcing supervisors for nondeterministic discrete event systems,” IFAC-PapersOnLine, vol. 51, no. 7, pp. 1–6, Jan. 2018. doi: 10.1016/j.ifacol.2018.06.270
[44]	C. Y. Zhou and R. Kumar, “Bisimilarity control of partially observed deterministic systems,” IEEE Trans. Automat. Control, vol. 52, no. 9, pp. 1642–1653, Sept. 2007. doi: 10.1109/TAC.2007.904470
[45]	C. Y. Zhou and R. Kumar, “A small model theorem for bisimilarity control under partial observation,” IEEE Trans. Automat. Sci. Eng., vol. 4, no. 1, pp. 93–97, Jan. 2007. doi: 10.1109/TASE.2006.873004
[46]	C. Y. Zhou and R. Kumar, “Control of nondeterministic discrete event systems for simulation equivalence,” IEEE Trans. Automat. Sci. Eng., vol. 4, no. 3, pp. 340–349, Jul. 2007. doi: 10.1109/TASE.2006.891474
[47]	S. Takai, “Synthesis of maximally permissive supervisors for nondeterministic discrete event systems with nondeterministic specifications,” IEEE Trans. Automat. Control, 2020. DOI: 10.1109/TAC.2020.3015453
[48]	T. H. Xu, H. F. Wang, T. M. Yuan, and M. C. Zhou, “BDD-based synthesis of fail-safe supervisory controllers for safety-critical discrete event systems,” IEEE Trans. Intell. Transp. Syst., vol. 17, no. 9, pp. 2385–2394, Sept. 2016. doi: 10.1109/TITS.2016.2515063
[49]	D. Kozen, “Results on the propositional μ-calculus,” Theor. Comput. Sci., vol. 27, no. 3, pp. 333–354, Dec. 1983. doi: 10.1016/0304-3975(82)90125-6
[50]	E. A. Emerson, C. S. Jutla, and A. P. Sistla, “On model checking for the μ-calculus and its fragments,” Theor. Comput. Sci., vol. 258, no. 1–2, pp. 491–522, May 2001. doi: 10.1016/S0304-3975(00)00034-7
[51]	G. Bhat and R. Cleaveland, “Efficient model checking via the equational μ-calculus”, in Proc. 11th Annu. IEEE Symp. Logic in Computer Science, New Brunswick, NJ, USA, 1996, pp. 304–312.
[52]	A. Tarski, “A lattice-theoretical fixpoint theorem and its applications,” Pacific J. Math., vol. 5, pp. 285–309, 1955. doi: 10.2140/pjm.1955.5.285
[53]	F. Cassez and F. Laroussinie, “Model-checking for hybrid systems by quotienting and constraints solving”, in Proc. 12th Int. Conf. Computer Aided Verification, Berlin, Heidelberg, 2000, pp. 373–388.
[54]	The XSB Group. The XSB logic programming system, 2004. [Online]. Available: http://xsb.sourceforge.net
[55]	R. Milner, A Calculus of Communicating Systems. Berlin Heidelberg: Springer Verlag, 1980.

Supplements(0)

Cited By

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(11) / Tables(2)

Get Citation

PDF

XML

Article Metrics

Article views (2757) PDF downloads(47)

Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting

doi: 10.1109/JAS.2021.1003964

Abstract

References

Proportional views

Catalog

通讯作者: 陈斌, bchen63@163.com

Article Metrics

Export File

Citation

Format

Content