{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T10:11:50Z","timestamp":1777111910846,"version":"3.51.4"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"unspecified","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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10703-017-0277-8","type":"journal-article","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T01:49:50Z","timestamp":1491961790000},"page":"117-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["On relative and probabilistic finite counterability"],"prefix":"10.1007","volume":"52","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8201-286X","authenticated-orcid":false,"given":"Gal","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,12]]},"reference":[{"key":"277_CR1","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-319-07317-0_3","volume-title":"Formal methods for executable software models","author":"E \u00c1brah\u00e1m","year":"2014","unstructured":"\u00c1brah\u00e1m E, Becker B, Dehnert C, Jansen N, Katoen JP, Wimmer R (2014) Counterexample generation for discrete-time markov models: an introductory survey. In: Bernardo M, Damiani F, H\u00e4hnle R, Johnsen EB, Schaefer I (eds) Formal methods for executable software models. Springer, Berlin, pp 65\u2013121"},{"key":"277_CR2","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 FB (1985) Defining liveness. Inf Process Lett 21:181\u2013185","journal-title":"Inf Process Lett"},{"key":"277_CR3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2:117\u2013126","journal-title":"Distrib Comput"},{"issue":"12","key":"277_CR4","doi-asserted-by":"crossref","first-page":"680","DOI":"10.1016\/j.ipl.2014.06.005","volume":"114","author":"DA Basin","year":"2014","unstructured":"Basin DA, Jim\u00e9nez CC, Klaedtke F, Zalinescu E (2014) Deciding safety and liveness in TPTL. Inf Process Lett 114(12):680\u2013688","journal-title":"Inf Process Lett"},{"key":"277_CR5","doi-asserted-by":"crossref","unstructured":"Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: Proceedings of 7th international workshop on formal methods for industrial critical systems, volume 66:2 of Electronic Notes in Theoretical Computuer Science","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"277_CR6","unstructured":"B\u00fcchi JR (1962) On a decision method in restricted second order arithmetic. In: Proceedings of international congress on logic, method, and philosophy of science, 1960. Stanford University Press, pp 1\u201312"},{"issue":"1","key":"277_CR7","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1):7\u201334","journal-title":"Form Methods Syst Des"},{"key":"277_CR8","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of 12th international conference on computer aided verification, volume 1855 of Lecture Notes in Computer Science. Springer, Berlin, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"277_CR9","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, McMillan KL, Zhao X (1995) Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proceedings of 32st design automation conference. IEEE Computer Society, pp 427\u2013432","DOI":"10.1145\/217474.217565"},{"key":"277_CR10","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"1990","unstructured":"Cormen TH, Leiserson CE (1990) Introduction to algorithms. MIT Press and McGraw-Hill, Cambridge"},{"key":"277_CR11","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42:857\u2013907","journal-title":"J ACM"},{"key":"277_CR12","doi-asserted-by":"crossref","unstructured":"Couvreur JM, Saheb N, Sutre G (2003) An optimal automata approach to LTL model checking of probabilistic systems. In: Proceedings 10th international conference on logic for programming artificial intelligence and reasoning. Springer, Berlin, pp 361\u2013375","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"277_CR13","unstructured":"David BS, Kupferman O (2013) A framework for ranking vacuity results. 11th international symposium on automated technology for verification and analysis, volume 8172 of Lecture Notes in Computer Science. Springer, Berlin, pp 148\u2013162"},{"key":"277_CR14","doi-asserted-by":"crossref","unstructured":"Diekert V, Muscholl A, Walukiewicz I (2015) A note on monitors and b\u00fcchi automata. In: 12th international colloquium cali, vol 9399, pp 39\u201357","DOI":"10.1007\/978-3-319-25150-9_3"},{"key":"277_CR15","doi-asserted-by":"crossref","unstructured":"Faran R, Kupferman O (2015) Spanning the spectrum from safety to liveness. International symposium on automated technology for verification and analysis. Springer, pp 183\u2013200","DOI":"10.1007\/978-3-319-24953-7_13"},{"key":"277_CR16","doi-asserted-by":"crossref","unstructured":"Gabbay D, Pnueli A, Shelah S, Stavi J (1980) On the temporal analysis of fairness. In: Proceedings of 7th ACM symposium on principles of programming languages, pp 163\u2013173","DOI":"10.1145\/567446.567462"},{"key":"277_CR17","unstructured":"Grinstead CM, Snell JL (2003) Introduction to probability, 2nd edn. American Mathematical Society, Rhode Island"},{"issue":"2","key":"277_CR18","first-page":"18","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund K, Rosu G (2004) Efficient monitoring of safety properties. Softw Tools Technol Transf 6(2):18\u2013173","journal-title":"Softw Tools Technol Transf"},{"key":"277_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Kupferman O, Qadeer S (1998) From pre-historic to post-modern symbolic model checking. In: Proceedings of 10th international conference on computer aided verification, volume 1427 of Lecture Notes in Computer Science. Springer, Berlin","DOI":"10.1007\/BFb0028745"},{"issue":"3","key":"277_CR20","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0020-0190(92)90005-G","volume":"43","author":"TA Henzinger","year":"1992","unstructured":"Henzinger TA (1992) Sooner is safer than later. Inf Process Lett 43(3):135\u2013141","journal-title":"Inf Process Lett"},{"key":"277_CR21","doi-asserted-by":"crossref","unstructured":"Katoen J-P, Song L, Zhang L (2014) Probably safe or live. In: Proceedings of 29th IEEE symposium on logic in computer science, pp 55:1\u201355:10","DOI":"10.1145\/2603088.2603147"},{"key":"277_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains","author":"JG Kemeny","year":"1976","unstructured":"Kemeny JG, Snell JL, Knapp AW (1976) Denumerable Markov chains. Springer, Berlin"},{"key":"277_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman O, Lampert R (2006) On the construction of fine automata for safety properties. In: 4th international symposium on automated technology for verification and analysis, volume 4218 of Lecture Notes in Computer Science. Springer, Berlin, pp 110\u2013124","DOI":"10.1007\/11901914_11"},{"key":"277_CR24","doi-asserted-by":"crossref","unstructured":"Kupferman O, Sheinvald-Faragy S (2006) Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Proceedings of 17th international conference on concurrency theory, volume 4137 of Lecture Notes in Computer Science. Springer, Berlin, pp 492\u2013508","DOI":"10.1007\/11817949_33"},{"issue":"3","key":"277_CR25","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291\u2013314","journal-title":"Form Methods Syst Des"},{"key":"277_CR26","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2004) From complementation to certification. In: Proceedings of 10th international conference on tools and algorithms for the construction and analysis of systems, volume 2988 of Lecture Notes in Computer Science. Springer, Berlin, pp 591\u2013606","DOI":"10.1007\/978-3-540-24730-2_43"},{"key":"277_CR27","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2010) Synthesis of trigger properties. In: Proceedings of 16th international conference on logic for programming artificial intelligence and reasoning, volume 6355 of Lecture Notes in Computer Science. Springer, Berlin, pp 312\u2013331","DOI":"10.1007\/978-3-642-17511-4_18"},{"key":"277_CR28","unstructured":"Lippmann M (2014) Temporalised description logics for monitoring partially observable events. PhD thesis, TU Dresden"},{"key":"277_CR29","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z Manna","year":"1984","unstructured":"Manna Z, Pnueli A (1984) Adequate proof principles for invariance and liveness properties of concurrent programs. Sci Comput Program 4:257\u2013289","journal-title":"Sci Comput Program"},{"key":"277_CR30","doi-asserted-by":"crossref","unstructured":"Meyer AR, Stockmeyer LJ (1972) The equivalence problem for regular expressions with squaring requires exponential time. In: Proceedings of 13th IEEE symposium on switching and automata theory, pp 125\u2013129","DOI":"10.1109\/SWAT.1972.29"},{"key":"277_CR31","unstructured":"Nitsche U, Wolper P (1997) Relative liveness and behavior abstraction. In: Proceedings of 24th ACM symposium on principles of programming languages. ACM, New York, pp 45\u201352"},{"issue":"3","key":"277_CR32","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"Owicki S, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4(3):455\u2013495","journal-title":"ACM Trans Program Lang Syst"},{"issue":"3","key":"277_CR33","doi-asserted-by":"crossref","first-page":"5","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman N (2007) From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log Methods Comput Sci 3(3):5","journal-title":"Log Methods Comput Sci"},{"key":"277_CR34","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli A (1981) The temporal semantics of concurrent programs. Theor Comput Sci 13:45\u201360","journal-title":"Theor Comput Sci"},{"key":"277_CR35","doi-asserted-by":"crossref","unstructured":"Schuppan V, Biere A (2005) Shortest counterexamples for symbolic model checking of LTL with past. In: Proceedings of 11th international conference on tools and algorithms for the construction and analysis of systems, volume 3440 of Lecture Notes in Computer Science. Springer, Berlin, pp 493\u2013509","DOI":"10.1007\/978-3-540-31980-1_32"},{"issue":"1","key":"277_CR36","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.entcs.2005.11.018","volume":"149","author":"V Schuppan","year":"2006","unstructured":"Schuppan V, Biere A (2006) Liveness checking as safety checking for infinite state spaces. Electron Notes Theor Comput Sci 149(1):79\u201396","journal-title":"Electron Notes Theor Comput Sci"},{"key":"277_CR37","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla AP (1994) Safety, liveness and fairness in temporal logic. Form Aspects Comput 6:495\u2013511","journal-title":"Form Aspects Comput"},{"key":"277_CR38","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logic. J ACM 32:733\u2013749","journal-title":"J ACM"},{"key":"277_CR39","unstructured":"van Emde Boas P (1997) The convenience of tilings. Lecture Notes on Pure and Applied Mathematics, pp 331\u2013363"},{"key":"277_CR40","doi-asserted-by":"crossref","unstructured":"Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of 26th IEEE symposium on foundations of computer science, pp 327\u2013338","DOI":"10.1109\/SFCS.1985.12"},{"issue":"1","key":"277_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0277-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0277-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0277-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,3,20]],"date-time":"2018-03-20T07:56:58Z","timestamp":1521532618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0277-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,12]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["277"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0277-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,12]]}}}