{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T04:52:39Z","timestamp":1726030359090},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_2","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:03:25Z","timestamp":1558998205000},"page":"19-35","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["$$\\textsf {ML}_{\\nu }$$ : A Distributed Real-Time Modal Logic"],"prefix":"10.1007","author":[{"given":"James","family":"Ortiz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moussa","family":"Amrani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Schobbens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-48340-3_12","volume-title":"Mathematical Foundations of Computer Science 1999","author":"L Aceto","year":"1999","unstructured":"Aceto, L., Laroussinie, F.: Is your model checker on time? In: Kuty\u0142owski, M., Pacholski, L., Wierzbicki, T. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 125\u2013136. Springer, Heidelberg (1999). \n                    https:\/\/doi.org\/10.1007\/3-540-48340-3_12"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-540-85361-9_10","volume-title":"CONCUR 2008 - Concurrency Theory","author":"S Akshay","year":"2008","unstructured":"Akshay, S., Bollig, B., Gastin, P., Mukund, M., Narayan Kumar, K.: Distributed timed automata with independently evolving clocks. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 82\u201397. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-85361-9_10"},{"key":"2_CR3","unstructured":"Al-Bataineh, O.I., Reynolds, M., French, T., Woodings, T.: Verifying real-time commit protocols using dense-time model checking technology. CoRR, volume 1201-3416 (2012)"},{"key":"2_CR4","unstructured":"Alur, R.: Techniques for automatic verification of real-time systems. Ph.D. thesis, Stanford University, CA, USA (1992)"},{"issue":"2","key":"2_CR5","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.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). \n                    https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.3176\/proc.2017.1.08","volume":"66","author":"A Anier","year":"2017","unstructured":"Anier, A., Vain, J., Tsiopoulos, L.: DTRON: a tool for distributed model-based testing of time critical applications. Proc. Est. Acad. Sci. 66, 75 (2017)","journal-title":"Proc. Est. Acad. Sci."},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.icte.2018.01.013","volume":"4","author":"M Asplund","year":"2018","unstructured":"Asplund, M.: Automatically proving the correctness of vehicle coordination. ICT Express 4, 51\u201354 (2018). SI: CI & Smart Grid Cyber Security","journal-title":"ICT Express"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-56496-9_24","volume-title":"Computer Aided Verification","author":"K \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 302\u2013315. Springer, Heidelberg (1993). \n                    https:\/\/doi.org\/10.1007\/3-540-56496-9_24"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/227210.227231","volume":"39","author":"F Cristian","year":"1996","unstructured":"Cristian, F.: Synchronous and asynchronous. Commun. ACM 39, 273\u2013297 (1996)","journal-title":"Commun. ACM"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"De Biasi, M., Snickars, C., Landern\u00e4s, K., Isaksson, A.: Simulation of process control with wirelesshart networks subject to clock drift. In: Proceedings of the 2008 32nd Annual IEEE International Computer Software and Applications Conference COMPSAC 2008 (2008)","DOI":"10.1109\/COMPSAC.2008.163"},{"key":"2_CR11","unstructured":"Gwaltney, D.A., Briscoe, J.M.: Comparison of communication architectures for spacecraft modular avionics systems. Technical Report 214431, NASA (2006). \n                    http:\/\/www.sti.nasa.gov\/"},{"issue":"2","key":"2_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.entcs.2014.10.011","volume":"308","author":"S Jaziri","year":"2014","unstructured":"Jaziri, S., Larsen, K.G., Mardare, R., Xue, B.: Adequacy and complete axiomatization for timed modal logic. Electr. Notes Theor. Comput. Sci. 308, 183\u2013210 (2014)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Krishnan, P.: Distributed timed automata. In: Workshop on Distributed Systems, vol. 28 (1999)","DOI":"10.1016\/S1571-0661(05)80627-9"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"Mathematical Foundations of Computer Science 1995","author":"F Laroussinie","year":"1995","unstructured":"Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic \u2014 and back. In: Wiedermann, J., H\u00e1jek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529\u2013539. Springer, Heidelberg (1995). \n                    https:\/\/doi.org\/10.1007\/3-540-60246-1_158"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.tcs.2014.03.007","volume":"546","author":"KG Larsen","year":"2014","unstructured":"Larsen, K.G., Mardare, R.: Complete proof systems for weighted modal logic. Theor. Comput. Sci. 546, 164\u2013175 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR17","unstructured":"Mall, R., Patnaik, L.: Specification and verification of timing properties of distributed real-time systems (1990)"},{"key":"2_CR18","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, New York (1989)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Monot, A., Navet, N., Bavoux, B.: Impact of clock drifts on CAN frame response time distributions. In: 16th IEEE International Conference on Emerging Technologies and Factory Automation - ETFA, Toulouse, France, p. 2011, September 2011","DOI":"10.1109\/ETFA.2011.6059186"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-57288-8_4","volume-title":"NASA Formal Methods","author":"J Ortiz","year":"2017","unstructured":"Ortiz, J., Amrani, M., Schobbens, P.-Y.: Multi-timed bisimulation for distributed timed automata. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 52\u201367. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-57288-8_4"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-22256-6_23","volume-title":"Implementation and Application of Automata","author":"J Ortiz","year":"2011","unstructured":"Ortiz, J., Legay, A., Schobbens, P.-Y.: Distributed event clock automata. In: Bouchou-Markhoff, B., Caron, P., Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2011. LNCS, vol. 6807, pp. 250\u2013263. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22256-6_23"},{"key":"2_CR22","unstructured":"Ramasamy, H.V., Cukier, M., Sanders, W.H.: Formal specification and verification of a group membership protocol for an intrusion-tolerant group communication system. In: Pacific Rim International Symposium on Dependable Computing (2002)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-27308-2_4","volume-title":"Euro-Par 2015: Parallel Processing Workshops","author":"M Raynal","year":"2015","unstructured":"Raynal, M.: Parallel computing vs. distributed computing: a great confusion? (position paper). In: Hunold, S., et al. (eds.) Euro-Par 2015. LNCS, vol. 9523, pp. 41\u201353. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-27308-2_4"},{"issue":"1","key":"2_CR24","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods Syst. Des. 18(1), 25\u201368 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR25","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/158431.158434","volume":"2","author":"F Wang","year":"1993","unstructured":"Wang, F., Mok, A.K., Emerson, E.A.: Distributed real-time system specification and verification in APTL. ACM Trans. Softw. Eng. Methodol. 2, 346\u2013378 (1993)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-30232-2_13","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"X Wang","year":"2004","unstructured":"Wang, X., Wang, J., Qi, Z.-C.: Automatic generation of run-time test oracles for distributed real-time systems. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 199\u2013212. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30232-2_13"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:13:48Z","timestamp":1558998828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}