{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:01:35Z","timestamp":1725544895798},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540326045"},{"type":"electronic","value":"9783540326052"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11678779_2","type":"book-chapter","created":{"date-parts":[[2006,3,2]],"date-time":"2006-03-02T08:03:26Z","timestamp":1141286606000},"page":"14-29","source":"Crossref","is-referenced-by-count":5,"title":["The Safety Simple Subset"],"prefix":"10.1007","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Dana","family":"Fisman","sequence":"additional","affiliation":[]},{"given":"Sitvanit","family":"Ruah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 184\u2013194. Springer, Heidelberg (1998)"},{"key":"2_CR2","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Automata construction for regular expressions in model checking, IBM research report H-0229 (June 2004)"},{"volume-title":"1st International Symposium on Leveraging Applications of Formal Methods","year":"2004","author":"S. Ben David","key":"2_CR3","unstructured":"Ben David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. In: 1st International Symposium on Leveraging Applications of Formal Methods. Springer, Heidelberg (2004)"},{"key":"2_CR4","unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science (May 2005)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/BFb0013029","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"E.M. Clarke","year":"1989","unstructured":"Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 428\u2013437. Springer, Heidelberg (1989)"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/800119.803886","volume-title":"STOC 1974: Proceedings of the sixth annual ACM symposium on Theory of computing","author":"A. Ehrenfeucht","year":"1974","unstructured":"Ehrenfeucht, A., Zeiger, P.: Complexity measures for regular expressions. In: STOC 1974: Proceedings of the sixth annual ACM symposium on Theory of computing, pp. 75\u201379. ACM Press, New York (1974)"},{"key":"2_CR7","first-page":"1","volume-title":"PODC 2005: Proceedings of the twenty-fourth annual ACM SIGACT-SIGOPS symposium on Principles of distributed computing","author":"C. Eisner","year":"2005","unstructured":"Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: PODC 2005: Proceedings of the twenty-fourth annual ACM SIGACT-SIGOPS symposium on Principles of distributed computing, pp. 1\u20138. ACM Press, New York (2005)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201340. Springer, Heidelberg (2003)"},{"issue":"2","key":"2_CR9","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci.,\u00a018(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci.,"},{"volume-title":"Introduction to Automata Theory, Languages, and Computation","year":"1979","author":"J.E. Hopcroft","key":"2_CR10","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"2_CR11","unstructured":"IEEE. IEEE standard for property specification language (PSL) (October 2005)"},{"key":"2_CR12","unstructured":"Kargl, C.J.: A Sugar translator. Master\u2019s thesis, Institut f\u00fcr Softwaretechnologie, Technische Univesit\u00e4at Graz, Graz, Austria (December 2003)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications, vol.\u00a01443, pp. 1\u201316 (1998)","DOI":"10.1007\/BFb0055036"},{"key":"2_CR14","unstructured":"Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: From linear-time to branching-time. In: Proc. 13th IEEE Symposium on Logic in Computer Science (June 1995)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 172\u2013183. Springer, Heidelberg (1999)"},{"key":"2_CR16","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: IEEE Symposium on Foundations of Computer Science, pp. 643\u2013652 (2000)"},{"key":"2_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: A temporal logic of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"2_CR19","unstructured":"Ruah, S., Fisman, D., Ben-David, S.: Automata construction for on-the-fly model checking PSL safety simple subset, Research Report H-0234 (June 2005)"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337, 15 (1994)","journal-title":"Information and Computation"},{"issue":"1\/2","key":"2_CR21","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1\/2), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software, Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11678779_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:15:39Z","timestamp":1619493339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11678779_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540326045","9783540326052"],"references-count":21,"URL":"http:\/\/dx.doi.org\/10.1007\/11678779_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}
