{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:24:05Z","timestamp":1725791045363},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_1","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:33:34Z","timestamp":1395408814000},"page":"1-14","source":"Crossref","is-referenced-by-count":0,"title":["Variations on Safety"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. IPL\u00a021, 181\u2013185 (1985)","journal-title":"IPL"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing\u00a02, 117\u2013126 (1987)","journal-title":"Distributed Computing"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 279\u2013290. Springer, Heidelberg (1997)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-40922-X_4","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Bloem","year":"2000","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n logn symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 37\u201354. Springer, Heidelberg (2000)"},{"key":"1_CR7","first-page":"275","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. FMSD\u00a01, 275\u2013288 (1992)","journal-title":"FMSD"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM\u00a042, 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M. d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of omega-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 364\u2013378. Springer, Heidelberg (2005)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-02444-8_12","volume-title":"Automated Technology for Verification and Analysis","author":"S. Ben-David","year":"2013","unstructured":"Ben-David, S., Kupferman, O.: A framework for ranking vacuity results. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol.\u00a08172, pp. 148\u2013162. Springer, Heidelberg (2013)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Ehlers, R., Finkbeiner, B.: Reactive safety. In: Proc. 2nd GANDALF. Electronic Proceedings in TCS, vol.\u00a054, pp. 178\u2013191 (2011)","DOI":"10.4204\/EPTCS.54.13"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"Emerson, E.A.: Alternative semantics for temporal logics. TCS\u00a026, 121\u2013130 (1983)","journal-title":"TCS"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"50","DOI":"10.2307\/2272945","volume":"41","author":"R. Fagin","year":"1976","unstructured":"Fagin, R.: Probabilities in finite models. Journal of Symb. Logic\u00a041(1), 50\u201358 (1976)","journal-title":"Journal of Symb. Logic"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"1_CR15","first-page":"245","volume":"28","author":"D. Gale","year":"1953","unstructured":"Gale, D., Stewart, F.M.: Infinite games of perfect information. Ann. Math. Studies\u00a028, 245\u2013266 (1953)","journal-title":"Ann. Math. Studies"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-70583-3_30","volume-title":"Automata, Languages and Programming","author":"K. Greimel","year":"2008","unstructured":"Greimel, K., Bloem, R., Jobstmann, B., Vardi, M.: Open implication. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 361\u2013372. Springer, Heidelberg (2008)"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0020-0190(93)90074-J","volume":"47","author":"H.P. Gumm","year":"1993","unstructured":"Gumm, H.P.: Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. IPL\u00a047, 291\u2013294 (1993)","journal-title":"IPL"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Harel, D., Katz, G., Marron, A., Weiss, G.: Non-intrusive repair of reactive programs. In: ICECCS, pp. 3\u201312 (2012)","DOI":"10.1109\/ICECCS20050.2012.6299199"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems, NATO ASI, vol.\u00a0F-13, pp. 477\u2013498. Springer (1985)","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"1_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/11916277_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Lustig, Y., Vardi, M.Y.: On locally checkable properties. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 302\u2013316. Springer, Heidelberg (2006)"},{"key":"1_CR22","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)"},{"issue":"3","key":"1_CR23","first-page":"291","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. FMSD\u00a019(3), 291\u2013314 (2001)","journal-title":"FMSD"},{"key":"1_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 24\u201338. Springer, Heidelberg (2001)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-39611-3_22","volume-title":"Hardware and Software: Verification and Testing","author":"O. Kupferman","year":"2013","unstructured":"Kupferman, O., Weiner, S.: Environment-friendly safety. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol.\u00a07857, pp. 227\u2013242. Springer, Heidelberg (2013)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","first-page":"19","volume-title":"Distributed Systems","author":"L. Lamport","year":"1985","unstructured":"Lamport, L.: Logical foundation. In: Alford, M.W., Hommel, G., Schneider, F.B., Ansart, J.P., Lamport, L., Mullery, G.P., Zhou, T.H. (eds.) Distributed Systems. LNCS, vol.\u00a0190, pp. 19\u201330. Springer, Heidelberg (1985)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0013024","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"Z. Manna","year":"1989","unstructured":"Manna, Z., Pnueli, A.: he anchored version of the temporal framework. 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. 201\u2013284. Springer, Heidelberg (1989)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"1_CR29","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer (1995)"},{"key":"1_CR30","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.: The temporal semantics of concurrent programs. TCS\u00a013, 45\u201360 (1981)","journal-title":"TCS"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2000","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 328\u2013343. Springer, Heidelberg (2000)"},{"key":"1_CR33","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"1_CR34","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM\u00a032, 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"issue":"1","key":"1_CR35","first-page":"101","volume":"118","author":"H.J. Touati","year":"1995","unstructured":"Touati, H.J., Brayton, R.K., Kurshan, R.: Testing language containment for \u03c9-automata using BDD\u2019s. I & C\u00a0118(1), 101\u2013109 (1995)","journal-title":"I & C"},{"issue":"1","key":"1_CR36","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I & C\u00a0115(1), 1\u201337 (1994)","journal-title":"I & C"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,16]],"date-time":"2020-08-16T16:34:45Z","timestamp":1597595685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}