{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:09:27Z","timestamp":1778256567798,"version":"3.51.4"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_3","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"75-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Modeling for Verification"],"prefix":"10.1007","author":[{"given":"Sanjit A.","family":"Seshia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR5","series-title":"LNCS","volume-title":"Real Time: Theory in Practice","author":"R. Alur","year":"1992","unstructured":"Alur, R., Henzinger, T.: Logics and models of real time: a survey. In: Real Time: Theory in Practice. LNCS, vol.\u00a0600 (1992)"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Form. Methods Syst. Des. 15, 7\u201348 (1999)","journal-title":"Form. Methods Syst. Des."},{"issue":"9","key":"3_CR7","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C. Baier","year":"2010","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"3_CR8","series-title":"LNCS","volume-title":"Validation of Stochastic Systems\u2014A Guide to Current Research","year":"2004","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P., Siegle, M. (eds.): Validation of Stochastic Systems\u2014A Guide to Current Research. LNCS, vol.\u00a02925. Springer, Heidelberg (2004)"},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/0304-3975(94)00046-8","volume":"135","author":"C. Baier","year":"1994","unstructured":"Baier, C., Majster-Cederbaum, M.: Denotational semantics in the CPO and metric approach. Theor. Comput. Sci. 135(2), 171\u2013220 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/MC.2003.1193228","volume":"36","author":"F. Balarin","year":"2003","unstructured":"Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, R., Sangiovanni-Vincentelli, A.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36, 45\u201352 (2003)","journal-title":"IEEE Comput."},{"key":"3_CR11","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol.\u00a04. IOS Press, Amsterdam (2009). Chap.\u00a08"},{"key":"3_CR12","first-page":"162","volume-title":"Third International Symposium on Formal Methods for Components and Objects (FMCO)","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., Larsen, K., Rasmussen, J.: Priced timed automata: algorithms and applications. In: Third International Symposium on Formal Methods for Components and Objects (FMCO), pp.\u00a0162\u2013182 (2004)"},{"key":"3_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-00602-9_4","volume-title":"HSCC\u201909: Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control","author":"A. Benveniste","year":"2009","unstructured":"Benveniste, A., Caspi, P., Lublinerman, R., Tripakis, S.: Actors without directors: a Kahnian view of heterogeneous systems. In: HSCC\u201909: Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control. LNCS, pp.\u00a046\u201360. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00602-9_4"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"3_CR15","unstructured":"Brady, B., Bryant, R., Seshia, S.: Abstracting RTL designs to the term level. Tech. Rep. UCB\/EECS-2008-136, EECS Department, University of California, Berkeley (2008) http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2008\/EECS-2008-136.html"},{"key":"3_CR16","volume-title":"Proceedings of the Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","author":"B. Brady","year":"2010","unstructured":"Brady, B., Bryant, R., Seshia, S., O\u2019Leary, J.: ATLAS: automatic term-level abstraction of RTL designs. In: Proceedings of the Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2010)"},{"key":"3_CR17","volume-title":"6th International Workshop on Multi-paradigm Modeling (MPM\u201912)","author":"D. Broman","year":"2012","unstructured":"Broman, D., Lee, E., Tripakis, S., T\u00f6rngren, M.: Viewpoints, formalisms, languages, and tools for cyber-physical systems. In: 6th International Workshop on Multi-paradigm Modeling (MPM\u201912) (2012)"},{"key":"3_CR18","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Specification and Development of Interactive Systems","author":"M. Broy","year":"2001","unstructured":"Broy, M., Stolen, K.: Specification and Development of Interactive Systems. Monographs in Computer Science, vol.\u00a062. Springer, Heidelberg (2001)"},{"issue":"8","key":"3_CR19","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Proc. Computer-Aided Verification (CAV\u201902)","author":"R. Bryant","year":"2002","unstructured":"Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K. (eds.) Proc. Computer-Aided Verification (CAV\u201902). LNCS, vol.\u00a02404, pp.\u00a078\u201392 (2002)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Buck, J.: Scheduling dynamic dataflow graphs with bounded memory using the token flow model. Ph.D. thesis, University of California, Berkeley (1993)","DOI":"10.1109\/ICASSP.1993.319147"},{"key":"3_CR22","volume-title":"14th ACM Symp. POPL","author":"P. Caspi","year":"1987","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: 14th ACM Symp. POPL. ACM, New York (1987)"},{"key":"3_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-87531-4_28","volume-title":"Proc. Computer Science Logic (CSL)","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. In: Proc. Computer Science Logic (CSL). LNCS, vol.\u00a05213, pp.\u00a0385\u2013400 (2008)"},{"key":"3_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-03409-1_2","volume-title":"Fundamentals of Computation Theory (FCT)","author":"K. Chatterjee","year":"2009","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.: Alternating weighted automata. In: Fundamentals of Computation Theory (FCT). LNCS, vol.\u00a05699, pp.\u00a03\u201313 (2009)"},{"key":"3_CR25","volume-title":"Model Checking","year":"2001","unstructured":"Clarke, E., Grumberg, O., Peled, D. (eds.): Model Checking. MIT Press, Cambridge (2001)"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/S0022-0000(71)80013-2","volume":"5","author":"F. Commoner","year":"1971","unstructured":"Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5, 511\u2013523 (1971)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"3_CR27","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1109\/18.61109","volume":"37","author":"R.L. Cruz","year":"1991","unstructured":"Cruz, R.L.: A calculus for network delay, part I. Network elements in isolation. IEEE Trans. Inf. Theory 37(1), 114\u2013131 (1991)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"1","key":"3_CR28","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45\u201380 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"3_CR29","volume-title":"Conference on Using Hardware Design and Verification Languages (DVCon)","author":"A. Davare","year":"2007","unstructured":"Davare, A., Densmore, D., Meyerowitz, T., Pinto, A., Sangiovanni-Vincentelli, A., Yang, G., Zeng, H., Zhu, Q.: A next-generation design framework for platform-based design. In: Conference on Using Hardware Design and Verification Languages (DVCon), vol.\u00a0152 (2007)"},{"key":"3_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-4483-2","volume-title":"Markov Models and Optimization","author":"M. Davis","year":"1993","unstructured":"Davis, M.: Markov Models and Optimization. Chapman & Hall, London (1993)"},{"key":"3_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III: Verification and Control","author":"C. Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Alur, R., Henzinger, T., Sontag, E. (eds.) Hybrid Systems III: Verification and Control. LNCS, vol.\u00a01066, pp.\u00a0208\u2013219. Springer, Heidelberg (1996)"},{"issue":"1","key":"3_CR32","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J. Eker","year":"2003","unstructured":"Eker, J., Janneck, J., Lee, E., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity\u2014the Ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"key":"3_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04293-9","volume-title":"Introduction to Process Algebra","author":"W. Fokkink","year":"2000","unstructured":"Fokkink, W.: Introduction to Process Algebra. Springer, Heidelberg (2000)"},{"key":"3_CR34","series-title":"LNCS","volume-title":"Abstract State Machines, Theory and Applications","year":"2000","unstructured":"Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.): Abstract State Machines, Theory and Applications, Proceedings of the International Workshop, ASM 2000, Monte Verit\u00e0, Switzerland, March 19\u201324, 2000. LNCS, vol.\u00a01912. Springer, Heidelberg (2000)"},{"key":"3_CR35","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"3_CR36","volume-title":"Communicating Sequential Processes","author":"C. Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice Hall, New York (1985)"},{"key":"3_CR37","doi-asserted-by":"crossref","first-page":"492","DOI":"10.1145\/2024724.2024840","volume-title":"Proceedings of the Design Automation Conference (DAC)","author":"D. Holcomb","year":"2011","unstructured":"Holcomb, D., Brady, B., Seshia, S.: Abstraction-based performance analysis of NoCs. In: Proceedings of the Design Automation Conference (DAC), pp.\u00a0492\u2013497 (2011)"},{"key":"3_CR38","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"2006","unstructured":"Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley, Reading (2006)","edition":"3"},{"key":"3_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-46430-1_16","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"J. Hu","year":"2000","unstructured":"Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a01790, pp.\u00a0160\u2013173. Springer, Heidelberg (2000)"},{"key":"3_CR40","unstructured":"ITU: Z.120\u2014Message Sequence Chart (MSC). Available at http:\/\/www.itu.int\/rec\/T-REC-Z.120 (02\/2011)"},{"key":"3_CR41","unstructured":"ITU: Z.120 Annex B: Formal semantics of Message Sequence Charts. Available at http:\/\/www.itu.int\/rec\/T-REC-Z.120 (04\/1998)"},{"key":"3_CR42","series-title":"Proceedings of IFIP Congress","volume-title":"Information Processing 74","author":"G. Kahn","year":"1974","unstructured":"Kahn, G.: The semantics of a simple language for parallel programming. In: Information Processing 74. Proceedings of IFIP Congress, vol.\u00a074. North-Holland, Amsterdam (1974)"},{"issue":"6","key":"3_CR43","doi-asserted-by":"publisher","first-page":"1390","DOI":"10.1137\/0114108","volume":"14","author":"R. Karp","year":"1966","unstructured":"Karp, R., Miller, R.: Properties of a model for parallel computations: determinacy, termination, queueing. SIAM J. Appl. Math. 14(6), 1390\u20131411 (1966)","journal-title":"SIAM J. Appl. Math."},{"key":"3_CR44","volume-title":"Switching and Finite Automata Theory","author":"Z. Kohavi","year":"1978","unstructured":"Kohavi, Z.: Switching and Finite Automata Theory, 2nd edn. McGraw-Hill, New York (1978)","edition":"2"},{"key":"3_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907)","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907). LNCS, vol.\u00a04486, pp.\u00a0220\u2013270. Springer, Heidelberg (2007)"},{"issue":"2","key":"3_CR46","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1-2","key":"3_CR47","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"Kim G. Larsen","year":"1997","unstructured":"Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1\/2) (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"9","key":"3_CR48","doi-asserted-by":"publisher","first-page":"1235","DOI":"10.1109\/PROC.1987.13876","volume":"75","author":"E. Lee","year":"1987","unstructured":"Lee, E., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75(9), 1235\u20131245 (1987)","journal-title":"Proc. IEEE"},{"key":"3_CR49","volume-title":"Introduction to Embedded Systems\u2014A Cyber-physical Systems Approach","author":"E. Lee","year":"2011","unstructured":"Lee, E., Seshia, S.: Introduction to Embedded Systems\u2014A Cyber-physical Systems Approach (2011)"},{"issue":"1","key":"3_CR50","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.tcs.2008.08.044","volume":"409","author":"X. Liu","year":"2008","unstructured":"Liu, X., Lee, E.: CPO semantics of timed interactive actor networks. Theor. Comput. Sci. 409(1), 110\u2013125 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"3_CR51","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S. Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"3_CR52","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)"},{"key":"3_CR53","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"3_CR54","volume-title":"Communicating and Mobile Systems: The \u03c0$\\pi$-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The \u03c0$\\pi$-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"3_CR55","unstructured":"Peh, L.S.: Flow control and micro-architectural mechanisms for extending the performance of interconnection networks. Ph.D. thesis, Stanford University (2001)"},{"key":"3_CR56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction","author":"W. Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985)"},{"key":"3_CR57","volume-title":"7th International Workshop on Formal Aspects of Component Software (FACS)","author":"S. Seshia","year":"2010","unstructured":"Seshia, S.: Quantitative analysis of software: challenges and recent advances. In: 7th International Workshop on Formal Aspects of Component Software (FACS) (2010)"},{"key":"3_CR58","volume-title":"FORMATS 2013","author":"C. Stergiou","year":"2013","unstructured":"Stergiou, C., Tripakis, S., Matsikoudis, E., Lee, E.: On the verification of timed discrete-event models. In: FORMATS 2013. Springer, Heidelberg (2013)"},{"key":"3_CR59","unstructured":"Theelen, B., Geilen, M., Stuijk, S., Gheorghita, S., Basten, T., Voeten, J., Ghamarian, A.: Scenario-aware dataflow. Tech. Rep. ESR-2008-08, Eindhoven University of Technology, (2008)"},{"issue":"5","key":"3_CR60","doi-asserted-by":"publisher","first-page":"960","DOI":"10.1109\/JPROC.2015.2510366","volume":"104","author":"S. Tripakis","year":"2016","unstructured":"Tripakis, S.: Compositionality in the science of system design. Proc. IEEE 104(5), 960\u2013972 (2016)","journal-title":"Proc. IEEE"},{"key":"3_CR61","doi-asserted-by":"publisher","first-page":"834","DOI":"10.1017\/S0960129512000278","volume":"23","author":"S. Tripakis","year":"2013","unstructured":"Tripakis, S., Stergiou, C., Shaver, C., Lee, E.: A modular formal semantics for Ptolemy. Math. Struct. Comput. Sci. 23, 834\u2013881 (2013). doi:10.1017\/S0960129512000278","journal-title":"Math. Struct. Comput. Sci."},{"key":"3_CR62","series-title":"LNCS","volume-title":"Proc. of the 4th Int. Conf. on Concurrency Theory (CONCUR)","author":"R. Yates","year":"1993","unstructured":"Yates, R.: Networks of real-time processes. In: Best, E. (ed.) Proc. of the 4th Int. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a0715. Springer, Heidelberg (1993)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T17:57:32Z","timestamp":1661277452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_3","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}