{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:59:59Z","timestamp":1743040799116,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642047602"},{"type":"electronic","value":"9783642047619"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04761-9_19","type":"book-chapter","created":{"date-parts":[[2009,10,10]],"date-time":"2009-10-10T06:43:53Z","timestamp":1255157033000},"page":"244-254","source":"Crossref","is-referenced-by-count":4,"title":["Specification Languages for Stutter-Invariant Regular Properties"],"prefix":"10.1007","author":[{"given":"Christian","family":"Dax","sequence":"first","affiliation":[]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"IEEE standard for property specification language (PSL). IEEE Std 1850TM (October 2005)"},{"issue":"2","key":"19_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1008767206905","volume":"18","author":"R. Alur","year":"2001","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state-space exploration. Form. Method. Syst. Des.\u00a018(2), 97\u2013116 (2001)","journal-title":"Form. Method. Syst. Des."},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/3-540-63166-6_53","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Geist, D., Gluhovsky, L., Heyman, T., Landver, A., Paanah, P., Rodeh, Y., Ronin, G., Wolfsthal, Y.: RuleBase: Model checking at IBM. In: Marie, R., Plateau, B., Calzarossa, M.C., Rubino, G.J. (eds.) TOOLS 1997. LNCS, vol.\u00a01245, pp. 480\u2013483. Springer, Heidelberg (1997)"},{"key":"19_CR4","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL. Technical report, The Prosyd Project (2005), \n                      http:\/\/www.prosyd.org"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/11817963_21","volume-title":"Computer Aided Verification","author":"D. Bustan","year":"2006","unstructured":"Bustan, D., Havlicek, J.: Some complexity results for SystemVerilog assertions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 205\u2013218. Springer, Heidelberg (2006)"},{"issue":"10","key":"19_CR6","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1109\/TCAD.2008.2003303","volume":"27","author":"A. Cimatti","year":"2008","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Symbolic compilation of PSL. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a027(10), 1737\u20131750 (2008)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Dax, C., Klaedtke, F., Lange, M.: On regular temporal logics with past. In: Proceedings of the 36th International Colloquium on Automata, Languages, and Programming, ICALP (to appear, 2009)","DOI":"10.1007\/978-3-642-02930-1_15"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering (ICSE), pp. 411\u2013420 (1999), \n                      http:\/\/patterns.projects.cis.ksu.edu\/","DOI":"10.1145\/302405.302672"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-48683-6_22","volume-title":"Computer Aided Verification","author":"K. Etessami","year":"1999","unstructured":"Etessami, K.: Stutter-invariant languages, \u03c9-automata, and temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 236\u2013248. Springer, Heidelberg (1999)"},{"issue":"6","key":"19_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0020-0190(00)00113-7","volume":"75","author":"K. Etessami","year":"2000","unstructured":"Etessami, K.: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Inform. Process. Lett.\u00a075(6), 261\u2013263 (2000)","journal-title":"Inform. Process. Lett."},{"issue":"2","key":"19_CR11","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput.\u00a0110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"key":"19_CR12","unstructured":"Holzmann, G., Kupferman, O.: Not checking for closure under stuttering. In: Proceedings of the 2nd International Workshop on the SPIN Verification System. Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a032, pp. 163\u2013169 (1996)"},{"key":"19_CR13","unstructured":"Lamport, L.: What good is temporal logic? In: Proceedings of the 9th IFIP World Computer Congress. Information Processing, vol.\u00a083, pp. 657\u2013668 (1983)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-74407-8_7","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"M. Lange","year":"2007","unstructured":"Lange, M.: Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 90\u2013104. Springer, Heidelberg (2007)"},{"issue":"1","key":"19_CR15","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Form. Method. Syst. Des.\u00a08(1), 39\u201364 (1996)","journal-title":"Form. Method. Syst. Des."},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1998","unstructured":"Peled, D.: Ten years of partial order reduction. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 17\u201328. Springer, Heidelberg (1998)"},{"issue":"5","key":"19_CR17","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next operator. Inform. Process. Lett.\u00a063(5), 243\u2013246 (1997)","journal-title":"Inform. Process. Lett."},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(97)00219-3","volume":"195","author":"D. Peled","year":"1998","unstructured":"Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of temporal logic specifications and \u03c9-regular languages. Theoret. Comput. Sci.\u00a0195(2), 183\u2013203 (1998)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BFb0055772","volume-title":"Mathematical Foundations of Computer Science 1998","author":"A.M. Rabinovich","year":"1998","unstructured":"Rabinovich, A.M.: Expressive completeness of temporal logic of action. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, pp. 229\u2013238. Springer, Heidelberg (1998)"},{"issue":"4","key":"19_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Method. Syst. Des.\u00a01(4), 297\u2013322 (1992)","journal-title":"Form. Method. Syst. Des."},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-92701-3_7","volume-title":"Logic and Its Applications","author":"M.Y. Vardi","year":"2009","unstructured":"Vardi, M.Y.: From philosophical to industrial logics. In: Ramanujam, R., Sarukkai, S. (eds.) Logic and Its Applications. LNCS, vol.\u00a05378, pp. 89\u2013115. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04761-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T21:32:34Z","timestamp":1675719154000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-04761-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642047602","9783642047619"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04761-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}