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

doi:10.1109/JAS.2021.1003964

CORC > 自动化研究所 > 中国科学院自动化研究所 > 学术期刊 > IEEE/CAA Journal of Automatica Sinica

	Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting
	Samik Basu; Ratnesh Kumar
刊名	IEEE/CAA Journal of Automatica Sinica
	2021
卷号	8 期号:5 页码:953-970
关键词	Discrete event systems (DES) non-deterministic plant μ-calculus supervisory control
ISSN号	2329-9266
DOI	10.1109/JAS.2021.1003964
英文摘要	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.
内容类型	期刊论文
源URL	[http://ir.ia.ac.cn/handle/173211/43959]
专题	自动化研究所_学术期刊_IEEE/CAA Journal of Automatica Sinica
推荐引用方式 GB/T 7714	Samik Basu,Ratnesh Kumar. Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting[J]. IEEE/CAA Journal of Automatica Sinica,2021,8(5):953-970.
APA	Samik Basu,&Ratnesh Kumar.(2021).Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting.IEEE/CAA Journal of Automatica Sinica,8(5),953-970.
MLA	Samik Basu,et al."Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting".IEEE/CAA Journal of Automatica Sinica 8.5(2021):953-970.