{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T20:40:08Z","timestamp":1736109608091,"version":"3.32.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":21,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019021X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0026107","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:47:21Z","timestamp":1132645641000},"page":"231-243","source":"Crossref","is-referenced-by-count":0,"title":["Regular automata and model checking"],"prefix":"10.1007","author":[{"given":"Z.","family":"Habasi\u0144ski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Arnold A. Crubille P. A linear algorithm to solve fixed-point equations on graphs, Rep. I-8632, Univ. de Bordeaux I."},{"key":"16_CR2","unstructured":"Browne M.C. An improved algorithm for the automatic verification of finite state systems using temporal logic, Rep. CMU-CS-86-156, Carnegie-Mellon Univ."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Clarke E.M. Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic, LNCS 131,:52\u201371.","DOI":"10.1007\/BFb0025774"},{"key":"16_CR4","unstructured":"Clarke E.M. Emerson E.A. Sistla A.P. Automatic verification of finite state concurrent systems using temporal logic specifications, POPL-Symp.,:117\u2013126; see also ACM Tran. on Prog. Lang. and Systems 8(2):244\u2013263, 1986."},{"key":"16_CR5","unstructured":"Clarke E.M., Grumberg O., Kurshan R.P. A synthesis of two approaches for verifying finite state concurrent systems, Report of the Carnegie Mellon Univ., 1987."},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Emerson E.A. Clarke M. Using branching time temporal logic to synthesize synchronization skeletons, Sci. of Comp. Programming 2,:241\u2013266.","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Emerson E.A. Lei Ch-L. Modalities for model checking: branching time strickes back, POPL-Symp.,:84\u201396.","DOI":"10.1145\/318593.318620"},{"key":"16_CR8","unstructured":"Emerson E.A. Lei Ch-L. Temporal model checking under generalized fairness constraints, Hawaii Int. Conf. System Sci.,1985."},{"key":"16_CR9","unstructured":"Floyd R.W. Assigning meaning to programs, Proc. of Symp. in Applied Math.XIX, Am. Math. Soc."},{"key":"16_CR10","unstructured":"Hailpern B. T. Verifying concurrent processes using temporal logic, LNCS 129."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Habasinski Z. Process logics: two decidability results, LNCS 176,:282\u2013290.","DOI":"10.1007\/BFb0030309"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Hoare C.A.R. The axiomatic basis of computer programming, Comm. of ACM 12,:576\u2013583.","DOI":"10.1145\/363235.363259"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Kozen D. Results on the propositional Mu-calculus, Th. Comput. Sci. 27,:333\u2013354.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Lamport L. Specifying concurrent modules, TOPLAS 5(2),:190\u2013222.","DOI":"10.1145\/69624.357207"},{"key":"16_CR15","unstructured":"Michel M. Algebre de machines et logique temporelle, LNCS 166, Proc. of STACS."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Manna Z. Pnueli A. Axiomatic approach to total correctness of programs, Acta Informatica 3.","DOI":"10.1007\/BF00288637"},{"key":"16_CR17","unstructured":"Quielle J.P. Sifakis J. Specification of concurrent systems in CESAR, Proc. of the 5th Int. Symp. in Programming."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Salwicki A. Muldner T. On the algorithmic properties of concurrent programs, LNCS 125,:169\u2013197.","DOI":"10.1007\/3-540-11160-3_6"},{"key":"16_CR19","unstructured":"Wolper P. Synthesis of Communicating Processes from temporal logic specifications, Ph.D.Thesis,Stanford Univ.,California."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Wolper P. Expressing interesting properties of programs in propositional temporal logic, POPL-Symp.,1986.","DOI":"10.1145\/512644.512661"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Wolper P. Vardi M.Y. Sistla A.P. Reasoning about infinite computation paths, FOCS-Symp.,:185\u2013194.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","CAAP '88"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026107.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T20:08:12Z","timestamp":1736107692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019021X"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0026107","relation":{},"subject":[]}}