{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:28:42Z","timestamp":1707521322522},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,4,16]],"date-time":"2014-04-16T00:00:00Z","timestamp":1397606400000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10009-014-0312-7","type":"journal-article","created":{"date-parts":[[2014,4,15]],"date-time":"2014-04-15T09:51:22Z","timestamp":1397555482000},"page":"223-243","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model-checking fair dense-time systems with propositions and events"],"prefix":"10.1007","volume":"17","author":[{"given":"Farn","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,4,16]]},"reference":[{"key":"312_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Burgueno, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.), 4th TACAS, volume LNCS 1384, pp. 263\u2013280 (1998)","DOI":"10.1007\/BFb0054177"},{"issue":"1","key":"312_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"312_CR3","doi-asserted-by":"crossref","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, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"312_CR4","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"312_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. In: 30th IEEE FOCS, pp. 164\u2013169 (1989)","DOI":"10.1109\/SFCS.1989.63473"},{"key":"312_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Real Time: Theory in Practice, volume LNCS 600, pp. 74\u2013106. Springer, Berlin (1992)","DOI":"10.1007\/BFb0031988"},{"key":"312_CR7","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104, 35\u201377 (1993)","journal-title":"Inf. Comput."},{"issue":"5","key":"312_CR8","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s00236-003-0135-6","volume":"40","author":"R Barbuti","year":"2004","unstructured":"Barbuti, R., Tesei, L.: Timed automata with urgent transitions. Acta Inf 40(5), 317\u2013347 (2004)","journal-title":"Acta Inf"},{"key":"312_CR9","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"312_CR10","unstructured":"Burch, J., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. In: IEEE LICS (1990)"},{"key":"312_CR11","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: IFM, volume LNCS 2999. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"312_CR12","volume-title":"Parallel Program Design-A Foundation","author":"KM Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design-A Foundation. Addison-Wesley, Reading (1988)"},{"key":"312_CR13","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on Logic of Programs, volume LNCS 131. Springer, Berlin (1981)"},{"key":"312_CR14","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Conference on Computer Aided Verification (CAV), volume LNCS 407. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"issue":"1","key":"312_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"312_CR16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u2018sometimes\u2019 and \u2018not never\u2019 revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"312_CR17","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8, 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"312_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation, 111, 193\u2013244 (a preliminary version appeared in the Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, pp. 394\u2013406 (1992)) (1994)","DOI":"10.1006\/inco.1994.1045"},{"key":"312_CR19","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: ESOP, volume LNCS 2028. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45309-1_11"},{"key":"312_CR20","doi-asserted-by":"crossref","unstructured":"Jensen, H.E., Larsen, K.G., Skou, A.: Modelling and analysis of a collision avoidance protocol using spin and uppaal. In: 2nd SPIN, Workshop (1996)","DOI":"10.7146\/brics.v3i24.20005"},{"key":"312_CR21","doi-asserted-by":"crossref","unstructured":"Kindler, E., Vesper, T.: Estl: A temporal logic for events and states. In: ATPN, volume LNCS 1420. Springer, Berlin (1998)","DOI":"10.1007\/3-540-69108-1_20"},{"key":"312_CR22","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"312_CR23","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"RD Nicola","year":"1995","unstructured":"Nicola, R.D., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"312_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual IEEE-CS Symposium on Foundations of Computer, Science, pp. 45\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"312_CR25","doi-asserted-by":"crossref","unstructured":"Shaw, A.: Communicating real-time state machines. IEEE Trans. Softw. Eng., 18(9) (1992)","DOI":"10.1109\/32.159840"},{"key":"312_CR26","volume-title":"Operating System Principles","author":"A Silberschatz","year":"2004","unstructured":"Silberschatz, A., Gagne, G., Galvin, P.B.: Operating System Principles, 7th edn. Wiley, London (2004)","edition":"7"},{"key":"312_CR27","doi-asserted-by":"crossref","unstructured":"Wang, F.: Efficient data-structure for fully symbolic verification of real-time software systems. In: TACAS, volume LNCS 1785. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_12"},{"key":"312_CR28","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data-structures. In. J. Softw. Tools Technol. Transf., 6(1) (special issue for the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan. 2003, LNCS 2575, Springer, Berlin) (2004)"},{"key":"312_CR29","doi-asserted-by":"crossref","unstructured":"Wang, F.: Efficient model-checking of dense-time systems with time-convexity analysis. In: IEEE Real-Time System Symposium (RTSS). IEEE Computer Society (2008)","DOI":"10.1109\/RTSS.2008.53"},{"key":"312_CR30","doi-asserted-by":"crossref","unstructured":"Wang, F.: Time-progress evaluation for dense-time automata with concave path conditions. In: Automated Technology for Verification and Analysis (ATVA), volume LNCS 5311. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88387-6_24"},{"key":"312_CR31","unstructured":"Wang, F.: Red: Model-checker for timed automata with clock-restriction diagram. In: Workshop on Real-Time Tools. Dept. of Information Technology, Uppsala University, August 2001. Technical Report 2001\u2013014, ISSN 1404\u20133203 (2001)"},{"key":"312_CR32","unstructured":"Wang, F.: Symbolic verification of complex real-time systems with clock-restriction diagram. In: FORTE (2001)"},{"key":"312_CR33","unstructured":"Wang, F.: Region encoding diagram for fully symbolic verification of real-time systems. In: The 24th COMPSAC. IEEE press (2000)"},{"key":"312_CR34","unstructured":"Wang, F., Hsiung, P.-A.: Efficient and user-friendly verification. IEEE Trans. Comput. (2002)"},{"key":"312_CR35","unstructured":"Wang, F., Huang, G.-D., Yu, F.: TCTL inevitability analysis of dense-time systems: from theory to engineering. IEEE Trans. Softw. Eng., 32(7) (a preliminary version of the work appears in the proceedings of 8th Conference on Implementation and Application of Automata (CIAA), July 2003, Santa Barbara, CA, USA; LNCS 2759, Springer, Berlin) (2006)"},{"issue":"4","key":"312_CR36","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/s11241-011-9122-0","volume":"47","author":"F Wang","year":"2011","unstructured":"Wang, F., Yao, L.-W., Yang, Y.-L.: Efficient verification of distributed real-time systems with broadcasting behaviors. Real Time Syst. J. 47(4), 285\u2013318 (2011)","journal-title":"Real Time Syst. J."},{"key":"312_CR37","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf., 1(1\/2) (1997)","DOI":"10.1007\/s100090050009"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0312-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0312-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0312-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T17:32:29Z","timestamp":1648834349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0312-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,16]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["312"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0312-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,16]]}}}