A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Volume 8 Issue 5
May  2021

IEEE/CAA Journal of Automatica Sinica

  • JCR Impact Factor: 11.8, Top 4% (SCI Q1)
    CiteScore: 17.6, Top 3% (Q1)
    Google Scholar h5-index: 77, TOP 5
Turn off MathJax
Article Contents
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

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

doi: 10.1109/JAS.2021.1003964
Funds:  The work was supported in part by the National Science Foundation (NSF-ECCS-1509420, NSF-CSSI-2004766)
More Information
  • 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.

     

  • loading
  • [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.

Catalog

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

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

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(11)  / Tables(2)

    Article Metrics

    Article views (2712) PDF downloads(46) Cited by()

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return