{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:39Z","timestamp":1762459359575,"version":"3.28.0"},"reference-count":32,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1109\/memcod.2015.7340472","type":"proceedings-article","created":{"date-parts":[[2015,12,3]],"date-time":"2015-12-03T16:13:03Z","timestamp":1449159183000},"page":"70-79","source":"Crossref","is-referenced-by-count":23,"title":["Metric interval temporal logic specification elicitation and debugging"],"prefix":"10.1109","author":[{"given":"Adel","family":"Dokhanchi","sequence":"first","affiliation":[]},{"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.09.013"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-642-34691-0_11","article-title":"Querying parametric temporal logic properties on embedded systems","author":"yang","year":"2012","journal-title":"Testing Software and Systems"},{"key":"ref30","first-page":"663","article-title":"Analyzing unsynthesizable specifications for high-level robot behavior using ltimop","author":"raman","year":"2011","journal-title":"Computer Aided Venfication - 23rd International Conference CAV 2011 Snowbird UT USA July 14&#x2013;20 2011 Proceedings"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0060-y"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_9"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.09.006"},{"key":"ref14","first-page":"167","article-title":"Breach, a toolbox for verification and parameter synthesis of hybrid systems","author":"donze","year":"2010","journal-title":"Computer Aided Verification Volume 6174 of LNCS"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.157.12"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315384"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2011.5979895"},{"key":"ref18","first-page":"7","article-title":"A framework for inherent vacuity","author":"fisman","year":"2008","journal-title":"Hardware and Software Verification and Testing 4th International Haifa Verification Conference HVC 2008 Haifa Israel October 27&#x2013;30 2008 Proceedings"},{"key":"ref19","first-page":"451","article-title":"How vacuous is vacuous?","author":"gurfinkel","year":"2004","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems 10th International Conference TACAS 2004 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2004 Barcelona Spain March 29 - April 2 2004 Proceedings"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.19"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-007-0012-6"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"ref3","first-page":"368","article-title":"Enhanced vacuity detection in linear temporal logic","author":"armoni","year":"2003","journal-title":"Computer Aided Verification 15th International Conference CAV 2003 Boulder CO USA July 8&#x2013;12 2003 Proceedings"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"492","DOI":"10.1007\/978-3-540-74407-8_33","article-title":"Temporal antecedent failure: Refining vacuity","author":"ben-david","year":"2007","journal-title":"CONCUR 2007 - Concurrency Theory 18th International Conference CONCUR 2007 Lisbon Portugal September 3&#x2013;8 2007 Proceedings"},{"key":"ref29","first-page":"152","article-title":"Monitoring temporal properties of continuous signals","volume":"3253 of lncs","author":"maler","year":"2004","journal-title":"Proceedings of FORMATS-FTRTFT"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/196244.196575","article-title":"formally verifying a microprocessor using a simulation methodology","author":"beatty","year":"1994","journal-title":"31st Design Automation Conference"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_7"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0229-y"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","article-title":"S-taliro: A tool for temporal logic falsification for hybrid systems","volume":"6605 of lncs","author":"annapureddy","year":"2011","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.119.8"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781152"},{"key":"ref20","article-title":"Towards formal specification visualization for testing and monitoring of cyber-physical systems","author":"hoxha","year":"2014","journal-title":"Int'l Workshop on Design and Implementation of Formal Tools and Systems"},{"key":"ref22","article-title":"Mining requirements from closed-loop control models","author":"jin","year":"2013","journal-title":"Proceedings of the International Conference on Hybrid Systems Computation and Control (HSCC)"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2015.7353863"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0221-y"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6224826"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"}],"event":{"name":"2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","start":{"date-parts":[[2015,9,21]]},"location":"Austin, TX, USA","end":{"date-parts":[[2015,9,23]]}},"container-title":["2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7329076\/7340456\/07340472.pdf?arnumber=7340472","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,2]],"date-time":"2019-09-02T01:17:38Z","timestamp":1567387058000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7340472\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/memcod.2015.7340472","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}