Reachability Analysis of Augmented Marked Graphs via Integer Linear Programming

Augmented marked graphs (AMGs) are 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 (FMSs). To our knowledge, the techniques developed for analyzing AMGs are mostly based upon checking certain Petri net structures such as siphons. This article 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. Examples arisen in FMSs are used to demonstrate the application of our technique.