{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T02:25:06Z","timestamp":1769048706597,"version":"3.49.0"},"reference-count":94,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2017,7,15]],"date-time":"2017-07-15T00:00:00Z","timestamp":1500076800000},"content-version":"vor","delay-in-days":14,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["New Gener. Comput."],"published-print":{"date-parts":[[2017,7]]},"DOI":"10.1007\/s00354-017-0023-1","type":"journal-article","created":{"date-parts":[[2017,7,15]],"date-time":"2017-07-15T07:35:51Z","timestamp":1500104151000},"page":"271-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Metamathematics for Systems Design"],"prefix":"10.1007","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,15]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of process algebra, pp. 197\u2013292. Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50021-7"},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0304-3975(95)00011-K","volume":"150","author":"J Ad\u00e1mek","year":"1995","unstructured":"Ad\u00e1mek, J., Koubek, V.: On the greatest fixed point of a set functor. Theor. Comp. Sci. 150, 57\u201375 (1995)","journal-title":"Theor. Comp. Sci."},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In Kroening and Pasareanu [60], pp. 356\u2013374","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"23_CR4","unstructured":"de\u00a0Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, vol. 2719 of Lect. Notes Comp. Sci., pp. 1022\u20131037. Springer (2003)"},{"key":"23_CR5","unstructured":"Almagor, S., Boker U., Kupferman, O.: Discounting in LTL. In: \u00c1brah\u00e1m, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, vol. 8413 of Lecture Notes in Computer Science, pp. 424\u2013439. Springer (2014)"},{"issue":"1","key":"23_CR6","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.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comp. Sci."},{"issue":"2","key":"23_CR7","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)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR8","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198568612.001.0001","volume-title":"Category theory. Oxford Logic Guides","author":"S Awodey","year":"2006","unstructured":"Awodey, S.: Category theory. Oxford Logic Guides. Oxford Univ Press, Oxford (2006)"},{"key":"23_CR9","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. The MIT Press (2008)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4\u20137, 2004, Proceedings, vol. 2999 of Lecture Notes in Computer Science, pp. 1\u201320. Springer (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13\u201318, 2004, Revised Lectures, vol. 3185 of Lecture Notes in Computer Science, pp. 200\u2013236. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"issue":"3","key":"23_CR12","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s00224-003-1061-2","volume":"36","author":"VD Blondel","year":"2003","unstructured":"Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theory Comput. Syst. 36(3), 231\u2013245 (2003)","journal-title":"Theory Comput. Syst."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In Giacobazzi and Cousot [32], pp. 457\u2013468","DOI":"10.1145\/2480359.2429124"},{"key":"23_CR14","unstructured":"B\u00fcchi, J.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science, 1960, pp. 1\u201312. Stanford University Press (1962)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Buss, S.R.: An introduction to proof theory. In: Buss, S.R. (ed) Handbook of proof theory, pp. 1\u201378. Elsevier (1998)","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, vol. 9058 of Lecture Notes in Computer Science, pp. 3\u201311. Springer (2015)","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Voronin, Y., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In Chechik and Raskin [18], pp. 260\u2013279","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Chechik, M., Raskin, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems\u201422nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2\u20138, 2016, Proceedings, vol. 9636 of Lecture Notes in Computer Science. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9"},{"key":"23_CR19","unstructured":"C\u00eerstea, C., Shimizu, S., Hasuo, I.: Parity automata for quantitative linear time logics. In: Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). To appear (2017)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification, 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings of Lecture Notes in Computer Science, vol. 8044, pp. 364\u2013380. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_25"},{"issue":"3","key":"23_CR22","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MSP.2010.203","volume":"9","author":"A Datta","year":"2011","unstructured":"Datta, A., Franklin, J., Garg, D., Jia, L., Kaynar, D.K.: On adversary models and compositional security. IEEE Secur Priv 9(3), 26\u201332 (2011)","journal-title":"IEEE Secur Priv"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Diwakaran, R.D., Sankaranarayanan, S., Trivedi, A.: Analyzing neighborhoods of falsifying traces in cyber-physical systems. In S.\u00a0Mart\u00ednez, E.\u00a0Tovar, C.\u00a0Gill and B.\u00a0Sinopoli, editors, Proceedings of the 8th International Conference on Cyber-Physical Systems, ICCPS 2017, Pittsburgh, Pennsylvania, USA, April 18-20, 2017, pp. 109\u2013119. ACM (2017)","DOI":"10.1145\/3055004.3055029"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds) Formal Modeling and Analysis of Timed Systems-8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings of Lecture Notes in Computer Science, vol. 6246, pp. 92\u2013106. Springer (2010)","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer Publishing Company, Incorporated (2009)","DOI":"10.1007\/978-3-642-01492-5"},{"issue":"42","key":"23_CR26","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J. (ed) Mathematical Aspects of Computer Science of Proceedings of Symposium on Applied Mathematics, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Forsberg, K., Mooz, H.: The relationship of system engineering to the project cycle. In: Proceedings of the National Council for Systems Engineering First Annual Conference, pp. 57\u201361 (1991)","DOI":"10.1002\/j.2334-5837.1991.tb01484.x"},{"key":"23_CR29","unstructured":"Frazzoli, E.: Robust hybrid control of autonomous vehicle motion planning. PhD thesis, Massachusetts Institute of Technology (2001)"},{"key":"23_CR30","unstructured":"Frehse, G., Mitra, S. (eds.) Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18\u201320, 2017. ACM (2017)"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Fu, Z., Su, Z.: XSat: a fast floating-point satisfiability solver. In S.\u00a0Chaudhuri and A.\u00a0Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, of Lecture Notes in Computer Science, vol. 9780, pp. 187\u2013209. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"23_CR32","unstructured":"Giacobazzi, R., Cousot, R. (eds) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. ACM (2013)"},{"issue":"5","key":"23_CR33","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A Girard","year":"2007","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Automatic Control 52(5), 782\u2013798 (2007)","journal-title":"IEEE Trans. Automatic Control"},{"issue":"5\u20136","key":"23_CR34","doi-asserted-by":"publisher","first-page":"568","DOI":"10.3166\/ejc.17.568-578","volume":"17","author":"A Girard","year":"2011","unstructured":"Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5\u20136), 568\u2013578 (2011)","journal-title":"Eur. J. Control"},{"key":"23_CR35","unstructured":"van Glabbeek, R.J.: The linear time\u2013branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chap.\u00a01, pp. 3\u201399. Elsevier (2001)"},{"key":"23_CR36","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In J.D. Herbsleb and M.B. Dwyer, editors, Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31\u2013June 7, 2014, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"23_CR37","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games: A Guide to Current Research, vol. 2500 of Lecture Notes in Computer Science. Springer (2002)","DOI":"10.1007\/3-540-36387-4"},{"issue":"2\u20133","key":"23_CR38","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.tcs.2005.03.045","volume":"342","author":"E Haghverdi","year":"2005","unstructured":"Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. Theor. Comput. Sci. 342(2\u20133), 229\u2013261 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR39","doi-asserted-by":"crossref","unstructured":"Hasuo. I.: Generic forward and backward simulations. In: Baier, C., Hermanns, H. (eds.) International Conference on Concurrency Theory (CONCUR 2006), vol. 4137 of Lect. Notes Comp. Sci., pp. 406\u2013420. Springer, Berlin (2006)","DOI":"10.1007\/11817949_27"},{"key":"23_CR40","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2015.03.047","volume":"604","author":"I Hasuo","year":"2015","unstructured":"Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theor. Comput. Sci. 604, 2\u201329 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR41","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Jacobs, B., A.\u00a0Sokolova. Generic trace semantics via coinduction. Logical Methods in Comp. Sci., 3(4:11), 2007","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"23_CR42","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Jacobs, B., Sokolova, A.: The microcosm principle and concurrency in coalgebra. In: Foundations of Software Science and Computation Structures of Lect. Notes Comp. Sci., vol. 4962, pp. 246\u2013260. Springer (2008)","DOI":"10.1007\/978-3-540-78499-9_18"},{"key":"23_CR43","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In R.\u00a0Bodik and R.\u00a0Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pp. 718\u2013732. ACM (2016)","DOI":"10.1145\/2837614.2837673"},{"key":"23_CR44","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of hybrid systems. In: Madhusudan P., Seshia, S.A. (eds.) CAV, vol. 7358 of Lect. Notes Comp. Sci., pp. 462\u2013478. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_34"},{"key":"23_CR45","doi-asserted-by":"crossref","unstructured":"F.\u00a0Herbreteau, B.\u00a0Srivathsan and I.\u00a0Walukiewicz. Efficient emptiness check for timed b\u00fcchi automata. In T.\u00a0Touili, B.\u00a0Cook and P.B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, vol. 6174 of Lecture Notes in Computer Science, pp. 148\u2013161. Springer, 2010","DOI":"10.1007\/978-3-642-14295-6_15"},{"key":"23_CR46","doi-asserted-by":"crossref","unstructured":"W.\u00a0Hino, H.\u00a0Kobayashi, I.\u00a0Hasuo and B.\u00a0Jacobs. Healthiness from duality. In M.\u00a0Grohe, E.\u00a0Koskinen and N.\u00a0Shankar, editors, Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, July 5-8, 2016, pp. 682\u2013691. ACM, 2016","DOI":"10.1145\/2933575.2935319"},{"key":"23_CR47","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM, 12:576\u2013580, 583 (1969)","DOI":"10.1145\/363235.363259"},{"key":"23_CR48","unstructured":"Holzmann, G.J.: The SPIN Model Checker, primer and reference manual. Addison-Wesley (2004)"},{"key":"23_CR49","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley, Boston, $$3^{rd}$$(edn.) (2006)"},{"key":"23_CR50","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, vol.\u00a059 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2016)","DOI":"10.1017\/CBO9781316823187"},{"key":"23_CR51","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Rutten,J.J.M.M.: An introduction to (co)algebra and (co)induction. In Advanced Topics in Bisimulation and Coinduction, no.\u00a052 in Cambridge Tracts in Theoretical Computer Science, pp. 38\u201399. Cambridge Univ. Press (2011)","DOI":"10.1017\/CBO9780511792588.003"},{"issue":"2","key":"23_CR52","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1006\/inco.1996.0057","volume":"127","author":"A Joyal","year":"1996","unstructured":"Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Inf. & Comp. 127(2), 164\u2013185 (1996)","journal-title":"Inf. & Comp."},{"key":"23_CR53","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M.: Small progress measures for solving parity games. In H.\u00a0Reichel and S.\u00a0Tison, editors, STACS, vol. 1770 of Lecture Notes in Computer Science, pp. 290\u2013301. Springer (2000)","DOI":"10.1007\/3-540-46541-3_24"},{"key":"23_CR54","unstructured":"Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress, pp. 471\u2013475 (1974)"},{"key":"23_CR55","unstructured":"Kane, A.: Runtime monitoring for safety-critical embedded systems. PhD thesis, Carnegie Mellon University (2015)"},{"key":"23_CR56","doi-asserted-by":"crossref","unstructured":"Kido, K., Chaudhuri, S., Hasuo, I.: Abstract interpretation with infinitesimals - towards scalability in nonstandard static analysis. In B.\u00a0Jobstmann and K.R.M. Leino, editors, Verification, Model Checking, and Abstract Interpretation, 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17\u201319, 2016. Proceedings, vol. 9583 of Lecture Notes in Computer Science, pp. 229\u2013249. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_11"},{"key":"23_CR57","doi-asserted-by":"crossref","unstructured":"Kim, E.S., Arcak, M., Seshia, S.A.: A small gain theorem for parametric assume-guarantee contracts. In Frehse and Mitra [30], pp. 207\u2013216","DOI":"10.1145\/3049797.3049805"},{"issue":"2","key":"23_CR58","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/j.ic.2007.10.006","volume":"207","author":"B Klin","year":"2009","unstructured":"Klin, B.: Bialgebraic methods and modal logic in structural operational semantics. Inf. & Comp. 207(2), 237\u2013257 (2009)","journal-title":"Inf. & Comp."},{"key":"23_CR59","unstructured":"Kobayashi, T., Ishikawa, F., Honiden, S.: Refactoring refinement structure of Event-B machines. In: J.S. Fitzgerald, C.L. Heitmeyer, S.\u00a0Gnesi and A.\u00a0Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, vol. 9995 of Lecture Notes in Computer Science, pp. 444\u2013459 (2016)"},{"key":"23_CR60","doi-asserted-by":"crossref","unstructured":"Kroening, D., Pasareanu, C.S.: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II of Lecture Notes in Computer Science. vol. 9207, Springer (2015)","DOI":"10.1007\/978-3-319-21668-3"},{"key":"23_CR61","unstructured":"M.Z. Kwiatkowska, G.\u00a0Norman and D.\u00a0Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G.\u00a0Gopalakrishnan and S.\u00a0Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, vol. 6806 of Lect. Notes Comp. Sci., pp. 585\u2013591. Springer, 2011"},{"key":"23_CR62","doi-asserted-by":"crossref","unstructured":"A.\u00a0Legay, S.\u00a0Sedwards and L.\u00a0Traonouez. Rare events for statistical model checking an overview. In K.G. Larsen, I.\u00a0Potapov and J.\u00a0Srba, editors, Reachability Problems - 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings, vol. 9899 of Lecture Notes in Computer Science, pp. 23\u201335. Springer, 2016","DOI":"10.1007\/978-3-319-45994-3_2"},{"key":"23_CR63","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107360068","volume-title":"Basic Category Theory","author":"T Leinster","year":"2014","unstructured":"Leinster, T.: Basic Category Theory. Cambridge Univ, Press (2014)"},{"issue":"2","key":"23_CR64","first-page":"214","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations. I. Untimed systems. Inf. & Comp. 121(2), 214\u2013233 (1995)","journal-title":"I. Untimed systems. Inf. & Comp."},{"key":"23_CR65","doi-asserted-by":"crossref","unstructured":"L.\u00a0Ma, C.\u00a0Artho, C.\u00a0Zhang, H.\u00a0Sato, J.\u00a0Gmeiner and R.\u00a0Ramler. GRT: program-analysis-guided random testing (T). In M.B. Cohen, L.\u00a0Grunske and M.\u00a0Whalen, editors, 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, pp. 212\u2013223. IEEE Computer Society, 2015","DOI":"10.1109\/ASE.2015.49"},{"key":"23_CR66","unstructured":"S.\u00a0Mac\u00a0Lane. Categories for the Working Mathematician. Springer, Berlin, 2nd edn., 1998"},{"key":"23_CR67","doi-asserted-by":"crossref","unstructured":"R.\u00a0Majumdar. Robots at the edge of the cloud. In Chechik and Raskin [18], pp. 3\u201313","DOI":"10.1007\/978-3-662-49674-9_1"},{"key":"23_CR68","unstructured":"R.\u00a0Milner. Communication and Concurrency. Prentice-Hall, 1989"},{"key":"23_CR69","unstructured":"Miyashita, H., Tai, H., Amano, S.: Controlled modeling environment using flexibly-formatted spreadsheets. In: Jalote, P., Briand, L.C., van\u00a0der Hoek, A. (eds.) 36th International Conference on Software Engineering, ICSE \u201914, Hyderabad, India - May 31\u2013June 07, 2014, pp. 978\u2013988. ACM (2014)"},{"key":"23_CR70","doi-asserted-by":"crossref","unstructured":"Nakagawa S., Hasuo, I.: Near-optimal scheduling for LTL with future discounting. In P.\u00a0Ganty and M.\u00a0Loreti, editors, Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers of Lecture Notes in Computer Science, vol. 9533, pp. 112\u2013130. Springer (2015)","DOI":"10.1007\/978-3-319-28766-9_8"},{"key":"23_CR71","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings 5th GI Conference on Theoretical Computer Science, vol. 104 of Lect. Notes Comp. Sci., pp. 15\u201332. Springer, Berlin (1981)"},{"key":"23_CR72","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical analysis of hybrid systems\u2014proving theorems for complex dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"23_CR73","volume-title":"Non-standard analysis","author":"A Robinson","year":"1966","unstructured":"Robinson, A.: Non-standard analysis. Princeton Univ Press, Princeton (1966)"},{"key":"23_CR74","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comp. Sci. 249, 3\u201380 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"23_CR75","volume-title":"Verifying Nonlinear Real Formulas Via Sums of Squares","year":"2007","unstructured":"Schneider, K., Brandt, J. (eds.): Verifying Nonlinear Real Formulas Via Sums of Squares. Springer, Berlin (2007)"},{"key":"23_CR76","doi-asserted-by":"crossref","unstructured":"Shoukry, Y., Nuzzo, P., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Pappas, G.J., Tabuada, P.: SMC: satisfiability modulo convex optimization. In Frehse and Mitra [30], pp. 19\u201328","DOI":"10.1145\/3049797.3049819"},{"key":"23_CR77","doi-asserted-by":"crossref","unstructured":"Souyris, J., Delmas, D.: Experimental assessment of astr\u00e9e on safety-critical avionics software. In F.\u00a0Saglietti and N.\u00a0Oster, editors, Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007, Nuremberg, Germany, September 18-21, 2007., of Lecture Notes in Computer Science, vol. 4680, pp. 479\u2013490. Springer (2007)","DOI":"10.1007\/978-3-540-75101-4_45"},{"key":"23_CR78","doi-asserted-by":"crossref","unstructured":"Suenaga, K., Hasuo, I.: Programming with infinitesimals: a while-language for hybrid system modeling. In L.\u00a0Aceto, M.\u00a0Henzinger and J.\u00a0Sgall, editors, ICALP (2), of Lect. Notes Comp. Sci., vol. 6756, pp. 392\u2013403. Springer (2011)","DOI":"10.1007\/978-3-642-22012-8_31"},{"key":"23_CR79","doi-asserted-by":"crossref","unstructured":"Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard modeling of continuous-time signals. In Giacobazzi and Cousot [32], pp. 417\u2013430","DOI":"10.1145\/2480359.2429120"},{"key":"23_CR80","doi-asserted-by":"crossref","unstructured":"Tedrake, R.: Convex and combinatorial optimization for dynamic robots in the real world. In Frehse and Mitra [30], p. 141","DOI":"10.1145\/3049797.3049803"},{"key":"23_CR81","doi-asserted-by":"crossref","unstructured":"Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Logic in Computer Science, pp. 280\u2013291. IEEE, Computer Science Press (1997)","DOI":"10.1109\/LICS.1997.614955"},{"key":"23_CR82","doi-asserted-by":"crossref","unstructured":"Ulus, D., Ferr\u00e8re, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In Chechik and Raskin [18], pp. 736\u2013751","DOI":"10.1007\/978-3-662-49674-9_47"},{"key":"23_CR83","doi-asserted-by":"crossref","unstructured":"Urabe, N., Hara, M., Hasuo, I.: Categorical liveness checking by corecursive algebras. In: Proc. LICS 2017. To appear (2017)","DOI":"10.1109\/LICS.2017.8005151"},{"key":"23_CR84","doi-asserted-by":"crossref","unstructured":"Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In P.\u00a0Baldan and D.\u00a0Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2\u20135, 2014. Proceedings of Lecture Notes in Computer Science, vol. 8704, pp. 451\u2013466. Springer. Best paper award (2014)","DOI":"10.1007\/978-3-662-44584-6_31"},{"key":"23_CR85","unstructured":"Urabe, N., Hasuo, I.: Coalgebraic infinite traces and kleisli simulations. In: Moss, L.S., Sobocinski, P. (eds) 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands, of LIPIcs, vol.\u00a035, pp. 320\u2013335. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik (2015)"},{"key":"23_CR86","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.ic.2016.03.007","volume":"252","author":"N Urabe","year":"2017","unstructured":"Urabe, N., Hasuo, I.: Quantitative simulations by matrices. Inf. Comput. 252, 110\u2013137 (2017)","journal-title":"Inf. Comput."},{"key":"23_CR87","unstructured":"Urabe, N., Shimizu, S., Hasuo, I.: Coalgebraic trace semantics for buechi and parity automata. In: Desharnais, J., Jagadeesan, R. (eds) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada, of LIPIcs, vol.\u00a059, pp. 24:1\u201324:15. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik (2016)"},{"key":"23_CR88","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G.M. (eds) Banff Higher Order Workshop of Lecture Notes in Computer Science, vol. 1043, pp. 238\u2013266. Springer (1995)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"23_CR89","doi-asserted-by":"crossref","unstructured":"Vijayaraghavan, M., Chlipala, A., Dave, N.: Modular deductive verification of multiprocessor hardware designs. In Kroening and Pasareanu [60], pp. 109\u2013127","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"23_CR90","doi-asserted-by":"crossref","unstructured":"Vitus, M.P., Zhang, W., Tomlin, C.J.: A hierarchical method for stochastic motion planning in uncertain environments. In: 2012 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 2263\u20132268 (2012)","DOI":"10.1109\/IROS.2012.6385724"},{"key":"23_CR91","doi-asserted-by":"crossref","unstructured":"Waga, M., Akazaki, T., Hasuo, I.: A boyer-moore type algorithm for timed pattern matching. In M.\u00a0Fr\u00e4nzle and N.\u00a0Markey, editors, Formal Modeling and Analysis of Timed Systems, 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings of Lecture Notes in Computer Science, vol. 9884, pp. 121\u2013139. Springer (2016)","DOI":"10.1007\/978-3-319-44878-7_8"},{"issue":"2","key":"23_CR92","doi-asserted-by":"crossref","first-page":"359","DOI":"10.36045\/bbms\/1102714178","volume":"8","author":"T Wilke","year":"2001","unstructured":"Wilke, T.: Alternating tree automata, parity games, and modal \u03bc-calculus. Bull. Belg. Math. Soc. Simon Stevin 8(2), 359\u2013391 (2001)","journal-title":"Bull. Belg. Math. Soc. Simon Stevin"},{"key":"23_CR93","doi-asserted-by":"crossref","unstructured":"G.\u00a0Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"23_CR94","unstructured":"Yamaguchi, T., Kaga, T., Donz\u00e9, A., Seshia, S.A..: Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3\u20136, 2016, pp. 201\u2013204. IEEE (2016)"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00354-017-0023-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-017-0023-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-017-0023-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T23:05:56Z","timestamp":1750633556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00354-017-0023-1"}},"subtitle":["Comprehensive Transfer of Formal Methods Techniques to Cyber-Physical Systems"],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":94,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["23"],"URL":"https:\/\/doi.org\/10.1007\/s00354-017-0023-1","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7]]},"assertion":[{"value":"25 May 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 June 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 July 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}