
IEEE/CAA Journal of Automatica Sinica
Citation: | Chuanliang Xia, Chengdong Li, "Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems," IEEE/CAA J. Autom. Sinica, vol. 8, no. 4, pp. 905-915, Apr. 2021. doi: 10.1109/JAS.2020.1003003 |
EMBEDDED systems are ubiquitous in almost all devices used today, including mobile telephones, network switches, household appliances, and controllers of the internet of things (IoT). Such systems are an important part of large complex networks and often include both software and hardware elements. Real-time behavior, correctness, and good reliability are vital requirements for successful embedded systems [1]. Many models have been proposed to describe such systems, including finite state machines, data flow graphs, and Petri nets.
Petri nets constitute a high-performing model, widely used in many fields of science. The model can be used to express concurrency, synchronization, sequential actions, and non-determinism when designing certain systems. Petri-net-based representation for embedded systems (PRES+) have been proposed for the design and verification of embedded systems [2]. Using PRES+ supports allows for a precise representation of embedded systems, improves expressiveness, and captures timing information.
The PRES+ model is important for the modeling, analysis, and verification of embedded systems [2]–[8]. In order to design and verify these systems, Cortés et al. [2] presented a formal computational model based on PRES+. An industrial example was also provided to illustrate the efficiency of the PRES+ method. To improve its verification efficiency, a translation algorithm from the PRES+ model to a finite state machine with the datapath model was proposed [3]. For systems specified in PRES+, Karlsson et al. [5] put forward a method to integrate them with component-based system level design. The model utilized was a mobile telephone system, consisting of seven connected components, which were modeled in PRES+. The properties of reachability and timing were then verified. Xia [6] proposed several reduction rules to improve the verification efficiency of PRES+. Under some constraints, the properties of reachability, functionality, and timing were preserved.
However, the state space explosion problem for PRES+ struggles to specify and analyze large, complex embedded systems. This problem is of exponential complexity and decreases the modeling and verification abilities of PRES+.
The state space explosion problem is due to the absence of abstraction and compositionality mechanisms. Many researchers have used transformation approaches to resolve the state space explosion problem for Petri nets. It is essential to neither destroy nor create properties under investigation when establishing transformations. Three popular transformations exist among the literature, namely reduction [6], [9]–[16], refinement [7], [17]–[22], and synthesis [23]–[36].
Petri-net-based synthesis is an effective approach to system design and verification. The synthesis method can create a system from several component modules in such a way that the system can be effectively analyzed for design correctness. A review of some approaches in the synthesis of Petri nets is provided below.
A Petri-net-based synthesis methodology to resolve the use-case driven system design problem was proposed in [23]. Zhou et al. [24] presented a hybrid synthesis approach for manufacturing systems by using parallel and sequential mutual exclusions. For distributed liveness-enforcing supervisors of automated manufacturing systems, Hu et al. [25] focused on a synthesis method that allows both multiple resource acquisition operations and flexible process routes. Best et al. [26] characterized the reachability graph of a Petri net marked graph. This work described procedures to synthesize a marked graph solving a labeled transition system benefiting from characterizing properties. Pouyan et al. [27] classified synthesis methods into the following groups: top-down techniques, hybrid approaches, knitting techniques, and bottom-up techniques. For systems of simple sequential processes with resources (
To solve the PRES+ state space explosion problem, as well as model, analyze, and verify large and complex embedded systems, two kinds of synthesis approaches are investigated in this paper. Compared with some synthesis methods for ordinary Petri nets [23], [29], time Petri nets, and colored nets, these approaches effectively represent important characteristics of embedded systems such as reachability, functionality, and timing. In [7], an approach for expanding the PRES+ model to the desired level of detail was provided, and a transition refinement method was proposed. Reachability, timing, functionality, liveness and boundedness preservation of the refined PRES+ model have also been investigated. To improve the verification efficiency of PRES+, Xia [6] presented a set of reduction rules. Under certain constraints, the reduced PRES+ model preserves reachability, timing, and functionality. A sharing synthesis operation for PRES+ and its liveness and boundedness preservation have been investigated in [8].
The principal motivation of this paper is to solve the synchronous problem in embedded systems, and the embedded subsystem sharing problem. The subsystem-sharing problem is formulated as a problem of merging several sets of subsystems into transition sets. Some constraints for ensuring that these synthesis methods preserve reachability, timing, functionality, and liveness are obtained in this work. The results are then applied to the verification of the modeling problem of embedded systems. First, a synthesis shared transition set for PRES+ is presented, and the property preservation of the method is investigated. Following this, the synthesis shared-transition-set technique of PRES+ is used to investigate the synthesis shared-transition-subnet-set technique by adopting the abstraction-synthesis-refinement representation method. Results obtained are useful for investigating the properties of PRES+ synthesis nets, and establishing models for large and complex embedded systems.
The remainder of this paper is organized as follows. Some preliminaries of PRES+ are proposed in Section II. The synthesis shared-transition-set approach and the synthesis shared-transition-subnet-set approach of PRES+ are presented in Section III. The abstraction-synthesis-refinement representation method is proposed in Section IV, and the preservation of reachability, timing, and functionality is investigated in Section V. Liveness preservation by these two synthesis approaches is discussed in Section VI. A case example is proposed in Section VII to illustrate the effectiveness of the proposed synthesis methods. Finally, conclusions are presented in Section VIII.
In this section, the fundamentals of PRES+ are provided as a foundation for the rest of this article. A more general discussion on PRES+ can be found in [2].
Definition 1: A PRES+ model is
Fig. 1 shows an example of the definitions of the PRES+ model presented in this section. For the example, we have
Definition 2: A marking is an assignment of tokens to places. The marking
For example, the initial marking
Definition 3: The pre-set
Definition 4: For every transition
In Fig. 1, for example, there exists a transition function
Definition 5: For every transition
For instance, in Fig. 1, the minimum transition delay of
Definition 6: A transition
The guard of transition
Definition 7: For an enabled transition
A PRES+ model is a restricted version of the CPN model. For successor marking definition, a more formal way is proposed in [36]. In this restricted CPN model, a marking
Definition 8 [36]: A marking
Note that, for verification purposes, the PRES+ nets can be restricted to safe PRES+ nets [2], that is, every place
In this section, the synthesis shared transition set operation and the synthesis shared transition subnet set operation for the PRES+ model are proposed.
Definition 9: A PRES+ model
Definition 10: Suppose
Definition 11: Let
Definition 12: Let
Definition 13: Let
From the above, it is clear that
Definition 14: A PRES+ model
Definition 15: For the transition set
Supposition 1: Suppose
1) In a procedure (tokens from outside flow into
2)
3) Before
In this section, we present the shared transition subnet set synthesis operation. Fig. 2 shows a schematic diagram of synthesis operation.
Definition 16: Let
In Fig. 2, the PRES+ model
Supposition 2: Suppose
1)
2) Let
3) Let
For example, in Fig. 2,
Definition 17 (Synthesis Operation):
For instance, in Fig. 2,
Supposition 3: It is assumed that
Note that, in Fig. 2, for convenience, the transition function and transition delay were omitted. For example, in Fig. 2, let
Supposition 4: Assume
For example, in Fig. 2, let
In this section we will present an abstraction-synthesis-refinement representation method and propose the transition subnet refinement operation and the transition subnet abstraction operation.
Since it is difficult to operate directly on the synthesis of shared transition subnets, we adopt the solution from an abstraction operation and a synthesis operation to a refinement operation. This solution is useful in proving certain theorems in Sections V and VI.
Fig. 3 illustrates a synthesis of shared transition subnet solution.
In Fig. 3,
In this section, definitions of the transition subnet refinement operation and the transition subnet abstraction operation are proposed.
Definition 18 (Transition Subnet Refinement Operation) [7]: the refined net
i)
ii)
iii)
iv)
v)
vi)
vii)
Note that, in the following, the process of the transition subnet abstraction operation (Definition 19) is the inverse of the process of the transition subnet refinement operation (Definition 18).
Definition 19 (Transition Subnet Abstraction Operation): here
i)
ii)
iii)
iv)
v)
vi)
Note that
In this section, some fundamentals of two PRES+ models with the same reachability, timing, and functionality are initially reviewed [7]. Reachability, timing, and functionality preservations of these two synthesis PRES+ models are then discussed.
Two PRES+ subnets
If
In this section, we investigate the shared transition set synthesis PRES+ model’s preservation of reachability, functionality, and timing.
Theorem 1: Suppose that
Proof: Assume that
The input places and output places of
By the concept of shared transition set synthesis, the tokens’ type in the input places of
By the shared transition set synthesis operation, the tokens’ time in the input places of
Let
In this section, we will use the abstraction-synthesis-refinement representation method to investigate the preservation of reachability, functionality, and timing of the shared transition subnet set synthesis PRES+ model. In this synthesis process, Lemmas 1 and 2 play an important role.
Lemma 1: Let
Proof: Let subnet
Let subnet
By Definition 19, the type of tokens in the input place of
By Definition 19, the token time of tokens in the input place of
As
Lemma 2 [7]: Let
The abstraction-synthesis-refinement representation method is used in the following proof for Theorem 2. First, the original PRES+ models
Theorem 2: Let
Proof: Let
The shared transition set synthesis PRES+ model
In this section, several fundamentals of the state, liveness, and boundedness of the PRES+ model are reviewed [7], and the liveness preservation of these synthesis approaches for PRES+ model is investigated.
The pair
J0(t)={0M0(p)≥W(p,t)∀p∈∙t#otherwise |
is the initial state of
To investigate the preservation of liveness of these two synthesis approaches, the concept of a PRES+ closed net must be presented.
A net
Suppose
Let
In this section, we investigate the liveness preservation of the shared transition set synthesis PRES+ model.
Theorem 3: Let PRES+ net system
Proof: (If) For every transition
(Only if) Since
Theorem 4: Let the PRES+ net systems
Proof: It is assumed here that
In this section, we will use the abstraction-synthesis-refinement representation method to investigate the liveness preservation of the shared transition subnet set synthesis PRES+ model. Lemmas 3 and 4, Theorems 3 and 4 ensure the correctness of the proofs of Theorems 5 and 6.
Lemma 3 [7]: Let the PRES+ net system
Lemma 4: Let the PRES+ net system
Note that the proof process of Lemma 4 is the inverse of the proof process of Lemma 3.
Theorem 5: Here it is assumed that
Proof: Consider
Note that the same procedure can be easily adapted by using Lemmas 3 and 4 and Theorem 4 to obtain the following results.
Theorem 6: Suppose
To demonstrate the effectiveness of our synthesis methods for PRES+, we will use these two methods to model and analyze an embedded subsystem based on PRES+.
Xia [7] constructed a model of the temperature measure and control system of a fire protection system (FPS) in an intelligent building by using the transition refinement operation for PRES+.
In this section, we construct a model of two control embedded systems that share the temperature measure and control subsystems in the FPS. This subsystem can measure or display temperature, and deliver signals to other subsystems.
A model of two control systems sharing two transitions and a transition subnet in the embedded system design is built, then the property preservations of these synthesis methods are verified.
In this section, the PRES+ model for an embedded control system is constructed. The PRES+ models of two embedded control systems are first presented. The synthesized PRES+ model is then provided by using the synthesis shared transition set method and the synthesis shared transition subnet set method. The abstraction-synthesis-refinement operation representation method is used to carry out the synthesis approach.
In this paper, we will adopt the synthesis operation to model and analyze this system. The PRES+ models of the two control subsystems are illustrated in Figs. 4 and 5 (adapted from [7]).
In Fig. 4 (Fig. 5),
In the transition subnet
The PRES+ models
In this section, the reachability, functionality, timing, and liveness preservations of the synthesis PRES+ model are analyzed.
1) Reachability, Functionality, and Timing Preservation: Let
Here, NT1 = (PT1, TT1, IT1, OT1, MT10) , where PT1 = {p11, p12, p13, p14, p15, p16}; TT1 = {t11, t12, t13, t14, t15, t16, t17, t18, t19}; IT1 = {(p11, t12), (p11, t13), (p12, t14), (p13, t15), (p14, t16), (p14, t17), (p15, t18), (p16, t19)}; OT1 = {(t11, p11), (t11, p14), (t12, p12), (t13, p13), (t14, p11), (t14, p14), (t15, p14), (t15, p11), (t16, p16), (t17, p15), (t18, p16)}; MT10 =
Then,
Let
Next,
In accordance with Lemma 1, the reachability, functionality and timing of
Here, in the shared transition set synthesis process,
As such
As the transition function
The same method can be used to discuss the reachability, functionality, and timing preservation of
By Theorem 1, the reachability, functionality, and timing of
Let
2) Liveness Preservation: Suppose that
Embedded systems have many applications in everyday life. Petri-net-based representation for embedded systems (PRES+) is an excellent tool to model and verify embedded systems. However, the state space explosion is a serious problem for using PRES+ to model and analyze large complex embedded systems. The Petri net synthesis method can avoid the state space explosion problem, and in this paper, the preservation of properties of the synthesized PRES+ model was investigated to help solve this problem. The synthesis shared transition set approach and the synthesis shared transition subnet set approach of the PRES+ method were proposed. Under several additional conditions, reachability, functionality, timing, and liveness were preserved after merging some transitions or transition subnets of PRES+ models. The results of this paper can be successfully applied to solve design problems in embedded control systems of intelligent buildings and manufacturing engineering.
Further research is required to investigate other more general synthesis operations for PRES+ and their applications.
[1] |
M. Ashjaei, N. Khalilzad, and S. Mubeen, “Modeling, designing and analyzing resource reservations in distributed embedded systems,” RealTime Modelling and Processing for Communication Systems. Springer, 2018, pp. 203–256.
|
[2] |
L. A. Cortés, P. Eles, and Z. Peng, “Modeling and formal verification of embedded systems based on a Petri net representation,” J. Systems Architecture, vol. 49, no. 12, pp. 571–598, 2003.
|
[3] |
S. Bandyopadhyay, K. Banerjee, D. Sarkar, and C. R. Mandal, “Translation validation for PRES+ models of parallel behaviours via an FSMD equivalence checker,” Progress in VLSI Design and Test. Springer, 2012, pp. 69–78.
|
[4] |
D. Karlsson, P. Eles, and Z. Peng, “Model validation for embedded systems using formal method-aided simulation,” IET Computers &Digital Techniques, vol. 2, no. 6, pp. 413–433, 2008.
|
[5] |
D. Karlsson, P. Eles, and Z. Peng, “Formal verification of componentbased designs,” Design Automation for Embedded Systems, vol. 11, no. 1, pp. 49–90, 2007. doi: 10.1007/s10617-006-9723-3
|
[6] |
C. Xia, “Reduction rules for Petri net based representation for embedded systems,” J. Front. Comput. Sci. Technol, vol. 2, no. 6, pp. 614–626, 2008.
|
[7] |
C. Xia, “Property preservation of refinement for Petri net based representation for embedded systems,” Cluster Computing, vol. 19, no. 3, pp. 1373–1384, 2016. doi: 10.1007/s10586-016-0597-2
|
[8] |
C. Xia, B. Shen, H. Zhang, and Y. Wang, “Liveness and boundedness preservations of sharing synthesis of Petri net based representation for embedded systems,” Computer Systems Science and Engineering, vol. 33, no. 5, pp. 345–350, 2018.
|
[9] |
J. Wang, Y. Deng, and M. Zhou, “Compositional time Petri nets and reduction rules,” IEEE Trans. Systems,Man,and Cybernetics,Part B, vol. 30, no. 4, pp. 562–572, 2000. doi: 10.1109/3477.865173
|
[10] |
S. A. Shah, E. L. Bohez, K. Shah, I. ul Haq, K. Azam, and S. Anwar, “Colored Petri net model for significant reduction of invariants in flexible manufacturing systems,” Int. J. Advanced Manufacturing Technology, vol. 88, no. 5–8, pp. 1775–1787, 2017. doi: 10.1007/s00170-016-8864-1
|
[11] |
P.-A. Bourdil, B. Berthomieu, S. Dal Zilio, and F. Vernadat, “Symmetry reduction for time Petri net state classes,” Science of Computer Programming, vol. 132, pp. 209–225, 2016. doi: 10.1016/j.scico.2016.08.008
|
[12] |
J. Esparza, P. Hoffmann, and R. Saha, “Polynomial analysis algorithms for free choice probabilistic workflow nets,” Performance Evaluation, vol. 117, pp. 104–129, 2017. doi: 10.1016/j.peva.2017.09.006
|
[13] |
B. Berthomieu, D. L. Botlan, and S. D. Zilio, “Petri net reductions for counting markings,” in Int. Symp. Model Checking Software, 2018.
|
[14] |
S. M. Shatz, S. Tu, T. Murata, and S. Duri, “An application of Petri net reduction for ADA tasking deadlock analysis,” IEEE Trans. Parallel and Distributed Systems, vol. 7, no. 12, pp. 1307–1322, 1996. doi: 10.1109/71.553301
|
[15] |
Y. Chen, Z. Li, K. Barkaoui, and M. Uzam, “New Petri net structure and its application to optimal supervisory control: interval inhibitor arcs,” IEEE Trans. Systems,Man,and Cybernetics:Systems, vol. 44, no. 10, pp. 1384–1400, 2014. doi: 10.1109/TSMC.2014.2307284
|
[16] |
L. Salum, “Avoiding state explosion in a class of Petri nets,” Expert Systems with Applications, vol. 42, no. 1, pp. 519–526, 2015. doi: 10.1016/j.eswa.2014.07.037
|
[17] |
Z. Ding, C. Jiang, M. Zhou, and Y. Zhang, “Preserving languages and properties in stepwise refinement-based synthesis of Petri nets,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 38, no. 4, pp. 791–801, 2008. doi: 10.1109/TSMCA.2008.923064
|
[18] |
L. Bernardinello, E. Mangioni, and L. Pomello, “Local state refinement and composition of elementary net systems: An approach based on morphisms,” Trans. Petri Nets and Other Models of Concurrency VIII. Springer, 2013, pp. 48–70.
|
[19] |
M. Khalgui, O. Mosbahi, Z. Li, and H.-M. Hanisch, “Reconfigurable multiagent embedded control systems: from modeling to implementation,” IEEE Trans. Computers, vol. 60, no. 4, pp. 538–551, 2010.
|
[20] |
D.-E. Gratie and C. Gratie, “Composition colored Petri nets for the refinement of reaction-based models,” Electronic Notes in Theoretical Computer Science, vol. 326, pp. 51–72, 2016. doi: 10.1016/j.entcs.2016.09.018
|
[21] |
P. Baldan, F. Bonchi, F. Gadducci, and G. V. Monreale, “Modular encoding of synchronous and asynchronous interactions using open Petri nets,” Science of Computer Programming, vol. 109, pp. 96–124, 2015. doi: 10.1016/j.scico.2014.11.019
|
[22] |
J. Li, M. Zhou, and X. Dai, “Reduction and refinement by algebraic operations for Petri net transformation,” IEEE Trans. Systems,Man,and Cybernetics-Part A:Systems and Humans, vol. 42, no. 5, pp. 1244–1255, 2012. doi: 10.1109/TSMCA.2012.2186440
|
[23] |
K. S. Cheung, T. Cheung, and K. Chow, “A Petri-net-based synthesis methodology for use-case-driven system design,” J. Systems and Software, vol. 79, no. 6, pp. 772–790, 2006. doi: 10.1016/j.jss.2005.06.018
|
[24] |
M. Zhou, F. DiCesare, and A. A. Desrochers, “A hybrid methodology for synthesis of Petri net models for manufacturing systems,” IEEE Trans. Robotics and Automation, vol. 8, no. 3, pp. 350–361, 1992. doi: 10.1109/70.143353
|
[25] |
H. Hu, R. Su, M. Zhou, and Y. Liu, “Polynomially complex synthesis of distributed supervisors for large-scale amss using Petri nets,” IEEE Trans. Control Systems Technology, vol. 24, no. 5, pp. 1610–1622, 2015.
|
[26] |
E. Best and R. Devillers, “Characterisation of the state spaces of marked graph Petri nets,” Information and Computation, vol. 253, pp. 399–410, 2017. doi: 10.1016/j.ic.2016.06.006
|
[27] |
A. A. Pouyan, H. T. Shandiz, and S. Arastehfar, “Synthesis a Petri net based control model for a FMS cell,” Computers in Industry, vol. 62, no. 5, pp. 501–508, 2011. doi: 10.1016/j.compind.2011.01.001
|
[28] |
G. Liu, Z. Li, K. Barkaoui, and A. M. Al-Ahmari, “Robustness of deadlock control for a class of Petri nets with unreliable resources,” Information Sciences, vol. 235, pp. 259–279, 2013. doi: 10.1016/j.ins.2013.01.003
|
[29] |
C. Xia, “Analysis of properties of petri synthesis net,” in Proc. Int. Conf. Theory and Applications of Models of Computation. Springer, 2006, pp. 576–587.
|
[30] |
C. Xia, “Liveness and boundedness analysis of Petri net synthesis,” Mathematical Structures in Computer Science, vol. 24, no. 5, Article No. 2014.
|
[31] |
D. Liu, Z. Li, and M. Zhou, “A parameterized liveness and ratioenforcing supervisor for a class of generalized Petri nets,” Automatica, vol. 49, no. 11, pp. 3167–3179, 2013. doi: 10.1016/j.automatica.2013.07.023
|
[32] |
L. Jiao, T.-Y. Cheung, and W. Lu, “On liveness and boundedness of asymmetric choice nets,” Theoretical Computer Science, vol. 311, no. 1–3, pp. 165–197, 2004. doi: 10.1016/S0304-3975(03)00359-1
|
[33] |
F. Basile, F. Caccavale, P. Chiacchio, J. Coppola, A. Marino, and D. Gerbasio, “Automated synthesis of hybrid Petri net models for robotic cells in the aircraft industry,” Control Engineering Practice, vol. 31, pp. 35–49, 2014. doi: 10.1016/j.conengprac.2014.05.008
|
[34] |
F. Basile, R. Cordone, and L. Piroddi, “A branch and bound approach for the design of decentralized supervisors in Petri net models,” Automatica, vol. 52, pp. 322–333, 2015. doi: 10.1016/j.automatica.2014.12.004
|
[35] |
Q. Hu, Y. Du, and S. Yu, “Service net algebra based on logic Petri nets,” Information Sciences, vol. 268, pp. 271–289, 2014. doi: 10.1016/j.ins.2013.10.014
|
[36] |
S. Bandyopadhyay, D. Sarkar, and C. Mandal, “Equivalence checking of Petri net models of programs using static and dynamic cut-points,” Acta Informatica, vol. 56, no. 4, pp. 321–383, 2019. doi: 10.1007/s00236-018-0320-2
|
[1] | Tao Qin, Li Yin, Gaiyun Liu, Naiqi Wu, Zhiwu Li. Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2025, 12(1): 54-68. doi: 10.1109/JAS.2024.124560 |
[2] | Xiaofeng Yuan, Weiwei Xu, Yalin Wang, Chunhua Yang, Weihua Gui. A Deep Residual PLS for Data-Driven Quality Prediction Modeling in Industrial Process[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(8): 1777-1785. doi: 10.1109/JAS.2024.124578 |
[3] | Wei Ren, Zhuo-Rui Pan, Weiguo Xia, Xi-Ming Sun. Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(10): 2082-2098. doi: 10.1109/JAS.2024.124473 |
[4] | Yifan Dong, Naiqi Wu, Zhiwu Li. State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11(5): 1274-1291. doi: 10.1109/JAS.2023.124128 |
[5] | Wei He, Xinxing Mu, Liang Zhang, Yao Zou. Modeling and Trajectory Tracking Control for Flapping-Wing Micro Aerial Vehicles[J]. IEEE/CAA Journal of Automatica Sinica, 2021, 8(1): 148-156. doi: 10.1109/JAS.2020.1003417 |
[6] | Fajun Yang, Naiqi Wu, Yan Qiao, Rong Su. Polynomial Approach to Optimal One-wafer Cyclic Scheduling of Treelike Hybrid Multi-Cluster Tools via Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2018, 5(1): 270-280. doi: 10.1109/JAS.2017.7510772 |
[7] | Dongming Xiang, Guanjun Liu, Chungang Yan, Changjun Jiang. Detecting Data-flow Errors Based on Petri Nets With Data Operations[J]. IEEE/CAA Journal of Automatica Sinica, 2018, 5(1): 251-260. doi: 10.1109/JAS.2017.7510766 |
[8] | Ran Ning, Su Hongye, Wang Shouguang. An Improved Approach to Test Diagnosability of Bounded Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2017, 4(2): 297-303. doi: 10.1109/JAS.2017.7510406 |
[9] | Jiacai Huang, YangQuan Chen, Haibin Li, Xinxin Shi. Fractional Order Modeling of Human Operator Behavior with Second Order Controlled Plant and Experiment Research[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 271-280. |
[10] | Yan Ma, Xiuwen Zhou, Bingsi Li, Hong Chen. Fractional Modeling and SOC Estimation of Lithium-ion Battery[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 281-287. |
[11] | Bingsan Chen, Chunyu Li, Benjamin Wilson, Yijian Huang. Fractional Modeling and Analysis of Coupled MR Damping System[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(3): 288-294. |
[12] | Xiaoyu Lu, Mengchu Zhou, Ahmed Chiheb Ammari, Jingchu Ji. Hybrid Petri Nets for Modeling and Analysis of Microgrid Systems[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(4): 349-356. |
[13] | Xian Li, Zengfu Wang. A HMM-based Mandarin Chinese Singing Voice Synthesis System[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(2): 192-202. |
[14] | Themistoklis Giitsidis, Georgios Ch. Sirakoulis. Modeling Passengers Boarding in Aircraft Using Cellular Automata[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 3(4): 365-384. |
[15] | Kecai Cao, YangQuan Chen, Dan Stuart, Dong Yue. Cyber-physical Modeling and Control of Crowd of Pedestrians: A Review and New Framework[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(3): 334-344. |
[16] | Hong Mo, Jie Wang, Xuan Li, Zhanlin Wu. Linguistic Dynamic Modeling and Analysis of Psychological Health State Using Interval Type-2 Fuzzy Sets[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 366-373. |
[17] | Naizhou Wang, Hailong Pei, Yong Tang. Anti-windup-based Dynamic Controller Synthesis for Lipschitz Systems under Actuator Saturation[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 358-365. |
[18] | Shouguang Wang, Mengdi Gan, Mengchu Zhou, Dan You. A Reduced Reachability Tree for a Class of Unbounded Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(4): 345-352. |
[19] | Tianmu Ma, Xiaochuan Luo, Tianyou Chai. Modeling and Hybrid Optimization of Batching Planning System for Steelmaking-continuous Casting Process[J]. IEEE/CAA Journal of Automatica Sinica, 2014, 1(2): 113-126. |
[20] | Manoj Kumar, Karthikeyan Rajagopal, Sivasubramanya Nadar Balakrishnan, Nhan T. Nguyen. Reinforcement Learning Based Controller Synthesis for Flexible Aircraft Wings[J]. IEEE/CAA Journal of Automatica Sinica, 2014, 1(4): 435-448. |