Saturday , April 20 2024

State Space Search for Safe Time Petri Nets Based on
Binary Decision Diagrams Tools: Application to
Air Traffic Flow Management Problem

Mohamed Ali KAMMOUN1, Nidhal REZG1,2, Zied ACHOUR1,2, Sadok REZIG1,2
1 Industrial Engineering and Production Laboratory of Maintenance,
Enim, Lorraine University,
Metz, France
mohamed-ali.kammoun@univ-lorraine.fr, nidhal.rezg@univ-lorraine.fr, zied.achour@univ-lorraine.fr, sadok.rezig@univ-lorraine.fr
2 ICN Business School,
Metz-Nancy, France

Abstract: The highly concurrent time discrete event systems modeled by Time Petri Net (TPN) suffer from the problem of the state space explosion owing to a large number of accessible markings. To handle this problem, this paper proposes a new solution based on modelling in discrete time the reachable markings of TPN using a new structure so-called Time Reduced Ordered Binary Decision Diagrams (TROBDDs). In this work a new efficient methodology is presented to generate and store a big state space to deal with the time execution and memory space constraints. This new approach is used to resolve the Flight Rescheduling Problem (FRP) subject to capacity constraints due to adverse weather conditions. An optimization algorithm is proposed to minimize the cost function and determine the optimal flight plan according to the new capacity constraints. A number of instances on the FRP is presented in order to illustrate such approach, which allows us to save the memory space and CPU requirements.

Keywords: Discrete event system, Time Petri Net, binary decision diagram, rescheduling problem.

>>Full text<<
 CITE THIS PAPER AS:
Mohamed Ali KAMMOUN, Nidhal REZG, Zied ACHOUR, Sadok REZIG, State Space Search for Safe Time Petri Nets Based on Binary Decision Diagrams Tools: Application to Air Traffic Flow Management Problem, Studies in Informatics and Control, ISSN 1220-1766, vol. 25(1), pp. 39-50, 2016. https://doi.org/10.24846/v25i1y201605

  1. Introduction

The Time Petri Net (TPN) is obtained from the Petri Net by associating a time interval for each transition. The TPN is considered as a perfect tool to modelize a large class of time discrete models. Therefore, several existing methods for the TPN analysis used the enumeration of state space. Besides, for highly competitive systems, the size of state space grows exponentially.

To overcome this problem, several methods are proposed such as partial order unfolding [5] which are limited to safe TPN, and consist in transforming a TPN to an acyclic Petri net, by respecting on one hand the firing time constraints and on the other hand the partial order of the initial model. Our previous approach [7] is ensured by a new structure so-called Discrete Time Reachability Graph (DT-RG). Each node of the DT-RG, called macro-state, represents a particular marking of the T-BPN. Furthermore, each macro-state integrates a set of timed micro-states where each one corresponds to a particular clock value associated to each transition enabled by the marking.

A symbolic method can be used to relieve the above constraints, by taking the advantage of Binary Decision Diagrams (BDDs) capacity to represent a large set of encoded data with small data structure. The BDD structure is initially used to generate Petri net state space by Pasteur et al. [10]. This work develops an algorithm for PN state space exploration by encoding each PN place using a binary variable. Taking the advantage of the BDD compact representation, the exploration of reachable states is done within hours [13]. With the same objective, [11] introduced more useful coding using the place invariants. However, the underlying logic is always based on Boolean variables. A Multi-Valued Decision Diagram (MDD) that is an extension of BDD, have been used by [9] to improve the running time of algorithm previously given to state-space exploration. However, the methods based on BDDs have been successfully applied to untimed Petri nets, but for the TPNs less progress has been made.

In this work, the key idea is to introduce firstly a symbolic approach to compute the markings, in discrete time, of Safe Time Petri Net (STPN) that is composed of Time Binary Petri Nets set. Next we introduce the temporal information to the BDD tools, and we develop an algorithm which allows us to model in each time slice the reachable markings in a small data structure with polynomial complexity space.

