{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:41Z","timestamp":1740099041283,"version":"3.37.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_26","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T10:02:34Z","timestamp":1520676154000},"page":"383-398","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0268-4843","authenticated-orcid":false,"given":"Massimo","family":"Narizzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0258-3222","authenticated-orcid":false,"given":"Luca","family":"Pulina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9487-331X","authenticated-orcid":false,"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6617-2874","authenticated-orcid":false,"given":"Simone","family":"Vuotto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"issue":"2","key":"26_CR2","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44622-2_17","volume-title":"Computer Science Logic","author":"H Comon","year":"2000","unstructured":"Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262\u2013276. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44622-2_17"},{"issue":"3","key":"26_CR4","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., DSouza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"issue":"2","key":"26_CR5","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"LK Dillon","year":"1994","unstructured":"Dillon, L.K., Kutty, G., Moser, L.E., Melliar-Smith, P.M., Ramakrishna, Y.S.: A graphical interval logic for specifying concurrent systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 3(2), 131\u2013165 (1994)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: Metric interval temporal logic specification elicitation and debugging. In: 13th ACM-IEEE International Conference on Formal Methods and Models for Codesign, pp. 21\u201323 (2015)","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: Formal requirement debugging for testing and verification of cyber-physical systems. arXiv preprint arXiv:1607.02549 (2016)","DOI":"10.1145\/3147451"},{"key":"26_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, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 274\u2013278. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_21"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372\u2013381 (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"26_CR11","unstructured":"Li, J., Pu, G., Zhang, L., Yao, Y., Vardi, M.Y., et al.: Polsat: a portfolio LTL satisfiability solver. arXiv preprint arXiv:1311.1602 (2013)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Li, J., Yao, Y., Pu, G., Zhang, L., He, J.: Aalta: an LTL satisfiability checker over infinite\/finite traces. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 731\u2013734 (2014)","DOI":"10.1145\/2635868.2661669"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Li, J., Zhang, L., Pu, G., Vardi, M.Y., He, J.: LTL satisfiability checking revisited. In: 20th International Symposium on Temporal Representation and Reasoning, pp. 91\u201398 (2013)","DOI":"10.1109\/TIME.2013.19"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-26287-1_13","volume-title":"Hardware and Software: Verification and Testing","author":"J Li","year":"2015","unstructured":"Li, J., Zhu, S., Pu, G., Vardi, M.Y.: SAT-based explicit LTL reasoning. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 209\u2013224. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26287-1_13"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Lumpe, M., Meedeniya, I., Grunske, L.: PSPWizard: machine-assisted definition of temporal logical properties with specification patterns. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, pp. 468\u2013471 (2011)","DOI":"10.1145\/2025113.2025193"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Masin, M., Palumbo, F., Myrhaug, H., de Oliveira Filho, J., Pastena, M., Pelcat, M., Raffo, L., Regazzoni, F., Sanchez, A., Toffetti, A., et al.: Cross-layer design of reconfigurable cyber-physical systems. In: 2017 Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 740\u2013745. IEEE (2017)","DOI":"10.23919\/DATE.2017.7927088"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"26_CR18","first-page":"12","volume":"16","author":"A Pnueli","year":"1992","unstructured":"Pnueli, A., Manna, Z.: The temporal logic of reactive and concurrent systems. Springer 16, 12 (1992)","journal-title":"Springer"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-27705-4_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Post","year":"2012","unstructured":"Post, A., Hoenicke, J.: Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 225\u2013240. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_18"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"issue":"2","key":"26_CR21","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. (STTT) 12(2), 123\u2013137 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277\u2013291. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-69778-0_28"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T13:02:03Z","timestamp":1570885323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}