臺灣博碩士論文加值系統

在各類的派屈網路上可達性分析是一個很重要的議題，它可以用來分析活性問題，
公平性問題，可控性問題以及模型檢驗問題。在派屈網路的各種不同分析技巧法方法
上，我們覺得加上正規方法是非常合適用來描述各種系統。模型檢驗是檢查系統是否滿
足行為的一種自動方法。使用模型檢驗的觀念，我們可以簡單描述許多問題並且解決這
些有趣的問題。

在這篇論文，我們先針對擴增標示圖來做探討。擴增標示圖可以被想成是標示圖的
一種延伸並使其允許資源共享的狀況。擴增標示圖可以有用的塑模及分析某一類的彈性
製造系統。就我們所知，在傳統的派屈網路的分析技巧中用來分析擴增標示圖是用虹吸
式(siphon)。在這篇論文裡面，我們利用整數線性規劃的方法來分析某一類的擴增標示
圖就是所謂的可分解的擴增標示圖。我們展示了在一個可分解的擴增標示圖的路徑中其
可達性的問題可以被看成是解整數線性規劃的一個問題。我們更進一步的把我們的方法
擴充使其可以應用到某一類的分支時間時序邏輯與線性時間時序邏輯的模型驗證上。此
外，我們展示了我們的方法可以應用到彈性製造系統上的幾個範例。

其次，我們針對各種有限溝通能力派屈網路來進行可達性之分析。對無交談派屈網
路之可達性問題複雜度的問題已知是NP的問題。在沒有同步機制之下，這樣的無交談派
屈網路能力是被受限制的。因此，很重要的問題是是否可以增加無交談派屈網路的描述
能力之下而不犧牲其分析能力。在這篇論文中，我們從可判定性及複雜度的觀點為出發
點，來研究分析幾類無交談派屈網路變體中的可達性問題。這幾類無交談談派屈網路變
體其中包括了”靜態優先”、”動態優先”、”狀態” 、”禁止器弧”以及”時間限制”
。對許多擴充式無交談派屈網路而言，可達性問題變成比較困難去分析。事實上，對狀態
擴充式無交談派屈網路中加入優先權或禁止器弧而言，可達性的問題變成是不可判定性。
對於基本無交談派屈網路的模型，如果動態優先關係被利用到變遷實施上，其可達性的問
題還是不可判定性。

Reachability analysis is key to the solutions of a variety of Petri net problems including
liveness, fairness, controllability, model checking and more. Among various analytical
techniques of Petri nets, we feel that the approach based on formal methods is most suitable
for flexible manufacturing systems. Model checking is an automatic technique for
verifying that a behavior holds for a model of a system. Using the concept of model
checking, it becomes feasible to describe and solve many interesting problems in practice.

In the thesis, we first investigate augmented marked graphs. Augmented marked
graphs (AMGs) can be thought of as extensions of marked graphs that allow resource
sharing. It has been shown that AMGs are useful for modeling and analyzing certain
types of flexible manufacturing systems. To our knowledge, the techniques developed
for analyzing AMGs are mostly based upon checking certain Petri net structures such as
siphons. This thesis exploits the integer linear programming approach for the analysis
of a subclass of AMGs called decomposable AMGs. We show that reachability between
two configurations of a decomposable AMG can be equated with solving an instance of
integer linear programming. We further extend our technique to model checking a type
of branching time temporal logics and a type of linear time temporal logics. Examples
arisen in flexible manufacturing systems are used to demonstrate the application of our
technique.

Next, we study that the reachability issue of various Petri nets with limited communication
capabilities. It is known that the reachability problem for communication-free
Petri nets is NP-complete. Lacking the synchronization mechanism, the expressive power
of communication-free Petri nets is somewhat limited. It is therefore important and interesting
to see whether the power of communication-free Petri nets can be enhanced
without sacrificing their analytical capabilities. As a first step towards this line of research,
our main concern is to investigate, from the decidability/complexity viewpoint,
the reachability problem for a number of variants of communication-free Petri nets, including
communication-free Petri nets augmented with ‘static priorities,’‘dynamic priorities,’
‘states’ ‘inhibitor arcs,’ and ‘timing constraints’. For most of the augmented
communication-free Petri nets, the reachability problem becomes undecidable for stateextended
communication-free Petri nets augmented with priority or inhibitor arcs. For the
basic model of communication-free Petri nets, the reachability problem is also undecidable
if a dynamic priority relation is imposed on transition firing.

