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

doi:10.1109/JAS.2021.1003964

CASIA OpenIR > 学术期刊 > 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
ISSN	2329-9266
	2021
卷号	8 期号:5 页码:953-970
摘要	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
DOI	10.1109/JAS.2021.1003964
引用统计	被引频次：3[WOS] [WOS记录] [WOS相关记录]
文献类型	期刊论文
条目标识符	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.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
JAS-2020-0936.pdf（2222KB）	期刊论文	出版稿	开放获取	CC BY-NC-SA	浏览