Formal Semantics, Algorithm Evaluation Of Logical Process Paradigm And Their Application In Spatial Stochastic Simulation

Traditional spatial stochastic simulation methods cannot meet the requirements oflarge scale and fine grain bio-chemical reaction network applications any longer. With-out the formal method, the modeling of logical process(LP)-based parallel discrete eventsimulation(PDES) usually tightly coupled with specific simulation platform. This ob-structs a formal analysis of the model's behavior. The execution performance of largescale spatial parallel stochastic simulation is very sensitive to the simulation algorithmsused. The behavioral complexity of the model, the physical characters of the platformand other factors lead to difficulties in effective simulation performance evaluation usingcomputational complexity theory. Therefore, to study the formal semantics and experi-mental algorithmic performance evaluation for LP paradigm are of great theoretical im-portance. And to study the equivalence problem of execution results and the simulationalgorithm selection problem in spatial parallel stochastic simulation, are of great practi-cal importance. This work will broaden the application domain of PDES, and facilitatefurther development of the modeling methodology and algorithm evaluation approachesin PDES.Inthisdissertation, weconductanin-depthresearchontheformalsemantics,simula-tion algorithm evaluation, as well as their applications in equivalence proof and algorithmevaluation for an efficient parallel spatial stochastic simulation. The innovations of thisdissertation are as follows:First, a formalism called Partitioned Event Graph(PEG) is proposed for logical pro-cess paradigm. The current lack of formal method obstructs the formal analysis of modelproperties. Targeting this problem, PEG is presented in this dissertation to formally de-scribe the event scheduling and the state partition in LP paradigm, together with thestructural operational semantics of PEG on the Timed Transition System. As a platform-independent semantic specification, PEG sets the foundation for the formal analysis ofPDES model and the model driven development.Second, an experimental performance evaluation method for LP simulation algo-rithms is proposed. Performance evaluation has been always a hot topic in PDES sincethe high cost for parallelizing existed applications and the strong demands for high per-formance. However, the assertions from algorithmic complexity theory are usually too general to meet the specific requirement of the simulation application. Thus the exper-imental method becomes an important approach for evaluating the simulation algorithmperformances. There is a lack of flexibility in algorithm experiment design and the open-ness of architecture in mainstream LP-based simulation platforms. In this dissertation,motivated by the experimental algorithmics, we construct the ontology for LP paradigminDiscreteeventModelingOntology(DeMo)framework, andthenasimulationalgorithmframework for LP paradigm. After that, with the plug'in method, we proposed an experi-mental performance evaluation framework for LP simulation algorithms, named as JamesII-LP. Model description and simulation algorithm are clearly separated with each otherin James II-LP. The framework provides baseline models and simulation algorithms forcomparison, and a flexible method for simulation algorithm experiment design. All ofthese qualify James II-LP as a flexible and open platform for the integration, experiment,and performance evaluation of simulation algorithms.Third, a spatial stochastic simulation method with loose coupling between modeldescription and simulation algorithm is proposed. Spatial stochastic simulation is a veryimportantapproachtorepresentthenoiseandspatialinhomogeneityinbio-chemicalreac-tionnetwork. Spatialstochasticsimulationiscomputationalintensive, alongwiththeevergrowing scale of the applications, using PDES to accelerate the execution is essential tomeettheefficiencydemand. ToalertthesequentialpropertyhamperingparallelexecutionintheNext SubvolumeMethod (NSM)and its descendants, theAbstract Next SubvolumeMethod(ANSM)ispresented. ANSMseparatesthemodelrepresentationwiththesimula-tion algorithms. We prove that the time trajectories generated by the execution of ANSMare statistically accord with those generated by NSM. Experiments are also conducted onthe pseudo random number generator and the parallel simulation with ANSM. The theo-retical analysis and experimental results show that ANSM can achieve parallel executionwhile preserving the statistical accordance, and improve simulation performance.Fourth, this dissertation presents a PEG based model transformation method. Tar-geting the efficient parallel spatial stochastic simulation of domain-specific model, Weproposed a three phased model transformation method(from Domain-Specific Language,throughPEG,toSimulationPlatform-relatedAPI)isproposed. Withthismethod,wecon-duct the simulation experiments of the 2D Lotka-Volterra System based on ANSM. TheYinHe Simulation Utilities for Parallel Environment(YHSUPE) is used as the simulation platform. The results show that proposed method solves the transformation from domain-specific language to LP paradigm, and that the generated platform-dependent model canachieve considerable parallel speedup.This dissertation emphasizes binding the fundamental theoretical research in model-ingandsimulation,withcuttingedgeapplications. Wetaketheefficientparallelexecutionof the spatial stochastic simulation as the motivation and background. The contributionin constructing the formalism of LP and the experimental performance evaluation of LPsimulation algorithms advance the research of PDES in general. Our contribution in par-allelizing the spatial stochastic simulation can also be applied to other applications.