--- _id: '3362' abstract: - lang: eng text: State-transition systems communicating by shared variables have been the underlying model of choice for applications of model checking. Such formalisms, however, have difficulty with modeling process creation or death and communication reconfigurability. Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling formalism that supports dynamic reconfiguration and creation/death of processes. The resulting formalism supports two types of variables, data variables and reference variables. Reference variables enable changing the connectivity between processes and referring to instances of processes. We show how this new formalism supports parallel composition and refinement through trace containment. DRM provide a natural language for modeling (and ultimately reasoning about) biological systems and multiple threads communicating through shared variables. alternative_title: - LNCS article_processing_charge: No author: - first_name: Jasmin full_name: Fisher, Jasmin last_name: Fisher - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic - first_name: Nir full_name: Piterman, Nir last_name: Piterman - first_name: Anmol full_name: Singh, Anmol last_name: Singh - first_name: Moshe full_name: Vardi, Moshe last_name: Vardi citation: ama: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. Dynamic reactive modules. In: Vol 6901. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2011:404-418. doi:10.1007/978-3-642-23217-6_27' apa: 'Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., & Vardi, M. (2011). Dynamic reactive modules (Vol. 6901, pp. 404–418). Presented at the CONCUR: Concurrency Theory, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-23217-6_27' chicago: Fisher, Jasmin, Thomas A Henzinger, Dejan Nickovic, Nir Piterman, Anmol Singh, and Moshe Vardi. “Dynamic Reactive Modules,” 6901:404–18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. https://doi.org/10.1007/978-3-642-23217-6_27. ieee: 'J. Fisher, T. A. Henzinger, D. Nickovic, N. Piterman, A. Singh, and M. Vardi, “Dynamic reactive modules,” presented at the CONCUR: Concurrency Theory, Aachen, Germany, 2011, vol. 6901, pp. 404–418.' ista: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. 2011. Dynamic reactive modules. CONCUR: Concurrency Theory, LNCS, vol. 6901, 404–418.' mla: Fisher, Jasmin, et al. Dynamic Reactive Modules. Vol. 6901, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:10.1007/978-3-642-23217-6_27. short: J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, A. Singh, M. Vardi, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–418. conference: end_date: 2011-09-09 location: Aachen, Germany name: 'CONCUR: Concurrency Theory' start_date: 2011-09-06 date_created: 2018-12-11T12:02:54Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:57Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-642-23217-6_27 ec_funded: 1 file: - access_level: open_access checksum: 6bf2453d8e52e979ddb58d17325bad26 content_type: application/pdf creator: dernst date_created: 2020-05-19T16:17:48Z date_updated: 2020-07-14T12:46:10Z file_id: '7870' file_name: 2011_CONCUR_Fisher.pdf file_size: 337125 relation: main_file file_date_updated: 2020-07-14T12:46:10Z has_accepted_license: '1' intvolume: ' 6901' language: - iso: eng month: '01' oa: 1 oa_version: Submitted Version page: 404 - 418 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '3253' quality_controlled: '1' scopus_import: 1 status: public title: Dynamic reactive modules type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6901 year: '2011' ...