Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates
This paper studies the symbolic reachability relations of a class of parameterized systems in the framework of regular model checking. The modules of each system are instantiated from a globally synchronized template, and each globally synchronized template is represented by a finite state automaton...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/137871 |
| _version_ | 1811690752556662784 |
|---|---|
| author | Lin, Liyong Stefanescu, Alin Wang, Weilin Su, Rong Wonham, Walter Murray |
| author2 | School of Electrical and Electronic Engineering |
| author_facet | School of Electrical and Electronic Engineering Lin, Liyong Stefanescu, Alin Wang, Weilin Su, Rong Wonham, Walter Murray |
| author_sort | Lin, Liyong |
| collection | NTU |
| description | This paper studies the symbolic reachability relations of a class of parameterized systems in the framework of regular model checking. The modules of each system are instantiated from a globally synchronized template, and each globally synchronized template is represented by a finite state automaton whose event set consists of global events and local events. It is shown that the symbolic reachability relations of these systems are effectively iteration-closed star languages. And for any iteration-closed star language, there exists a template with only global events that realizes it. Application of the symbolic reachability analysis to computing the entrance control functions that enforce deadlock freeness and blocking freeness is then illustrated for systems with idle modules. In particular, we show that the maximally permissive entrance control functions can be encoded using finite state automata. |
| first_indexed | 2024-10-01T06:08:59Z |
| format | Journal Article |
| id | ntu-10356/137871 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T06:08:59Z |
| publishDate | 2020 |
| record_format | dspace |
| spelling | ntu-10356/1378712020-04-17T01:51:43Z Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates Lin, Liyong Stefanescu, Alin Wang, Weilin Su, Rong Wonham, Walter Murray School of Electrical and Electronic Engineering Center for System Intelligence and Efficiency Engineering::Electrical and electronic engineering Symbolic Reachability Analysis Parameterized Discrete-event Systems This paper studies the symbolic reachability relations of a class of parameterized systems in the framework of regular model checking. The modules of each system are instantiated from a globally synchronized template, and each globally synchronized template is represented by a finite state automaton whose event set consists of global events and local events. It is shown that the symbolic reachability relations of these systems are effectively iteration-closed star languages. And for any iteration-closed star language, there exists a template with only global events that realizes it. Application of the symbolic reachability analysis to computing the entrance control functions that enforce deadlock freeness and blocking freeness is then illustrated for systems with idle modules. In particular, we show that the maximally permissive entrance control functions can be encoded using finite state automata. MOE (Min. of Education, S’pore) Accepted version 2020-04-17T01:51:43Z 2020-04-17T01:51:43Z 2017 Journal Article Lin, L., Stefanescu, A., Wang, W., Su, R., & Wonham, W. M. (2018). Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates. Automatica, 87, 290-300. doi:10.1016/j.automatica.2017.10.015 0005-1098 https://hdl.handle.net/10356/137871 10.1016/j.automatica.2017.10.015 87 290 300 en Automatica © 2017 Elsevier Ltd. All rights reserved.This paper was published in Automatica and is made available with permission of Elsevier Ltd. application/pdf |
| spellingShingle | Engineering::Electrical and electronic engineering Symbolic Reachability Analysis Parameterized Discrete-event Systems Lin, Liyong Stefanescu, Alin Wang, Weilin Su, Rong Wonham, Walter Murray Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title | Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title_full | Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title_fullStr | Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title_full_unstemmed | Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title_short | Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| title_sort | symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates |
| topic | Engineering::Electrical and electronic engineering Symbolic Reachability Analysis Parameterized Discrete-event Systems |
| url | https://hdl.handle.net/10356/137871 |
| work_keys_str_mv | AT linliyong symbolicreachabilityanalysisandmaximallypermissiveentrancecontrolforgloballysynchronizedtemplates AT stefanescualin symbolicreachabilityanalysisandmaximallypermissiveentrancecontrolforgloballysynchronizedtemplates AT wangweilin symbolicreachabilityanalysisandmaximallypermissiveentrancecontrolforgloballysynchronizedtemplates AT surong symbolicreachabilityanalysisandmaximallypermissiveentrancecontrolforgloballysynchronizedtemplates AT wonhamwaltermurray symbolicreachabilityanalysisandmaximallypermissiveentrancecontrolforgloballysynchronizedtemplates |