{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T23:53:13Z","timestamp":1656373993970},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,1,15]],"date-time":"2009-01-15T00:00:00Z","timestamp":1231977600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s10626-008-0057-0","type":"journal-article","created":{"date-parts":[[2009,1,14]],"date-time":"2009-01-14T17:41:36Z","timestamp":1231954896000},"page":"103-137","source":"Crossref","is-referenced-by-count":9,"title":["Model Checking for a Class of Weighted Automata"],"prefix":"10.1007","volume":"20","author":[{"given":"Peter","family":"Buchholz","sequence":"first","affiliation":[]},{"given":"Peter","family":"Kemper","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,1,15]]},"reference":[{"key":"57_CR1","volume-title":"The design and analysis of computer algorithms","author":"A Aho","year":"1974","unstructured":"Aho A, Hopcraft J, Ullman J (1974) The design and analysis of computer algorithms. Addison-Wesley, Massachusetts"},{"key":"57_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 (1993) Model-checking in dense real-time. Inf Comput 104:2\u201334","journal-title":"Inf Comput"},{"key":"57_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 DL (1994) A theory of timed automata. Theor Comp Sci 126:183\u2013235","journal-title":"Theor Comp Sci"},{"key":"57_CR4","volume-title":"Synchronization and linearity","author":"F Baccelli","year":"1992","unstructured":"Baccelli F, Cohen, G, Olsder, G, Quadrat J (1992) Synchronization and linearity. Wiley, New York"},{"key":"57_CR5","unstructured":"Baccelli F, Gaujal, B, Simon, D (1999) Analysis of preemptive periodic real time systems using the (max,plus) algebra. Research Report 3778, INRIA"},{"key":"57_CR6","unstructured":"Baccelli F, Hong, D (2000) TCP is (max\/+) linear. In: Proc SIGCOM 2000, ACM"},{"issue":"7","key":"57_CR7","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen JP (2003) Model checking algorithms for continuous time markov chains. IEEE Trans Softw Eng 29(7):524\u2013541","journal-title":"IEEE Trans Softw Eng"},{"issue":"4","key":"57_CR8","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C Baier","year":"2007","unstructured":"Baier C, Cloth L, Kuntz M, Siegle M (2007) Model checking markov chains with actions and state labels. IEEE Trans Softw Eng 33(4):209\u2013224","journal-title":"IEEE Trans Softw Eng"},{"key":"57_CR9","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1007\/s002360050136","volume":"35","author":"D Beauquier","year":"1998","unstructured":"Beauquier D, Slissenko A (1998) Polytime model checking for timed probabilistic computation tree logic. Acta Inform 35:645\u2013664","journal-title":"Acta Inform"},{"key":"57_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and software verification","author":"M Berard","year":"2001","unstructured":"Berard M et al (2001) Systems and software verification. Springer, Berlin"},{"key":"57_CR11","first-page":"3","volume":"158","author":"P Bouyer","year":"2006","unstructured":"Bouyer P (2006) Weighted timed automata: Model checking and games. ENTCS 158:3\u201317","journal-title":"ENTCS"},{"key":"57_CR12","first-page":"277","volume-title":"Proc FORMATS\/FTRTFT, LNCS, vol 3254","author":"T Brihaye","year":"2004","unstructured":"Brihaye T, Bruy\u00e8re V, Raskin JF (2004) Model-checking for weighted timed automata. In: Lakhnech Y, Yovine S (eds) Proc FORMATS\/FTRTFT, LNCS, vol 3254. Springer, Berlin pp 277\u2013292"},{"issue":"4","key":"57_CR13","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1145\/937555.937558","volume":"4","author":"J Bryans","year":"2003","unstructured":"Bryans J, Bowman H, Derrick J (2003) Model checking stochastic automata. ACM Trans Comput Log 4(4):452\u2013492","journal-title":"ACM Trans Comput Log"},{"key":"57_CR14","unstructured":"Buchholz P (1994) Markovian process algebra: composition and equivalence. In: Herzog U, Rettelbach M (eds) Proc 2nd work on process algebras and performance modelling. Arbeitsberichte, des IMMD, University of Erlangen, no. 27, pp 11\u201330"},{"issue":"2","key":"57_CR15","first-page":"93","volume":"15","author":"P Buchholz","year":"2000","unstructured":"Buchholz P (2000) Efficient computation of equivalent and reduced representations for stochastic automata. Int J Comput Syst Sci Eng 15(2):93\u2013103","journal-title":"Int J Comput Syst Sci Eng"},{"issue":"1\u20133","key":"57_CR16","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.tcs.2007.11.018","volume":"393","author":"P Buchholz","year":"2008","unstructured":"Buchholz P (2008) Bisimulation relations for weighted automata. Theor Comp Sci 393(1\u20133):109\u2013123","journal-title":"Theor Comp Sci"},{"key":"57_CR17","first-page":"184","volume-title":"Proc. process algebras and probabilistic methods, LNCS 2165","author":"P Buchholz","year":"2001","unstructured":"Buchholz P, Kemper P (2001) Quantifying the dynamic behavior of process algebras. In: de Alfaro L, Gilmore S (eds) Proc. process algebras and probabilistic methods, LNCS 2165. Springer, Berlin, pp 184\u2013199"},{"key":"57_CR18","unstructured":"Buchholz P, Kemper P (2003a) Model checking for a class of weighted automata. Technical Report 779, TU Dortmund, Fachbereich Informatik"},{"issue":"2","key":"57_CR19","first-page":"187","volume":"8","author":"P Buchholz","year":"2003","unstructured":"Buchholz P, Kemper P (2003b) Weak bisimulation for (max\/+) automata and related models. J Autom Lang Comb 8(2):187\u2013218","journal-title":"J Autom Lang Comb"},{"issue":"2","key":"57_CR20","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"issue":"2","key":"57_CR21","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"issue":"4","key":"57_CR22","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Wing JM et al (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28(4):626\u2013643","journal-title":"ACM Comput Surv"},{"key":"57_CR23","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Massachusetts"},{"issue":"6","key":"57_CR24","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Kurshan R (1996) Computer-aided verification. IEEE Spectrum 33(6):61\u201367","journal-title":"IEEE Spectrum"},{"issue":"1","key":"57_CR25","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/S0004-3702(01)00059-5","volume":"127","author":"P Dasgupta","year":"2001","unstructured":"Dasgupta P, Chakrabarti PP, Deka JK, Sankaranarayanan S (2001) Min\u2013max computation tree logic. Artif Intell 127(1):137\u2013162","journal-title":"Artif Intell"},{"key":"57_CR26","doi-asserted-by":"crossref","unstructured":"Donatelli S, Haddad S, Sproston J (2007) CSL TA : an expressive logic for continuous time markov chains. In: Proc QEST 2007, IEEE","DOI":"10.1109\/QEST.2007.40"},{"key":"57_CR27","unstructured":"Dragan M (2007) Model checking f\u00fcr gewichtete automaten. Master\u2019s thesis, TU Dortmund, Fakult\u00e4t f\u00fcr Informatik (in German)"},{"key":"57_CR28","volume-title":"Automata, languages and machines part A. Pure and applied matematics : a series of monographs and textbook, vol 58","author":"S Eilenberg","year":"1974","unstructured":"Eilenberg S (1974) Automata, languages and machines part A. Pure and applied matematics : a series of monographs and textbook, vol 58. Academic, New York"},{"key":"57_CR29","unstructured":"Eisner J (2001) Expectation semirings: flexible EM for learning finite-state transducers. In: Proc ESSLLI workshop on finite-state methods in NLP"},{"key":"57_CR30","unstructured":"Eisner J (2002) Parameter estimation for probabilistic finite-state transducers. In: Proc 40th annual meeting of the association for computational linguistics (ACL), Philadelphia, July pp 1\u20138"},{"key":"57_CR31","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"EA Emerson","year":"1992","unstructured":"Emerson EA, Mok A, Sistla AP, Srinivasan J (1992) Quantitative temporal reasoning. Real-time Systems, 4:331\u2013352, Kluwer","journal-title":"Real-time Systems"},{"issue":"6","key":"57_CR32","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1145\/358876.358884","volume":"23","author":"JG Fletcher","year":"1980","unstructured":"Fletcher JG (1980) A more general algorithm for computing closed semiring costs between vertices of a directed graph. Commun ACM 23(6):350\u2013351","journal-title":"Commun ACM"},{"issue":"2\/3","key":"57_CR33","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita M, McGeer PC, Chih-Yuan Yang J (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form Methods Syst Des 10(2\/3):149\u2013169","journal-title":"Form Methods Syst Des"},{"issue":"12","key":"57_CR34","doi-asserted-by":"crossref","first-page":"2014","DOI":"10.1109\/9.478227","volume":"40","author":"S Gaubert","year":"1995","unstructured":"Gaubert S (1995) Performance evaluation of (max\/+) automata. IEEE Trans Automat Contr 40(12):2014\u20132025","journal-title":"IEEE Trans Automat Contr"},{"key":"57_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9333-5","volume-title":"Semirings and their applications","author":"JS Golan","year":"1999","unstructured":"Golan JS (1999) Semirings and their applications. Wiley, New York"},{"key":"57_CR36","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6:512\u2013535","journal-title":"Form Asp Comput"},{"key":"57_CR37","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"MC Hennessy","year":"1985","unstructured":"Hennessy MC, Milner R (1985) Algebraic laws for non-determinism and concurrency. J ACM 32:137\u2013161","journal-title":"J ACM"},{"key":"57_CR38","unstructured":"Hillston J (1994) A compositional approach for performance modelling. PhD thesis, University of Edinburgh, Dep of Comp Sc"},{"key":"57_CR39","doi-asserted-by":"crossref","unstructured":"Jiang Z, Litow B, de\u00a0Vel O (2000) Similarity enrichment in image compression through weighted finite automata. In: Du DZ, et al (eds) Proc COCOON 00, LNCS 1858. Springer, pp 447\u2013456","DOI":"10.1007\/3-540-44968-X_44"},{"key":"57_CR40","volume-title":"Finite markov chains","author":"JG Kemeny","year":"1976","unstructured":"Kemeny JG, Snell JL (1976) Finite markov chains. Springer, Berlin"},{"key":"57_CR41","volume-title":"ETACS monographs on theoretical computer science","author":"W Kuich","year":"1986","unstructured":"Kuich W, Salomaa A (1986) Semirings, automata, languages. In: ETACS monographs on theoretical computer science, Springer, Berlin"},{"key":"57_CR42","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01158397","volume":"2","author":"R Lal","year":"1987","unstructured":"Lal R, Bhat UN (1987) Reduced systems in Markov chains and their application to queueing theory. Queueing Syst 2:147\u2013172","journal-title":"Queueing Syst"},{"key":"57_CR43","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inf Comput 94:1\u201328","journal-title":"Inf Comput"},{"key":"57_CR44","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall, New Jersey"},{"issue":"3","key":"57_CR45","first-page":"321","volume":"7","author":"M Mohri","year":"2002","unstructured":"Mohri M (2002) emiring frameworks and algorithms for shortest-distance problems. J Autom Lang Comb 7(3):321\u2013350","journal-title":"J Autom Lang Comb"},{"key":"57_CR46","unstructured":"Mohri M, Pereira F, Riley M (1996) Weighted automata in text and speech processing. In: Kornai A (ed) Proc ECAI 96"},{"key":"57_CR47","first-page":"167","volume-title":"Proc 5th GI conference on theoretical computer science, LNCS 104","author":"D Park","year":"1981","unstructured":"Park D (1981) Concurrency and automata on infinite sequences. In: Proc 5th GI conference on theoretical computer science, LNCS 104. Springer, Berlin, pp 167\u2013183"},{"key":"57_CR48","volume-title":"Introduction to the numerical solution of Markov chains","author":"WJ Stewart","year":"1994","unstructured":"Stewart WJ (1994) Introduction to the numerical solution of Markov chains. Princeton University Press, Princeton"},{"key":"57_CR49","doi-asserted-by":"crossref","unstructured":"van Glabbek R, Smolka S, Steffen B, Tofts C (1990) Reactive, generative and stratified models for probabilistic processes. In: Proc LICS\u201990, pp 130\u2013141","DOI":"10.1109\/LICS.1990.113740"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-008-0057-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-008-0057-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-008-0057-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:58:52Z","timestamp":1559246332000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-008-0057-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,15]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["57"],"URL":"https:\/\/doi.org\/10.1007\/s10626-008-0057-0","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1,15]]}}}