Articles Event Segment Timed Event System Verifiable sub-classes of DEVS: SP-DEVS, FD-DEVS Behavior of Atomic DEVS Behavior of Coupled DEVS Simulation Algorithms for Atomic DEVS Simulation Algorithms for Coupled DEVS Other Formalisms Automata Theory: a formal method for state transition systems Finite State Machine: a state transition machine with finite sets of events and states Petri Nets: a graphical representation of state and transition relations Markov Chain: a stochastic process in which the future will be determined by the current state Specification and Description Language: SDL, a formal complete and unambiguous language to graphically represent simulation models. Footnotes References [Cellier91] [CK06] [Giambiasi01] Giambiasi N., Escude B. Ghosh S. “Generalized Discrete Event Simulation of Dynamic Systems”, in: Issue 4 of SCS Transactions: Recent Advances in DEVS Methodology-part II, Vol. 18, pp. 216–229, dec 2001 [Hwang05] M.H. Hwang, "Tutorial: Verification of Real-time System Based on Schedule-Preserved DEVS", Proceedings of 2005 DEVS Symposium, San Diego, Apr. 2-8, 2005, , [HZ06] M.H. Hwang and B. P. Zeigler, "A Modular Verification Framework using Finite and Deterministic DEVS", Proceedings of 2006 DEVS Symposium, pp57–65, Huntsville, Alabama, USA, [HZ09] M.H. Hwang and B.P. Zeigler, "Reachability Graph of Finite and Deterministic DEVS Networks", IEEE Transactions on Automation Science and Engineering, Volume 6, Issue 3, 2009, pp. 454–467, [Hwang12] M.H. Hwang, "Qualitative verification of finite and real-time DEVS networks", Proceedings of the 2012 Symposium on Theory of Modeling and Simulation - DEVS Integrative M&S Symposium, Article No. 43, [Mittal13] [Nutaro10] [Sarjoughian09] [Wainer09] [Wainer10] [Zacharewicz08] Gregory Zacharewicz, Claudia Frydman, and Norbert Giambiasi (2008) G-DEVS/HLA Environment for Distributed Simulations of Workflows, SIMULATION May 2008 84: 197-213, . [Zeiger68] [Zeigler76] [Zeigler84] [Zeigler87] [ZKP00] Automata (computation) Formal specification languages