Booming world trade, scarcity of land for yard expansion in many ports, and deployment of new, massive megaships have magnified the need to find better ways of performing container terminal operations. Automated guided vehicle systems (AGVS) have been proposed as possible candidates for future automated container operation because of their ability to significantly improve the performance of container terminals. However, before the deployment of AGVS, computer model simulations to investigate the potential problems are necessary to successfully implement the system. Petri net is a well-known modeling tool that, with the advantages of its graphic nature and the availability of mathematical analysis techniques, is clearly suitable for the application of automated container terminal systems (ACTS) modeling. A timed-place petri net (TPPN) model of ACTS using automated guided vehicles (AGVs) is constructed. The TPPN model contains a transportation layout module, two unit submodels, an AGV unit submodel, and a crane unit submodel. The transportation layout module serves as a basic unit to construct the transportation road map of the system. The AGV unit submodel is used to model the traveling behavior of the AGV on a node-to-node basis, and the crane unit submodel is used to model the crane's container-loading and -unloading movement. A collision-free control rule, which is primely modeled using inhibitor and actuator arcs, is embedded in the submodels to ensure a collision-free environment for the AGVs. The important properties of the model such as liveness, safeness, and reversibility are analyzed.