誌謝 i
中文摘要 ii
英文摘要 iv
1 Introduction 1
1.1 Augmented Marked Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Organization of the Dissertation . . . . . . . . . . . . . . . . . . . . . . 7
2 Preliminaries 8
2.1 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Petri Net Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.1 Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.2 Liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.3 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3 Analytical Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.1 State Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.2 Net Unfoldings . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.4 Augmented Marked Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 24
3 Reachability Analysis of AMGs 29
3.1 Reachability Analysis of AMGs by Linear Inequalities . . . . . . . . . . 29
3.2 Reachability Analysis of AMGs by Net Unfoldings . . . . . . . . . . . . 39
4 Model Checking 46
4.1 Unified System of Branching Time for Petri Nets . . . . . . . . . . . . . 47
4.2 Linear Time Temporal Logic for Petri Nets . . . . . . . . . . . . . . . . 50
4.3 Model Checking Using Net Unfoldings . . . . . . . . . . . . . . . . . . 52
5 Examples in Automated Manufacturing Systems 56
6 Variants of Communication-Free Petri Nets 74
6.1 State-Extended Communication-Free Petri Nets . . . . . . . . . . . . . . 74
6.2 Priority Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . 75
6.3 Communication-Free Petri Nets with Inhibitor Arcs . . . . . . . . . . . . 76
6.4 Clocked Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . 77
6.5 Complexity and Decidability Analysis of the Reachability Problem . . . . 79
6.5.1 Priority Communication-Free Petri Nets . . . . . . . . . . . . . . 79
6.5.2 Communication-Free Petri Nets with Inhibitor Arcs . . . . . . . . 85
6.5.3 Communication-Free Clocked Petri Nets . . . . . . . . . . . . . 88
7 Conclusion 91
References 93