The structure is so-called Time Reduced Ordered Binary Decision Diagrams (TROBDDs). The state space is built by exploration of TROBDDs and its storage into stacks. The intended application concerns the Flight Rescheduling Problem (FRP) due to a reduction of available capacity in air traffic network. In air traffic management the time slice is 15 minutes and the planning horizon is one day for tactical decision. So, the time study is limited to 96 time slices, which makes practicable the use of a discrete-time model. Our point of view on the FRP is focused on the accessibility problem under capacity constraints floating in time. We model the itineraries set of rescheduled flights using the STPN. Therefore, a cost function is associated to TROBDDs model. Next one can develop an optimization algorithm based on optimization criterion in order to determine the optimal flight plan.

This paper is organized as follows; the section 2 describes the background of the time Petri nets tools and binary decision diagrams. The section 3 depicts the symbolic approach to compute the reachable makings. The Section 4 presents the modeling reachable makings through TROBDDs. The exploration of state space and the storage technic is presented in Section 5. In order to illustrate the application of our approach, the FRP is presented in Section 6. We report the experimental results and discussion in Section 7. Finally, the conclusion and the future work are presented in Section 8.

REFERENCES

  1. ACHOUR, Z., N. REZG, Time floating general mutual exclusion constraints, Studies in Informatics and Control, 16, no. 1, 2007, pp. 57–66.
  2. BERTHOMIEU, B., F. VERNADAT, State class constructions for branching analysis of time Petri nets, Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2003. pp. 442-457.
  3. BRYANT, R.E, Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, ACM Computing Surveys, 1992, vol. 24, no. 2, pp. 293-318.
  4. BROWN, F. M, Boolean reasoning, Dordrecht: Kluwer Academic Publishers, 1990.
  5. CHATAIN, T., C. JARD, Complete finite prefixes of symbolic unfoldings of safe time Petri nets, In Petri Nets and Other Models of Concurrency-ICATPN Springer Berlin Heidelberg, 2006, pp. 125-145.
  6. FUJITA, M., Y. MATSUNAGA., T. KAKUDA, On variable ordering of binary decision diagrams for the application of multi-level logic synthesis, in : Proceedings of the conference on European design automation, 1991, pp. 50-54.
  7. KAMMOUN, M.A., N. REZG., Z. ACHOUR, New approach for air traffic management based on control theory, International Journal of Production Research (IJPR), 2014, vol. 52, no.6, pp.1711-1727.
  8. LIAW, H. T., C. S. LIN, On the OBDD-representation of general Boolean functions, IEEE Transactions on computers, 1992, vol. 41, no.6, pp. 661-664.
  9. MINER, A.S., G. CIARDO, Efficient reachability set generation and storage using decision diagrams, Application and Theory of Petri Nets Springer Berlin Heidelberg, 1999, pp. 6-25.
  10. PASTOR, E., O. ROIG., J. CORTADELLA., R. M. BADIA, Petri net analysis using Boolean manipulation, Application and Theory of Petri Nets, Springer Berlin Heidelberg, 1994, pp. 416-435.
  11. PASTOR, E., J. CORTADELLA, Efficient encoding schemes for symbolic analysis of Petri nets, proceedings of the conference on Design, automation and test in Europe. IEEE Computer Society, 1998. pp. 790-795.
  12. PASTOR, E., J. CORTADELLA., O. ROIG, Symbolic Analysis of Bounded Petri Nets, IEEE Transactions on Computers, 2001, vol.50, no.5, pp. 432-448.
  13. ROIG, O., J. CORTADELLA., E. PASTOR, Verification of asynchronous circuits by BDD-based model checking of Petri nets, In Application and Theory of Petri Nets, 1995, pp. 374-391.
  14. RUDELL, R, Dynamic variable ordering for ordered binary decision diagrams, In Proceedings of IEEE/ACM international conference on Computer-aided design, 1993, pp. 42-47.
  15. TOKTAS, B, Addressing Capacity Uncertainty in Resource-Constrained Assignment Problems, PhD Thesis, university of Washington, 2003.
Designed by | ICI Bucharest
© Copyright 2024, All Rights Reserved