| Title | Efficient Deadlock Detection in FMS based on the Transitive Matrix of Resource Share Places |
| Author | Jongwoog Kim, *Jongkun Lee (Changwon National University, Republic of Korea) |
| Page | pp. 277 - 280 |
| Keyword | deadlock, FMS, Petri net, resource share place, transitive matrix |
| Abstract | Since a deadlock is a condition in which the excessive demand for the resources being used by others causes activities to stop, it is very important to detect and prevent deadlocks. This paper proposes a new and more efficient deadlock detection algorithm based on the transitive matrix of resource share places. For presenting the results, the suggested deadlock detection and avoidance algorithms were also adapted to an illustrated model. |
| Title | Modeling of Quantum Computer by using Quantum Petri Net |
| Author | *Shinsuke Ito, Atsushi Ohta, Kohkichi Tsuji (Aichi Prefectural University, Japan) |
| Page | pp. 281 - 284 |
| Keyword | Petri Net, Quantum Petri Net, quantum computer, modeling, quantum Turing machine |
| Abstract | Petri Net that is an effective tool for concurrent systems, has been extended to Quantum Petri Net. The conventional modeling method of quantum computer using Quantum Petri Net, have several drawbacks. This paper defines new model and examines conditions to solve drawbacks, and proposes new model from modeling quantum Turing machine, and shows that the model can simulate more general calculation processes than which the conventional model. |
| Title | A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets |
| Author | Shingo Yamaguchi, *Munenori Yamaguchi, Minoru Tanaka (Yamaguchi University, Japan) |
| Page | pp. 285 - 288 |
| Keyword | workflow net, soundness, SPIN, Woflan, verification |
| Abstract | In this paper, we propose a tool to verify soundness of acyclic WF-nets using SPIN. We first give a method to describe a given WF-net system in the modeling language of SPIN. Next we give a method to express the conditions of soundness property as Linear Temporal Logic formulas. Finally we show efficiency of our method by comparing it with Woflan on verification time for acyclic asymmetric choice WF-nets. |
| Title | A Model of Multiprocessor System with Communication Delays and Its Scheduling Method |
| Author | *Takashi Otsuka (Yamaguchi University, Japan), Hironori Youhata (Fujitsu TEN Limited, Japan), Qi-Wei Ge, Mitsuru Nakata (Yamaguchi University, Japan), Yuu Moriyama, Hirotoshi Tonou (Fujitsu TEN Limited, Japan) |
| Page | pp. 289 - 292 |
| Keyword | multiprocessor scheduling, communication time, approximate modified critical path, approximate modified critical net |
| Abstract | This paper aims at developing a scheduling method for multiprocessor systems with communication time. In this paper, we firstly propose a model of multiprocessor system with communication time occurring in reading data. Then, for the proposed model, we propose a scheduling method (called AMCN scheduling method) that (i) divides a task graph to subgraphs so that a task (called node hereafter) and its successors and predecessors are as much as possible included in the same subgraph to shorten communication time; and (ii) uses a fixed processor to execute all the nodes of a subgraph. Finally, we do computational simulation experiments to evaluate our scheduling method. |