{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T06:29:53Z","timestamp":1780381793047,"version":"3.54.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T00:00:00Z","timestamp":1556841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100010669","name":"H2020 LEIT Information and Communication Technologies","doi-asserted-by":"publisher","award":["732105"],"award-info":[{"award-number":["732105"]}],"id":[{"id":"10.13039\/100010669","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1007\/s11334-019-00339-1","type":"journal-article","created":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:10:09Z","timestamp":1556889009000},"page":"307-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Property specification patterns at work: verification and inconsistency explanation"],"prefix":"10.1007","volume":"15","author":[{"given":"Massimo","family":"Narizzano","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luca","family":"Pulina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6617-2874","authenticated-orcid":false,"given":"Simone","family":"Vuotto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,5,3]]},"reference":[{"key":"339_CR1","doi-asserted-by":"crossref","unstructured":"Awad A, Gor\u00e9 R, Thomson J, Weidlich M (2011) An iterative approach for business process template synthesis from compliance rules. In: International conference on advanced information systems engineering, Springer, pp 406\u2013421","DOI":"10.1007\/978-3-642-21640-4_31"},{"key":"339_CR2","first-page":"276","volume":"93","author":"RR Bakker","year":"1993","unstructured":"Bakker RR, Dikker F, Tempelman F, Wognum PM (1993) Diagnosing and solving over-determined constraint satisfaction problems. IJCAI 93:276\u2013281","journal-title":"IJCAI"},{"issue":"1","key":"339_CR3","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-015-0348-9","volume":"28","author":"J Barnat","year":"2016","unstructured":"Barnat J, Bauch P, Bene\u0161 N, Brim L, Beran J, Kratochv\u00edla T (2016) Analysing sanity of requirements for avionics systems. Form Asp Comput 28(1):45\u201363","journal-title":"Form Asp Comput"},{"key":"339_CR4","unstructured":"Belov A, Marques-Silva J (2011) Accelerating MUS extraction with recursive model rotation. In: Formal methods in computer-aided design (FMCAD), 2011. pp 37\u201340. IEEE"},{"key":"339_CR5","first-page":"123","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov A, Marques-Silva J (2012) Muser2: an efficient mus extractor. J Satisf Boolean Model Comput 8:123\u2013128","journal-title":"J Satisf Boolean Model Comput"},{"key":"339_CR6","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J (2017) Consistency checking in requirements analysis. In: Proceedings of the 26th ACM SIGSOFT international symposium on software testing and analysis, pp 408\u2013411. ACM","DOI":"10.1145\/3092703.3098239"},{"key":"339_CR7","unstructured":"Bertello M, Gigante N, Montanari A (2016) Reynolds M Leviathan: A new ltl satisfiability checking tool based on a one-pass tree-shaped tableau. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, AAAI Press, pp 950\u2013956. IJCAI\u201916, \n                    http:\/\/dl.acm.org\/citation.cfm?id=3060621.3060753"},{"issue":"2","key":"339_CR8","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"JW Chinneck","year":"1991","unstructured":"Chinneck JW, Dravnieks EW (1991) Locating minimal infeasible constraint sets in linear programs. ORSA J Comput 3(2):157\u2013168","journal-title":"ORSA J Comput"},{"key":"339_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: 14th international conference on computer aided verification (CAV 2002), pp 359\u2013364","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"2","key":"339_CR10","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Progr Lang Syst (TOPLAS) 8(2):244\u2013263","journal-title":"ACM Trans Progr Lang Syst (TOPLAS)"},{"key":"339_CR11","doi-asserted-by":"crossref","unstructured":"Comon H, Cortier V (2000) Flatness is not a weakness. In: International workshop on computer science logic, pp 262\u2013276","DOI":"10.1007\/3-540-44622-2_17"},{"issue":"3","key":"339_CR12","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri S, DSouza D (2007) An automata-theoretic approach to constraint LTL. Inf Comput 205(3):380\u2013415","journal-title":"Inf Comput"},{"issue":"2","key":"339_CR13","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10878-008-9142-4","volume":"18","author":"C Desrosiers","year":"2009","unstructured":"Desrosiers C, Galinier P, Hertz A, Paroz S (2009) Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J Comb Optim 18(2):124\u2013150","journal-title":"J Comb Optim"},{"issue":"2","key":"339_CR14","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"LK Dillon","year":"1994","unstructured":"Dillon LK, Kutty G, Moser LE, Melliar-Smith PM, Ramakrishna YS (1994) A graphical interval logic for specifying concurrent systems. ACM Trans Softw Eng Methodol (TOSEM) 3(2):131\u2013165","journal-title":"ACM Trans Softw Eng Methodol (TOSEM)"},{"key":"339_CR15","doi-asserted-by":"crossref","unstructured":"Dokhanchi A, Hoxha B, Fainekos G (2015) Metric interval temporal logic specification elicitation and debugging. In: 13th ACM-IEEE international conference on formal methods and models for codesign, pp 21\u201323","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"339_CR16","unstructured":"Dokhanchi A, Hoxha B, Fainekos G (2016) Formal requirement debugging for testing and verification of cyber-physical systems. arXiv preprint \n                    arXiv:1607.02549"},{"key":"339_CR17","unstructured":"Dravnieks EW (1989) Identifying minimal sets of inconsistent constraints in linear programs: deletion, squeeze and sensitivity filtering. Carleton University"},{"key":"339_CR18","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"339_CR19","unstructured":"Fisman D, Kupferman O, Sheinvald-Faragy S, Vardi MY (2008) A framework for inherent vacuity. In: Haifa verification conference, Springer, pp 7\u201322"},{"key":"339_CR20","unstructured":"Gor\u00e9 R, Huang J, Sergeant T, Thomson J (2013) Finding minimal unsatisfiable subsets in linear temporal logic using BDDS. \n                    https:\/\/www.timsergeant.com\/files\/pltlmup\/gore_huang_sergeant_thomson_mus_pltl.pdf"},{"key":"339_CR21","unstructured":"Hustadt U, Konev B (2003) TRP++ 2.0: A temporal resolution prover. In: 19th international conference on automated deduction, pp 274\u2013278"},{"key":"339_CR22","unstructured":"Junker U (2001) Quickxplain: Conflict detection for arbitrary constraint propagation algorithms. In: IJCAI01 workshop on modelling and solving problems with constraints"},{"key":"339_CR23","doi-asserted-by":"crossref","unstructured":"Kesten Y, Manna Z, McGuire H, Pnueli A (1993) A decision algorithm for full propositional temporal logic. In: International conference on computer aided verification, Springer, pp 97\u2013109","DOI":"10.1007\/3-540-56922-7_9"},{"key":"339_CR24","unstructured":"Konrad S, Cheng BH (2005) Real-time specification patterns. In: Proceedings of the 27th international conference on software engineering, pp 372\u2013381"},{"key":"339_CR25","unstructured":"Li J, Pu G, Zhang L, Yao Y, Vardi M Y et\u00a0al. (2013) Polsat: A portfolio LTL satisfiability solver. arXiv preprint \n                    arXiv:1311.1602"},{"key":"339_CR26","doi-asserted-by":"crossref","unstructured":"Li J, Yao Y, Pu G, Zhang L, He J (2014) 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","DOI":"10.1145\/2635868.2661669"},{"key":"339_CR27","doi-asserted-by":"crossref","unstructured":"Li J, Zhang L, Pu G, Vardi MY, He J (2013) LTL satisfiability checking revisited. In: 20th international symposium on temporal representation and reasoning, pp 91\u201398","DOI":"10.1109\/TIME.2013.19"},{"key":"339_CR28","doi-asserted-by":"crossref","unstructured":"Li J, Zhu S, Pu G, Vardi MY (2015) Sat-based explicit LTL reasoning. In: 11th Haifa verification conference, pp 209\u2013224","DOI":"10.1007\/978-3-319-26287-1_13"},{"key":"339_CR29","unstructured":"Liffiton MH, Malik A (2013) Enumerating infeasibility: finding multiple muses quickly. In: International conference on AI and OR techniques in constraint programming for combinatorial optimization problems, Springer, pp 160\u2013175"},{"issue":"1","key":"339_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton MH, Sakallah KA (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason 40(1):1\u201333","journal-title":"J Autom Reason"},{"key":"339_CR31","doi-asserted-by":"crossref","unstructured":"Lumpe M, Meedeniya I, Grunske L (2011) 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","DOI":"10.1145\/2025113.2025193"},{"key":"339_CR32","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems, Springer, pp 152\u2013166","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"339_CR33","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"2012","unstructured":"Manna Z, Pnueli A (2012) Temporal verification of reactive systems: safety. Springer, Berlin"},{"key":"339_CR34","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Lynce I (2011) On improving MUS extraction algorithms. In: International conference on theory and applications of satisfiability testing. Springer, pp 159\u2013173","DOI":"10.1007\/978-3-642-21581-0_14"},{"key":"339_CR35","doi-asserted-by":"crossref","unstructured":"Masin M, Palumbo F, Myrhaug H, de\u00a0Oliveira\u00a0Filho J, Pastena M, Pelcat M, Raffo L, Regazzoni F, Sanchez A, Toffetti A, et\u00a0al. (2017) Cross-layer design of reconfigurable cyber-physical systems. In: 2017 design, automation & test in Europe conference & exhibition (DATE), pp 740\u2013745. IEEE","DOI":"10.23919\/DATE.2017.7927088"},{"key":"339_CR36","unstructured":"Nadel A (2010) Boosting minimal unsatisfiable core extraction. In: Proceedings of the 2010 conference on formal methods in computer-aided design, pp 221\u2013229. FMCAD Inc"},{"key":"339_CR37","doi-asserted-by":"crossref","unstructured":"Narizzano M, Pulina L, Tacchella A, Vuotto S (2018) Consistency of property specification patterns with boolean and constrained numerical signals. In: NASA formal methods: 10th international symposium, NFM 2018, Newport News, VA, USA, April 17\u201319, 2018, Proceedings, vol 10811. Springer, pp 383\u2013398","DOI":"10.1007\/978-3-319-77935-5_26"},{"key":"339_CR38","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977, pp 46\u201357. IEEE","DOI":"10.1109\/SFCS.1977.32"},{"key":"339_CR39","unstructured":"Pnueli A, Manna Z (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin 16:12"},{"key":"339_CR40","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 179\u2013190. ACM","DOI":"10.1145\/75277.75293"},{"key":"339_CR41","doi-asserted-by":"crossref","unstructured":"Post A, Hoenicke J (2012) Formalization and analysis of real-time requirements: a feasibility study at BOSCH. Verified software: theories, tools, experiments, pp 225\u2013240","DOI":"10.1007\/978-3-642-27705-4_18"},{"key":"339_CR42","doi-asserted-by":"crossref","unstructured":"Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Spin. vol. 4595, pp 149\u2013167. Springer","DOI":"10.1007\/978-3-540-73370-6_11"},{"issue":"2","key":"339_CR43","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier KY, Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf (STTT) 12(2):123\u2013137","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"key":"339_CR44","unstructured":"Rozier KY, Vardi MY (2011) A multi-encoding approach for LTL symbolic satisfiability checking. In: International symposium on formal methods, Springer, pp 417\u2013431"},{"issue":"3","key":"339_CR45","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s00236-015-0242-1","volume":"53","author":"V Schuppan","year":"2016","unstructured":"Schuppan V (2016) Extracting unsatisfiable cores for lTl via temporal resolution. Acta Inform 53(3):247\u2013299","journal-title":"Acta Inform"},{"key":"339_CR46","doi-asserted-by":"crossref","unstructured":"Schwendimann S (1998) A new one-pass tableau calculus for PLTL. In: International conference on automated reasoning with analytic tableaux and related methods, Springer, pp 277\u2013291","DOI":"10.1007\/3-540-69778-0_28"},{"issue":"110\/111","key":"339_CR47","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper P (1985) The tableau method for temporal logic: an overview. Logique et Analyse 28(110\/111):119\u2013136","journal-title":"Logique et Analyse"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00339-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-019-00339-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00339-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T23:20:33Z","timestamp":1588375233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-019-00339-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,3]]},"references-count":47,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["339"],"URL":"https:\/\/doi.org\/10.1007\/s11334-019-00339-1","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5,3]]},"assertion":[{"value":"1 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 April 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}