IEEE/CAA Journal of Automatica Sinica
Citation:  Samik Basu and Ratnesh Kumar, "Control of NonDeterministic Systems With μCalculus Specifications Using Quotienting," IEEE/CAA J. Autom. Sinica, vol. 8, no. 5, pp. 953970, May 2021. doi: 10.1109/JAS.2021.1003964 
[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/S03043975(02)004425

[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/s106260069327x

[6] 
S. Basu and R. Kumar, “Quotientbased control synthesis for nondeterministic 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, “Quotientbased control synthesis for partially observed nondeterministic 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 mucalculus,” 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: SpringerVerlag, 1994, pp. 59–65.

[20] 
M. Heymann and F. Lin, “Discreteevent 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 discreteevent 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: SpringerVerlag, 1994, pp. 39–48.

[24] 
M. A. Shayman and R. Kumar, “Process objects/masked composition: An objectoriented approach for modeling and control of discreteevent 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 discreteevent 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 controlD 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: SpringerVerlag, 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: SpringerVerlag, 1999, pp. 382–398.

[31] 
S. Riedweg and S. Pinchinat, “Quantified mucalculus 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 discreteevent 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: SpringerVerlag, 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/S03043975(00)003078

[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 discreteevent 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,” IFACPapersOnLine, 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, “BDDbased synthesis of failsafe supervisory controllers for safetycritical 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/03043975(82)901256

[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/S03043975(00)000347

[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 latticetheoretical 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, “Modelchecking 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.
