{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T04:13:36Z","timestamp":1750997616018,"version":"3.41.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2017,10,23]],"date-time":"2017-10-23T00:00:00Z","timestamp":1508716800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["278410"],"award-info":[{"award-number":["278410"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s00236-017-0307-4","type":"journal-article","created":{"date-parts":[[2017,10,23]],"date-time":"2017-10-23T22:37:05Z","timestamp":1508798225000},"page":"703-732","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Spanning the spectrum from safety to liveness"],"prefix":"10.1007","volume":"55","author":[{"given":"Rachel","family":"Faran","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4699-6117","authenticated-orcid":false,"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,23]]},"reference":[{"key":"307_CR1","doi-asserted-by":"crossref","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. Inf. Process. Lett. 21, 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"307_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2, 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"307_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1579. Springer (1999)","DOI":"10.21236\/ADA360973"},{"key":"307_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gabow, H.N., and Somenzi, F.: An algorithm for strongly connected component analysis in $$n \\log n$$ n log n symbolic steps. In: Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1954, pp. 37\u201354. Springer (2000)","DOI":"10.1007\/3-540-40922-X_4"},{"key":"307_CR5","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events. In: Proceedings of the 17th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 443, pp. 336\u2013349. Springer (1990)","DOI":"10.1007\/BFb0032043"},{"key":"307_CR6","doi-asserted-by":"crossref","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 42, 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"307_CR7","doi-asserted-by":"crossref","unstructured":"Ben David, S., Kupferman, O.: A framework for ranking vacuity results. In: 11th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 8172, pp. 148\u2013162. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_12"},{"key":"307_CR8","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"EA Emerson","year":"1983","unstructured":"Emerson, E.A.: Alternative semantics for temporal logics. Theor. Comput. Sci. 26, 121\u2013130 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"307_CR9","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of the 21st International Conference on Computer Aided Verification, vol. 5643, pp. 263\u2013277 (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"307_CR10","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0020-0190(93)90074-J","volume":"47","author":"HP Gumm","year":"1993","unstructured":"Gumm, H.P.: Another glance at the Alpern\u2013Schneider characterization of safety and liveness in concurrent executions. Inf. Process. Lett. 47, 291\u2013294 (1993)","journal-title":"Inf. Process. Lett."},{"key":"307_CR11","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":"307_CR12","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2280, pp. 342\u2013356. Springer (2002)","DOI":"10.1007\/3-540-46002-0_24"},{"key":"307_CR13","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1016\/S0022-0000(75)80050-X","volume":"11","author":"ND Jones","year":"1975","unstructured":"Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68\u201375 (1975)","journal-title":"J. Comput. Syst. Sci."},{"key":"307_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"JG Kemeny","year":"1976","unstructured":"Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. Springer, Berlin (1976)"},{"key":"307_CR15","unstructured":"Kupferman, O., Vardi, G.: On relative and probabilistic finite counterability. In: Proceedings of the 24th Annual Conference of the European Association for Computer Science Logic. Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, pp. 175\u2013192 (2015)"},{"issue":"3","key":"307_CR16","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"307_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: On bounded specifications. In Proceedings of the 8th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 2250, pp. 24\u201338. Springer (2001)","DOI":"10.1007\/3-540-45653-8_2"},{"key":"307_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science, pp. 389\u2013398 (2001)","DOI":"10.1109\/LICS.2001.932514"},{"key":"307_CR19","unstructured":"Lamport, L.: Logical foundation. In: Distributed Systems\u2014Methods and Tools for Specification. Lecture Notes in Computer Science, vol. 190. Springer (1985)"},{"key":"307_CR20","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"LH Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for $$\\omega $$ \u03c9 -automata. Math. Syst. Theory 3, 376\u2013384 (1969)","journal-title":"Math. Syst. Theory"},{"key":"307_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The anchored version of the temporal framework. In: Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science, vol. 345, pp. 201\u2013284. Springer (1989)","DOI":"10.1007\/BFb0013024"},{"key":"307_CR22","doi-asserted-by":"crossref","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, Berlin (1992)"},{"key":"307_CR23","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, Berlin (1995)"},{"key":"307_CR24","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential time. In: Proceedings of the 13th IEEE Symposium on Switching and Automata Theory, pp. 125\u2013129 (1972)","DOI":"10.1109\/SWAT.1972.29"},{"key":"307_CR25","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time: preliminary report. In: Proceedings of the 5th ACM Symposium on Theory of Computing, pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"key":"307_CR26","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Proceedings of the 21st IEEE Symposium on Logic in Computer Science, pp. 255\u2013264. IEEE press (2006)","DOI":"10.1109\/LICS.2006.28"},{"key":"307_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Proceedings of the 12th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, pp. 328\u2013343. Springer (2000)","DOI":"10.1007\/10722167_26"},{"key":"307_CR28","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of $$\\omega $$ \u03c9 -automata. In: Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"307_CR29","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Form. Asp. Comput. 6, 495\u2013511 (1994)","journal-title":"Form. Asp. Comput."},{"key":"307_CR30","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"2","key":"307_CR31","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"307_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-017-0307-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0307-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0307-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T17:56:11Z","timestamp":1750960571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-017-0307-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,23]]},"references-count":32,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["307"],"URL":"https:\/\/doi.org\/10.1007\/s00236-017-0307-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2017,10,23]]}}}