{"corpus_id":259367532,"paper_sha":"d6af27dda1e9f18014f134e1dbf120817d808fc8","doi":"10.1109/LCSYS.2023.3287244","arxiv_id":null,"pmid":null,"pmcid":null,"mag_id":null,"dblp_id":"journals/csysl/HanS23","acl_id":null,"title":"Exploiting Invariance Properties to Certify Always and Eventually Signal Temporal Logic Operators for Hybrid Dynamical Systems","year":2023,"publication_date":null,"venue":"IEEE Control Systems Letters","journal":{"name":"IEEE Control Systems Letters","pages":"2809-2814","volume":"7"},"journal_issn":null,"journal_title":null,"publication_types":["JournalArticle"],"pubmed_pub_types":null,"s2_fields_of_study":["Mathematics","Computer Science"],"reference_count":20,"citation_count":1,"influential_citation_count":0,"is_open_access":false,"arxiv_categories":null,"arxiv_license":null,"arxiv_journal_ref":null,"mesh_headings":null,"chemicals":null,"comments_corrections":null,"source_flags":1,"s2_open_access_pdf_url":null,"s2_open_access_landing_url":null,"s2_open_access_license":null,"s2_open_access_status":null,"pmc_open_access_pdf_url":null,"pmc_open_access_landing_url":null,"pmc_open_access_license":null,"pmc_open_access_status":null,"unpaywall_open_access_pdf_url":null,"unpaywall_open_access_landing_url":null,"unpaywall_open_access_license":null,"unpaywall_open_access_status":null,"abstract":"In this letter, semantics and characterizations of signal temporal logic formulas for hybrid dynamical systems are presented. Hybrid dynamical systems are given in terms of constrained differential and difference inclusions, which, respectively, capture the continuous evolution and the instantaneous events exhibited by solutions. For such systems, the always and eventually operator of signal temporal logic are studied and characterizations in terms of dynamical properties of hybrid systems are presented – in particular, using invariance and finite-time attractivity properties. Sufficient conditions that guarantee the satisfaction of a signal temporal logic formula for a given system through the satisfaction of an untimed formula for an appropriately defined new system are introduced. Specifically, it is shown that satisfying an (untimed) temporal logic formula involving until operators suffices to certify always and eventually signal temporal logic formulas for hybrid systems.","claims":[{"public_id":"cl_94fb1b8300636a6f4785d72214f5b121","status":"active","text":"Satisfying an untimed temporal logic formula involving until operators is sufficient to certify always and eventually signal temporal logic formulas for hybrid systems.","confidence":0.9,"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/claims/cl_94fb1b8300636a6f4785d72214f5b121"},{"public_id":"cl_498f1563859adfaf602ee1af4231ae3c","status":"active","text":"Semantics of signal temporal logic formulas for hybrid dynamical systems are defined using constrained differential and difference inclusions that capture continuous evolution and instantaneous events.","confidence":0.85,"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/claims/cl_498f1563859adfaf602ee1af4231ae3c"},{"public_id":"cl_14f7b9f50f70a5921aaeb72232acc888","status":"active","text":"The always operator of signal temporal logic is characterized in terms of invariance properties of hybrid dynamical systems.","confidence":0.85,"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/claims/cl_14f7b9f50f70a5921aaeb72232acc888"},{"public_id":"cl_2000d159d308f770aca167fbb5e61536","status":"active","text":"The eventually operator of signal temporal logic is characterized in terms of finite-time attractivity properties of hybrid dynamical systems.","confidence":0.85,"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/claims/cl_2000d159d308f770aca167fbb5e61536"}],"concepts":[{"public_id":"co_05e8fbcc2d8e03bba8fdf74f983f1e88","status":"active","name":"finite-time attractivity","description":"A dynamical system property whereby solutions reach a target set within a finite amount of time.","types":["dynamical system property"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_05e8fbcc2d8e03bba8fdf74f983f1e88"},{"public_id":"co_25bdd5d2cc3d6186bf883c091abe6b58","status":"active","name":"constrained difference inclusions","description":"Set-valued difference equations restricted to a constraint (jump) set, used to model the instantaneous events of hybrid system solutions.","types":["mathematical model"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_25bdd5d2cc3d6186bf883c091abe6b58"},{"public_id":"co_2d1db0204955f2096ebc30acfc7a67df","status":"active","name":"constrained differential inclusions","description":"Set-valued differential equations restricted to a constraint (flow) set, used to model the continuous-time evolution of hybrid system solutions.","types":["mathematical model"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_2d1db0204955f2096ebc30acfc7a67df"},{"public_id":"co_3845d49e8d3f86aec5bbf4dbac98c83b","status":"active","name":"always operator","description":"The signal temporal logic operator requiring a specified property to hold throughout an interval of the signal.","types":["temporal logic operator"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_3845d49e8d3f86aec5bbf4dbac98c83b"},{"public_id":"co_43c653ea7df3bfd06aee37d46f0ec4f7","status":"active","name":"untimed temporal logic formula","description":"A temporal logic formula without explicit timing constraints, used as an auxiliary specification for an appropriately redefined system.","types":["logic formula"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_43c653ea7df3bfd06aee37d46f0ec4f7"},{"public_id":"co_6dcb5f9fb591b5ba1a38f4a56ad54f8c","status":"active","name":"invariance","description":"A dynamical system property whereby solutions starting in a given set remain within that set for all time.","types":["dynamical system property"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_6dcb5f9fb591b5ba1a38f4a56ad54f8c"},{"public_id":"co_9a1776bd59d89eb238d664d5a26b8292","status":"active","name":"eventually operator","description":"The signal temporal logic operator requiring a specified property to hold at some time within an interval of the signal.","types":["temporal logic operator"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_9a1776bd59d89eb238d664d5a26b8292"},{"public_id":"co_bb535607939fc0d10d397a2fe43653c2","status":"active","name":"until operator","description":"The temporal logic operator requiring one property to hold continuously until a second property becomes true.","types":["temporal logic operator"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_bb535607939fc0d10d397a2fe43653c2"},{"public_id":"co_c4d082baf082d0d05784881bf56b1424","status":"active","name":"signal temporal logic","description":"A temporal logic for specifying properties of real-valued signals over continuous and discrete time.","types":["temporal logic formalism"],"aliases":[],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_c4d082baf082d0d05784881bf56b1424"},{"public_id":"co_f75d81a600be38d88305a483835fb1f7","status":"active","name":"hybrid dynamical systems","description":"Systems whose solutions exhibit both continuous-time evolution and instantaneous discrete events.","types":["system model"],"aliases":["hybrid systems"],"contributors":[{"id":17,"public_id":"322360f1c1","public_label":"Killer Whale (322360f1c1)","roles":["extraction"],"url":"https://sah.borca.ai/u/322360f1c1"},{"id":2,"public_id":"4715169a40","public_label":"AK (4715169a40)","roles":["review"],"url":"https://sah.borca.ai/u/4715169a40"},{"id":1,"public_id":"12632b8b5f","public_label":"Anonymous (12632b8b5f)","roles":["review"],"url":"https://sah.borca.ai/u/12632b8b5f"}],"url":"https://sah.borca.ai/concepts/co_f75d81a600be38d88305a483835fb1f7"}],"external_ids":{"DOI":"10.1109/LCSYS.2023.3287244","ArXiv":null,"PubMed":null,"PubMedCentral":null,"MAG":null,"DBLP":"journals/csysl/HanS23","ACL":null},"open_access":{"is_open_access":false,"pdf_url":null,"landing_url":"https://sah.borca.ai/papers/259367532","source":null,"pdf_url_source":null,"license":null,"reason":"pdf_url_not_indexed"},"reference_availability":{"status":"available","references_indexed":true,"full_text_available":false,"full_text_source":null,"count_basis":"semantic_scholar_metadata","extraction_status":"not_applicable","reason":null},"source":{"provider":"episteme2","base_corpus":"semantic_scholar_dump","freshness_mode":"unknown","basis":["semantic_scholar_metadata","postgres_metadata"],"limits":["paper metadata is based on indexed upstream scholarly datasets","claims and concepts are available only for extracted papers","absence of claims or concepts means no extracted graph data is available in this response"],"status":"available","degraded":false,"degraded_reasons":[],"diagnostics":{"status":"available","degraded":false,"degraded_reasons":[],"metadata_status":"available","graph_status":"available","abstract_status":"available"},"source_flags":1},"paper_id":631667,"paper_uid":"58b014e0-efc0-43c0-b8a3-712873f1bedd","canonical_identity":{"paper_id":631667,"paper_uid":"58b014e0-efc0-43c0-b8a3-712873f1bedd","identity_status":"available","lookup_basis":"semantic_scholar_external_id","compatibility_path":"corpus_id"},"url":"https://sah.borca.ai/papers/259367532"}