[1] S. Reveliotis, “A linear characterization of the petri net reachability space corresponding
to bounded-length fireable transition sequences and its implications for
the structural analysis of process-resource nets with acyclic, quasi-live and strongly
reversible process subnets,” in IEEE Conference on Decision and Control and European
Control Conference, pp. 2113– 2118, 2005.
[2] A. E. Kostin, “Reachability analysis in t-invariant-less petri nets,” IEEE Transactions
on Automatic Control, vol. 48, no. 6, pp. 1019–1024, 2003.
[3] T. Matsumoto and A. Tarek, “Finding legal firing sequences of petri nets by means
of dynamic programming included linear programming,” in Proceedings of the 35th
Conference on Decision and Control, vol. 4, pp. 4459–4466, 1996.
[4] T. Matsumoto, M. Takata, and S. Moro, “Reachability analyses in petri nets by
groebner bases,” in Proceedings of the 41st SICE Annual Conference, vol. 2,
pp. 841–846, 2002.
[5] T. Murata, “Circuit theoretic analysis and synthesis of marked graphs,” IEEE Transactions
on Circuits and Systems, vol. 24, no. 7, pp. 400–405, 1977.
[6] F. Chu and X. L. Xie, “Deadlock analysis of petri nets using siphons and mathematical
programming,” IEEE Transactions on Robotics and Automation, vol. 13,
pp. 793–804, 1997.
[7] H. J. Huang, L. Jiao, and T. Y. Cheung, “Property-preserving composition of augmented
marked graphs that share common resources,” in IEEE International Conference
on Robotics and Automation, vol. 1, pp. 1446–1451, 2003.
[8] K. S. Cheung, “New characterization for live and reversible augmented marked
graphs,” Information Processing Letters, vol. 92, pp. 239–243, 2004.
[9] Y. S. Huang, M. Jeng, X. Xie, and D. H. Chung, “Siphon-based deadlock prevention
policy for flexible manufacturing systems,” IEEE Transactions on Systems, Man,
and Cybernetics, Part A, vol. 36, no. 6, pp. 1248–1256, 2006.
[10] Z. W. Li and M. C. Zhou, “Elementary siphons of petri nets and their application
to deadlock prevention in flexible manufacturing systems,” IEEE Transactions on
Systems, Man, and Cybernetics, Part A, vol. 34, no. 1, pp. 38–51, 2004.
[11] K. L. McMillan, “Using unfoldings to avoid the state explosion problem in the verification
of asynchronous circuits,” in Computer Aided Verification: Proc. of the
Fourth International Workshop CAV’92 (G. von Bochmann and D. K. Probst, eds.),
pp. 164–177, Berlin, Heidelberg: Springer, 1993.
[12] E. M. Clarke and E. A. Emerson, “Design and synthesis of synchronization skeletons
using branching-time temporal logic,” in Logic of Programs, (London, UK), pp. 52–
71, Springer-Verlag, 1981.
[13] R. R. Howell and L. E. Rosier, “On questions of fairness and temporal logic for
conflict-free petri nets,” in Advances in Petri Nets 1988, (London, UK), pp. 200–
226, Springer-Verlag, 1988.
[14] D. T. Huynh, “Commutative grammars: the complexity of uniform word problems,”
Inf. Control, vol. 57, no. 1, pp. 21–39, 1983.
[15] R. Lipton, “The reachability problem requires exponential space,” tech. rep., Yale
University, Dept. of CS., 1976.
[16] M. Marsan and G. Chiola, “On petri nets with deterministic and exponential transition
firing times,” in Proceedings of the 7th European Workshop on Application and
Theory of Petri Nets, 1986.
[17] C. Ramchandani, “Analysis of asynchronous concurrent systems by petri nets,” tech.
rep., Massachusetts Institute of Technology, 1974.
[18] R. Gorrieri and G. Siliprandi, “Real-time system verification using p/t nets,” in CAV
’94: Proceedings of the 6th International Conference on Computer Aided Verification,
(London, UK), pp. 14–26, Springer-Verlag, 1994.
[19] B. B′erard, “Untiming timed languages,” Inf. Process. Lett., vol. 55, no. 3, pp. 129–
135, 1995.
[20] R. Alur and D. L. Dill, “A theory of timed automata,” Theoretical Computer Science,
vol. 126, pp. 183–235, 1994.
[21] J. Esparza, “Petri nets, commutative context-free grammars, and basic parallel processes,”
Fundam. Inf., vol. 31, no. 1, pp. 13–25, 1997.
[22] F. Commoner, “Deadlocks in petri nets,” tech. rep., Applied Data Research Inc.,
1972.
[23] R. R. Howell, L. E. Rosier, and H. C. Yen, “A taxonomy of fairness and temporal
logic problems for petri nets,” in MFCS ’88: Proceedings of the Mathematical Foundations
of Computer Science 1988, (London, UK), pp. 351–359, Springer-Verlag,
1988.
[24] H. C. Yen, “Integer linear programming and the analysis of some petri net problems,”
Theory Comput. Syst., vol. 32, no. 4, pp. 467–485, 1999.
[25] K. L. McMillan, “A technique of state space search based on unfolding,” Form.
Methods Syst. Des., vol. 6, no. 1, pp. 45–65, 1995.
[26] J. Esparza, S. R‥omer, and W. Vogler, “An improvement of mcmillan’s unfolding
algorithm,” Form. Methods Syst. Des., vol. 20, no. 3, pp. 285–310, 2002.
[27] A. Kondratyev, M. Kishinevsky, A. Taubin, and S. Ten, “A structural approach for
the analysis of petri nets by reduced unfoldings,” in Proceedings of the 17th International
Conference on Application and Theory of Petri Nets, (London, UK),
pp. 346–365, Springer-Verlag, 1996.
[28] K. S. Cheung and K. O. Chow, “Cycle-inclusion property of augmented marked
graphs.,” Information Processing Letters, vol. 94, no. 6, pp. 271–276, 2005.
[29] H. C. Yen, “A polynomial time algorithm to decide pairwise concurrency of transitions
for 1-bounded conflict-free petri nets,” Information Processing Letters, vol. 38,
no. 2, pp. 71–76, 1991.
[30] S. Melzer and S. Romer, “Deadlock checking using net unfoldings,” in In Proceeding
of 9th International Conference on Computer Aided Verification, pp. 352–363,
Springer-Verlag, 1997.
[31] J. Esparza, “Decidability of model checking for infinite-state concurrent systems,”
Acta Informatica, vol. 34, pp. 85–107, 1997.
[32] P. Jancar, “Decidability of a temporal logic problem for petri nets,” Theoretical Computer
Science, vol. 74, pp. 71–93, 1990.
[33] O. Burkart and J. Esparza, More infinite results. River Edge, NJ, USA: World Scientific
Publishing, 2001.
[34] M. Ben-Ari, A. Pnueli, and Z. Manna, “The temporal logic of branching time,” Acta
Informatica, vol. 20, pp. 207–226, 1983.
[35] H. C. Yen, “A unified approach for deciding the existence of certain petri net paths,”
Inf. Comput., vol. 96, no. 1, pp. 119–137, 1992.
[36] K. S. Cheung, “Modelling and analysis of manufacturing systems using augmented
marked graphs,” Information Technology And Control, vol. 35, pp. 19–26, 2006.
[37] M. Zhou and M. C. Leu, “Petri net modeling of a flexible assembly station for printed
circuit boards,” in IEEE Internationl Confreence on Robotics and Automation, vol. 3,
pp. 2530–2535, 1991.
[38] P. Janˇcar, A. Kuˇcera, and R. Mayr, “Deciding bisimulation-like equivalences with
finite-state processes,” Theor. Comput. Sci., vol. 258, no. 1-2, pp. 409–433, 2001.
[39] P. Jancar and F. Moller, “Techniques for decidability and undecidability of bisimilarity,”
in In Proceedings of CONCUR’99, LNCS 1664, pp. 30–45, Springer, 1999.
[40] F. Bause, “On the analysis of petri nets with static priorities,” Acta Inf., vol. 33, no. 7,
pp. 669–685, 1996.
[41] F. Bause, “Analysis of petri nets with a dynamic priority method,” in ICATPN ’97:
Proceedings of the 18th International Conference on Application and Theory of Petri
Nets, (London, UK), pp. 215–234, Springer-Verlag, 1997.
[42] H. C. Yen, “On reachability equivalence for bpp-nets,” Theor. Comput. Sci., vol. 179,
no. 1-2, pp. 301–317, 1997.
[43] H. C. Yen, “Priority conflict-free petri nets,” Acta Inf., vol. 35, no. 8, pp. 673–688,
1998.
[44] E. W. Mayr, “An algorithm for the general petri net reachability problem,” SIAM J.
Comput., vol. 13, no. 3, pp. 441–460, 1984.